Locally Cartesian Closed Quasicategories from Type Theory

TL;DR

This paper demonstrates that quasicategories derived from models of Martin-Löf type theory through simplicial localization possess the property of being locally cartesian closed, linking type theory and higher category theory.

Contribution

It establishes a new connection between models of type theory and higher category theory by proving local cartesian closure of certain quasicategories.

Findings

Quasicategories from Martin-Löf type theory models are locally cartesian closed.

The result bridges type theory and higher category theory.

Provides a foundation for further categorical semantics of type theories.

Abstract

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