A cubical model of homotopy type theory

Steve Awodey

We construct an algebraic weak factorization system $(L,R)$ on the cartesian cubical sets, in which the canonical path object factorization $A\to A^I\to A\times A$ induced by th…