Personal tools

The Erwin Schroedinger Institute for Mathematical Physics

Paige North (U Cambridge): Weak factorization systems for intensional type theory

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

At a glance

Type: Lecture
When: May 20, 2015
from 02:15 PM to 03:15 PM
Where: ESI, Schrödinger Lecture Hall
Add event to calendar: vCal
iCal