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).

From Awodey 09, p. 13, Awodey 10, p. 15:

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. the internal logic of (∞,1)-toposes is univalent homotopy type theory

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

2. there is a model of (univalent) homotopy type theory in any $(\infty,1)$-topos

   (this version has a proof, see below);

3. homotopy type theory is synthetic homotopy theory

   (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

• André Joyal, Remarks on homotopical logic Oberwolfach (2011) (pdf)

and stated more precisely in

• Chris Kapulkin, Peter Lumsdaine, The homotopy theory of type theories, Advances in Mathematics 337 (2018) 1-38 $[$arXiv:1610.00037, doi:10.1016/j.aim.2018.08.003$]$

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

• Michael Shulman, Example 2.16 of Univalence for inverse diagrams and homotopy canonicity, Mathematical Structures in Computer Science, Volume 25, Issue 5 ( From type theory and homotopy theory to Univalent Foundations of Mathematics ) June 2015 (arXiv:1203.3253, doi:/10.1017/S0960129514000565)

following

• Denis-Charles Cisinski, blog comment (2012)

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

• Shulman 12

• Michael Shulman, The univalence axiom for elegant Reedy presheaves, Homology, Homotopy and Applications Volume 17 (2015) Number 2 (arXiv:1307.6248, doi:10.4310/HHA.2015.v17.n2.a6)

A general proof was announced in

• Michael Shulman, slides 5 to 10 of: Semantics of higher modalities, talk at Geometry in Modal HoTT (2019) (pdf slides, video recording)

and appeared in

• Michael Shulman, All $(\infty,1)$-toposes have strict univalent universes (arXiv:1904.07004)

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$]$