Speaker
Astra Kolomatskaia, Wesleyan University
Abstract
Displayed Type Theory [dTT] is an analytic approach to formalising higher category theory, designed to treat higher coherence directly rather than synthetically. Joint work with Mike Shulman, dTT is semantically general: it admits models in any CwF with Π-types, universes, and suitable coinductive types. In particular, it defines semi-simplicial types directly, rather than axiomatizing their expected properties. A modally closed fragment of dTT has been implemented by Shulman in Narya. I will survey the basic ideas of dTT and present a Narya formalisation of Kan complexes.
Astra Kolomatskaia, Wesleyan University
Abstract
Displayed Type Theory [dTT] is an analytic approach to formalising higher category theory, designed to treat higher coherence directly rather than synthetically. Joint work with Mike Shulman, dTT is semantically general: it admits models in any CwF with Π-types, universes, and suitable coinductive types. In particular, it defines semi-simplicial types directly, rather than axiomatizing their expected properties. A modally closed fragment of dTT has been implemented by Shulman in Narya. I will survey the basic ideas of dTT and present a Narya formalisation of Kan complexes.