BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Definitional Functoriality for Dependent (Sub)Types  - Dr Meven Le
 nnon-Bertrand (University of Cambridge)
DTSTART:20231002T120000Z
DTEND:20231002T130000Z
UID:TALK206494@talks.cam.ac.uk
CONTACT:47138
DESCRIPTION:There are two standard approaches to subtyping. In the subsump
 tive one\, subtyping is implicit and does not appear in program code\, whi
 le 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.\n\nTo resolve this\, one can elab
 orate 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.\n\nAs usual\, the story becomes 
 more complicated with dependent types\, where the equational theory of pro
 grams 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 equation
 s to MLTT while keeping all the other good properties\, allowing for a typ
 e-preserving elaboration\, reconciling the semanticists and the users.
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR