Identity types in Algebraic Model Structures

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

• Andrew Swan, The Logic Group, School of Mathematics, University of Leeds
• Friday 12 February 2016, 14:00-15:00
• FW11.

If you have a question about this talk, please contact Ohad Kammar.

NOTE UNUSUAL VENUE This is the second seminar this week.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW11
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.