#HoTT #HTTUF Homotopy type theory =#HigherToposTheory ?

  1.  https://homotopytypetheory.org

»Homotopy Type Theory refers to a new field of study relating Martin-Löf’s system of intensional, constructive type theory with abstract homotopy theory. … As the natural logic of homotopy, constructive type theory is also related to higher category theoryas it is used e.g. in the notion of a higher topos. »


Click to access CoqHoTT-local.pdf

Page 24 sur 31 :

Homotopy type theory = Higher topos theory ( en encadré)


Click to access 1807.02177.pdf

page 3 sur 21

« it is suspected  that HoTT can be modeled in higher toposes , more precisely (∞,1)-toposes »


« Working in the (∞,1)-category ∞Grpd of (∞,0)-categories amounts to doing homotopy theory. The point of (∞,1)-sheaves is to pass to parameterized (∞,0)-categories, namely (∞,1)-presheaf categories. Although these (∞,1) (∞,1) ∞Grpd, their objects are generalized spaces with higher homotopies that may carry more structure. More generally we have topoi of sheaves, and (∞,1) (∞,1)-sheaves. For instance, an ∞-Lie groupoid is an (∞,1)-sheaf on CartSp

«The Cartesian cubical model of cubical type theory and homotopy type theory is conjectured to be an (∞,1)-topos not equivalent to (∞,1)-groupoids. »

« Syntax in univalent homotopy type theory

(∞,1) categorical semantics for homotopy type theory with a univalent Tarskian type of types (which inteprets as the object classifier).«

Ce qui est développé dans :



1. Overview

It is expected that every elementary (infinity,1)-topos admits a model of homotopy type theory with the univalence axiom and higher inductive types. However, so far there is not a standard definition of elementary (∞,1) almost know that every Grothendieck (infinity,1)-topos admits such a model; the caveat is that we only get univalent universes that are weakly a la Tarski (see universe).« 

Et dans:



While (∞,1)-sheaf (∞,1)-toposes are those currently understood, the basic type theory with univalent universes does not see or care about their local presentability as such (although it is used in other places, such as the construction of higher inductive types). It is to be expected that there is a decent concept of elementary (∞,1)-topos such that homotopy type theory with univalent type universes and some supply of higher inductive types has categorical semantics precisely in elementary (∞,1)-toposes (as conjectured in Awodey 10). But the fine-tuning of this statement is currently still under investigation.

Notice that this statement, once realized, makes (or would make) Univalent HoTT+HITs a sort of homotopy theoreticrefinement of foundations of mathematics in topos theory as proposed by William Lawvere. It could be compared to his elementary theory of the category of sets, although being a type theory rather than a theory in first-order logic, it is more analogous to the internal type theory of an elementary topos.«


An adjunction between the category of type theories with product types and toposes is discussed in chapter II of

  • Joachim Lambek, P. Scott, Introduction to higher order categorical logic, Cambridge University Press (1986) . »


A precise definition of elementary (infinity,1)-topos inspired by giving a natural equivalence to homotopy type theorywith univalence was then proposed in


Proof that all ∞-stack (∞,1)-topos have presentations by model categories which interpret (provide categorical semantics) for homotopy type theory with univalent type universes:

Michael Shulman, All (∞,1) (arXiv:1904.07004).«





This entry was posted in EHTT, Higher category theory, Higher topos theory, homotopy type theory, HTTUF, Science, mathesis, Science-internelle. Bookmark the permalink.