A cubical model of homotopy type theory

TL;DR

This paper develops a cubical model for homotopy type theory by constructing an algebraic weak factorization system on cartesian cubical sets, enabling canonical path object factorizations.

Contribution

It introduces a novel algebraic weak factorization system on cartesian cubical sets that models homotopy type theory more effectively.

Findings

Established an algebraic weak factorization system on cubical sets.

Provided a canonical path object factorization for homotopy models.

Enhanced the algebraic framework for homotopy type theory.

Abstract

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 the 1-cube $I$ is an $L$-$R$ factorization for any $R$-object $A$.