![[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)
Andrew Swan, The Logic Group, School of Mathematics, University of Leeds 
Friday 12 February 2016, 14:00-15:00
Identity types in Algebraic Model Structures
- 👤 Speaker: Andrew Swan, The Logic Group, School of Mathematics, University of Leeds 🔗 Website
- 📅 Date & Time: Friday 12 February 2016, 14:00 - 15:00
- 📍 Venue: FW11
Abstract
The original Bezem-Coquand-Huber cubical set model promised to give a constructive model of homotopy type theory. However, in its original form there was a notable shortcoming: one of the definitional equalities usually included in type theory, the J computation rule was absent. One way to fix this is to use an alternative definition of identity type in which we keep track more carefully of degenerate paths. The new identity type has a nice presentation in the setting of algebraic model structures. I’ll use this idea to show that in particular cubical sets with Kan fibrations satisfy Garner and van den Berg’s notion of “homotopy theoretic model of identity types.” In this way we get a constructive proof that cubical sets model intensional type theory including all definitional equalities.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- FW11
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- tcw57’s list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.