[msp-interest] [MSP101] Fredrik Nordvall Forsberg: Representing type theory in type theory (LT412, 3pm Mon 3-Mar)

[Dilsat Yuksel]

Hi,

On Monday, the MSP101 talk will be given by Fredrik Nordvall Forsberg (MSP). See the details of the talk below.

Best,
Dilsat

**********************************************************************

Date: Monday, 3 March at 15:00

Room: LT412, Livingstone Tower

Zoom link: https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1
Live stream on Youtube: https://www.youtube.com/@msp101strathclyde4

Speaker: Fredrik Nordvall Forsberg

Title: Representing type theory in type theory

Abstract: It is often claimed that type theory can act as a foundation of mathematics. If that is so, then type theory should in particular be able to reason about type theory itself. Of course, Dr Gödel points out that this cannot work, in general, but we would expect that type theory could still reason about a slightly weaker version of itself. This turns out to be true, but messy, because type theory is quite complicated as a theory. After heroic attempts by Danielsson (2006) and Chapman (2009) to represent type theory internally in type theory, Altenkirch and Kaposi (2016) made a breakthrough in using so-called quotient inductive-inductive types to represent the well typed terms of type theory, where quotient constructors are used to encode beta and eta laws as equalities in the type. Being able to treat such laws as actual equalities is a major improvement, but quickly leads into so-called transport hell, where explicit transports along equalities show up in terms and needs to be reasoned about. I will report on some recent work together with Liang-Ting Chen and Tzu-Chun Tsai on how one can use experimental (and hopefully future) features of Agda to improve on the quotient inductive-inductive representation and remove most uses of transport.

**********************************************************************

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20250227/dbfc407b/attachment.html