# nLab Awodey's proposal

Contents

### Context

#### $(\infty,1)$-Topos Theory

(∞,1)-topos theory

## Constructions

structures in a cohesive (∞,1)-topos

# Contents

## Idea

### Statement

In Awodey 09, Awodey 10 was first expressed the idea that dependent type theory with intensional identity types (Martin-Löf dependent type theory), viewed as homotopy type theory, is in similar relation to the concept of (∞,1)-toposes as extensional type theory is to the ordinary concept of toposes (as discussed at relation between type theory and category theory).

The homotopy interpretation of Martin-Löf type theory into Quillen model categories, and the related results on type-theoretic constructions of higher groupoids, are analogous to basic results interpreting extensional type theory and higher-order logic in (1-)toposes, and clearly indicate that the logic of higher toposes, and therewith of higher homotopy theory, is a form of intensional type theory.

A concise re-statement would be that:

1. (though there is fine print involved, e.g. the initiality conjecture);

2. (this version has a proof, see below);

3. (this may be read as a suggestive colloquial version of the previous statement, remaining vague on whether univalence is considered or not).

Following this suggestion, the weaker form of this idea, ignoring the univalent type universe and relating to the broader class of locally Cartesian closed (∞,1)-categories, was stated more concretely as a conjecture in Joyal 11. For more precision see Kapulkin-Lumsdaine 16, p. 9.

Roughly, this is about the following table of correspondences (for more see at relation between type theory and category theory):

Fore more precision see Kapulkin-Lumsdaine 16, p. 9.

### Proof

A proof of the weaker version of the conjecture, in form of the statement that every locally presentable locally Cartesian closed (∞,1)-category is presented by a suitable type theoretic model category which provides categorical semantics for homotopy type theory, was proven in Shulman 12, Example 2.16, following Cisinski 12.

Generalizing this to a proof of the full conjecture required finding “strict” models for the object classifier by strict type universes. A series of article (Shulman 12, Shulman 13) showed that this is possible in an increasing class of special cases.

A proof of the general case was finally announced in Shulman 19.

For more see at model of type theory in an (infinity,1)-topos.

## References

### Statement

The idea is due to

• Steve Awodey, Homotopy and Type Theory, grant proposal project description (pdf)

• Steve Awodey, Type theory and homotopy, in: Dybjer P., Lindström S., Palmgren E., Sundholm G. (eds.), Epistemology versus Ontology, Springer (2012) 183-201 $[$arXiv:1010.1810, doi:10.1007/978-94-007-4435-6_9$]$

A pronounced statement of the weaker version was highlighted in

and stated more precisely in

### Proof

The proof of the weaker version of Awodey’s conjecture (that every locally Cartesian closed (∞,1)-category has a presentation by a suitable type-theoretic model category which provides categorical semantics for homotopy type theory) is due, independently, to

following

The proof of the stronger version (including univalent type universes modelling object classifier of (∞,1)-toposes) was found for the special case of (∞,1)-presheaf (∞,1)-toposes over elegant Reedy categories in

A general proof was announced in

and appeared in

It is reviewed in:

• Emily Riehl, On the $\infty$-topos semantics of homotopy type theory, lecture at Logic and higher structures CIRM (Feb. 2022) $[$pdf, pdf$]$

Last revised on June 17, 2022 at 10:38:30. See the history of this page for a list of all contributions to it.