COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## Identity types in Algebraic Model StructuresAdd 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. |
## Other listsCambridge Lymphoma Network (CaLy) Indo-European Seminar Justice and Communities Research Unit, Anglia Ruskin University henry moore Kelvin Club - The Scientific Society of Peterhouse, Cambridge LMS Invited Lectures 2011## Other talksDeep & Heavy: Using machine learning for boosted resonance tagging and beyond Uncertainty Quantification with Multi-Level and Multi-Index methods Overview of Research Process Cohomology of the moduli space of curves Developing an optimisation algorithm to supervise active learning in drug discovery A lifelong project in clay: Virtues of Unity |