Univalence for inverse EI diagrams

We construct a new model category presenting the homotopy theory of presheaves on “inverse $\mathrm{EI} (\infty,1)$-categories”, which contains universe objects that satisfy Voevodsky’s univalence axiom. In addition to diagrams on ordinary inverse categories, as considered in previous work of the author, this includes a new model for equivariant algebraic topology with a compact Lie group of equivariance. Thus, it offers the potential for applications of homotopy type theory to equivariant homotopy theory.

Keywords

homotopy type theory, univalence axiom, inverse category, EI-category

2010 Mathematics Subject Classification

03G30, 18G55, 55U35

Full Text (PDF format)

This material is based on research sponsored by The United States Air Force Research Laboratory under agreement number FA9550-15-1-0053. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the United States Air Force Research Laboratory, the U.S. Government, or Carnegie Mellon University.

Received 18 August 2016

Received revised 24 March 2017

Published 15 November 2017