![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Tuesday 12 May 2015, 14:15-15:15
Weak factorization systems for intensional type theory
- 👤 Speaker: Paige North - DPMMS ( DPMMS)
- 📅 Date & Time: Tuesday 12 May 2015, 14:15 - 15:15
- 📍 Venue: MR5, Centre for Mathematical Sciences
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.
Series This talk is part of the Category Theory Seminar series.
Included in Lists
- All CMS events
- All Talks (aka the CURE list)
- bld31
- Category Theory Seminar
- CMS Events
- DPMMS info aggregator
- DPMMS lists
- DPMMS Lists
- DPMMS Pure Maths Seminar
- Hanchen DaDaDash
- Interested Talks
- MR5, Centre for Mathematical Sciences
- ndb35's list
- School of Physical Sciences
- yk373's list
Note: Ex-directory lists are not shown.