University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Identity types in Algebraic Model Structures

Identity types in Algebraic Model Structures

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

  • UserAndrew Swan, The Logic Group, School of Mathematics, University of Leeds World_link
  • ClockFriday 12 February 2016, 14:00-15:00
  • HouseFW11.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2020, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity