A cubical model of homotopy type theory
Category Theory
2016-07-22 v1 Logic
Abstract
We construct an algebraic weak factorization system on the cartesian cubical sets, in which the canonical path object factorization induced by the 1-cube is an - factorization for any -object .
Keywords
Cite
@article{arxiv.1607.06413,
title = {A cubical model of homotopy type theory},
author = {Steve Awodey},
journal= {arXiv preprint arXiv:1607.06413},
year = {2016}
}
Comments
Lecture notes from a series of lectures for the Stockholm Logic group