Definitional Functoriality for Dependent (Sub)Types

Add to your list(s) Download to your calendar using vCal

• Dr Meven Lennon-Bertrand (University of Cambridge)
• Monday 02 October 2023, 13:00-14:00
• FS07, Computer Laboratory.

If you have a question about this talk, please contact nk480.

There are two standard approaches to subtyping. In the subsumptive one, subtyping is implicit and does not appear in program code, while in the coercive one each usage of subtyping has to be explicitly marked, using a form of coercion. Coercions should not be written by users: it is the work of a type-checker to put them in. Yet, they make the life of the semanticist much easier and cleaner.

To resolve this, one can elaborate programs from the subsumptive to the coercive discipline, by adding coercions wherever needed, based on a typing derivation. Yet, multiple derivations for the same program lead to different elaborations. This is tackled by a coherence theorem, which says that any two elaboration of the same program have the same semantics.

As usual, the story becomes more complicated with dependent types, where the equational theory of programs appears during typing. In other words, to show that elaboration is type-preserving, we need coherence to hold. Yet, the equations demanded by coherence, which correspond to a form of functoriality of type-formers, do not hold on the nose in vanilla Martin-Löf Type Theory. Fortunately, this is repairable: I will show how to add these functoriality equations to MLTT while keeping all the other good properties, allowing for a type-preserving elaboration, reconciling the semanticists and the users.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FS07, Computer Laboratory

Note that ex-directory lists are not shown.