Vojtěch Štěpančík: Properties of type families over pushouts in Homotopy Type Theory

Abstract: Homotopy Type Theory characterizes the identity type of universes via the univalence axiom, which allows us to construct non-trivial commuting diagrams involving the universe type. Those in turn provide a way to construct type families over higher inductive types.

The talk will explore the particular case of pushouts. We will characterize the data necessary to glue together a type family over a pushout (the descent property), and show that total spaces of such families are again pushouts (the flattening lemma). We conclude by using the built infrastructure to give an induction principle of identity types of pushouts.