Weak factorization systems for intensional type theory

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

• Paige North - DPMMS ( DPMMS)
• Tuesday 12 May 2015, 14:15-15:15
• MR5, Centre for Mathematical Sciences.

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.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Category Theory Seminar
• DPMMS Lists
• DPMMS Pure Maths Seminar
• DPMMS info aggregator
• DPMMS lists
• Hanchen DaDaDash
• Interested Talks
• MR5, Centre for Mathematical Sciences
• School of Physical Sciences
• bld31
• ndb35's list
• yk373's list

Note that ex-directory lists are not shown.