Steve Awodey: Homotopy type theory: A cubical algebraic weak factorization system

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.