Locally Cartesian Closed Quasicategories from Type Theory

Abstract

We prove that the quasicategories arising from models of Martin-Löf type theory via simplicial localization are locally cartesian closed.

21 pages; to appear in J. Topology

References in corpus (2)

• The local universes model: an overlooked coherence construction for dependent type theories
• Two Models for the Homotopy Theory of Cocomplete Homotopy Theories

Cited by in corpus (2)

• The homotopy theory of type theories
• Univalence and completeness of Segal objects