On a model invariance problem in homotopy type theory

DOI10.1007/S10485-019-09558-WzbMath1428.18043arXiv1712.03409OpenAlexW2963386411WikidataQ128459578 ScholiaQ128459578MaRDI QIDQ2423835

Anthony Bordg

Publication date: 20 June 2019

Published in: Applied Categorical Structures (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1712.03409

zbMATH Keywords

universegroupoidhomotopy type theoryunivalence axiomgroupoid modelQuillen model categoryunivalent foundationsinjective model structuremodel invariance problemtype-theoretic fibration category

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Homotopical algebra, Quillen model categories, derivators (18N40) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Cites Work

• Unnamed Item
• Univalence for inverse EI diagrams
• Higher Topos Theory (AM-170)
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves

This page was built for publication: On a model invariance problem in homotopy type theory