English

A cubical model of homotopy type theory

Category Theory 2016-07-22 v1 Logic

Abstract

We construct an algebraic weak factorization system (L,R)(L, R) on the cartesian cubical sets, in which the canonical path object factorization AAIA×AA \to A^I \to A\times A induced by the 1-cube II is an LL-RR factorization for any RR-object AA.

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