University of Cambridge > Talks.cam > Category Theory Seminar > Weak factorization systems for intensional type theory

Weak factorization systems for intensional type theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dr Ignacio Lopez Franco.

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.

This talk is part of the Category Theory Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity