Steve Awodey: Homotopy type theory: A cubical algebraic weak factorization system
Time: Wed 2016-06-01 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university
Participating: Steve Awodey, Carnegie Mellon University, Pittsburgh
Abstract: Fourth and final lecture in the series previously advertised. We prove that the category of cartesian cubical sets carries an algebraic weak factorization system in which every fibration admits the canonical pathobject factorization of the diagonal map. As a consequence, the cubical semantics for Martin-Löf type theory developed in the previous lectures soundly model all the rules for identity types.