Menno de Boer: The Gluing Construction for Path Categories

Abstract: Path Categories are a categorical semantics for homotopy type theory with propositional identity types. In this type theory, the judgmental equality in the elimination rules is replaced by propositional equality. This has some direct consequences when one deals with universal constructions like exponentials and natural numbers object: they will have a homotopic counterpart. Additionally, if one has an appropriate functor F between two such categories, it is possible to define a new path category GL(F), called the gluing category. During my master's thesis I have studied this gluing category and specifically when it preserves these homotopy universal constructions.

During my talk, I will first give a motivation for such gluing constructions, before I will introduce you to Path Categories. After this introduction, I will give the definitions of homotopy universal constructions and the gluing category, before ending with some of the results from my thesis regarding these constructions. I will assume basic knowledge of category theory and some intuitive understanding of type theory.