Abstract:

In their paper, van den Berg and Garner [1] described algebraic conditions on an endofunctor of a category which enable it to represent the identity type in an interpretation of dependent type theory. In this talk, I will describe the weak factorization systems that can give rise to such an endofunctor, thus characterizing the weak factorization systems that can interpret intensional type theory. In fact, they are exactly those in which (1) every object is fibrant and (2) the left class of maps is stable under pullback along the right class. I will also talk about internal categories and presheaves in such a category, and under which conditions they themselves form a category that can interpret intensional type theory.

[1] Benno van den Berg and Richard Garner, “Topological and simplicial models of 
identity types,” ACM Trans. Comput. Log. 13.1 (2012), Art. 3, 44.

Flyer