nLab internal logic of an (infinity,1)-topos



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


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

(∞,1)-topos theory

structures in a cohesive (∞,1)-topos



Just as an ordinary elementary topos comes with its internal logic formalized by type theory, an elementary (∞,1)-topos should come with its internal “(,1)(\infty,1)-logic” formalized by homotopy type theory.

Type theory versus logic

As remarked at type theory, it is useful to distinguish between the internal type theory of a category and the internal logic which sits on top of that type theory. The type theory is about constructing objects, while the logic is about constructing subobjects. For instance, limits and colimits, exponentials, and object classifiers belong to the type theory, while images, dual images?, intersections, unions, and subobject classifiers belong to the logic. Thus, the semantics of (extensional) type theory naturally lies in a category with appropriate structure, while the semantics of logic over that type theory naturally lies in some indexed poset over that category. However, we commonly take this indexed poset to consist of the subobjects in the category in question, in which case additional “logical” structure on the category is required, for instance that it be a Heyting category.

In an elementary 1-topos, all of the “logical” structure is not usually included in the definition, because it comes for free once you have power objects. But object classifiers may not be as powerful as power objects in this respect, so for purposes of studying the internal logic (and not just the internal type theory) of an (,1)(\infty,1)-topos, it’s good to keep in mind both the type-theoretic structure and the logical structure, and in particular both the object classifier and the subobject classifier.

The type theory of an (,1)(\infty,1)-category

Amazingly, a variant of type theory that seems appropriate for interpretation in an (,1)(\infty,1)-category already exists, namely intensional type theory with identity types.

Intensional identity types in (,1)(\infty,1)-categories

The usual sort of type theory that one interprets in a 1-category is extensional type theory. To explain what this means, consider how the categorical structure of finite limits is represented in the type theory. On the one hand, we have product types A×BA\times B, which of course represent categorical products; thus to obtain finite limits it suffices to have equalizers. We can obtain these from identity types, which supply for each type AA and each pair of terms x,y:Ax,y:A, a dependent type Id A(x,y)Id_A(x,y), whose intended interpretation is that it is inhabited precisely when x=yx=y. In terms of 1-categorical semantics, it is natural to require that any two elements of Id A(x,y)Id_A(x,y) be equal, i.e. that Id A(x,y)Id_A(x,y) be essentially a truth value/subsingleton. Then if we have two terms x:Af(x):Bx:A\vdash f(x):B and x:Ag(x):Bx:A\vdash g(x):B representing morphisms f,g:ABf,g\colon A\to B, their equalizer is represented by the type Σ x:AId B(f(x),g(x))\Sigma_{x:A} Id_B(f(x),g(x)).

However, for semantics in an (,1)(\infty,1)-category, it makes sense to use the same identity types, but now interpreted as a path space. Now it will no longer be true that Id A(x,y)Id_A(x,y) is a subsingleton, since two points can be connected by more than one path, so we must drop that axiom. This intensional type theory has been widely studied by type-theorists, although from a different point of view: assuming the propositions as types approach, Id A(x,y)Id_A(x,y) should be the type of proofs or reasons why x=yx=y, which can also of course have many different elements.

Thus we suspect that intensional type theory may be a natural sort of type theory to have semantics in an (,1)(\infty,1)-category. According to the general framework of syntax/semantics, we would hope that

  1. From any intensional type theory, we can construct a syntactic (,1)(\infty,1)-category, and
  2. In any (,1)(\infty,1)-category, we can model an intensional type theory.

Some work in both of these directions has been done. On the one hand, it is known that in any intensional type theory with identity types, for any type AA the globular set (or more accurately globular context) given by

AId AId Id A A \leftleftarrows Id_A \leftleftarrows Id_{Id_A} \leftleftarrows \dots

has the structure of a Batanin ∞-groupoid. This can be found in:

Moreover, the syntactic category of such a theory carries a natural weak factorization system, the identity type weak factorization system?. However, there seems as yet to be no published work constructing a full syntactic (,1)(\infty,1)-category.

On the other hand, it is known that in any nice enough model category (and in fact, in any category with a nice enough weak factorization system), one can model intensional type theory. This is studied in

Vladimir Voevodsky has also studied the particular model of intensional type theory in simplicial sets, which he calls the univalent model; see his website.

Additional axioms

Although intensional type theory has semantics in (,1)(\infty,1)-categories, one can naturally expect that these models will all satisfy additional axioms. This is especially true if we want to add additional structure to our (,1)(\infty,1)-categories.

  • Exponential (and dependent product) types can probably be modeled by (locally) cartesian closed (,1)(\infty,1)-categories. However, although exponentials in an (,1)(\infty,1)-category are not strictly extensional the way they are in a 1-category, they are still extensional “up to coherent higher homotopies,” which (unlike the case for identity types) is seemingly not guaranteed by the type-theoretic structure. Thus, there may be an \infty-extensionality axiom to be added.

  • Disjoint sum types may be expected to correspond to coproducts in an (,1)(\infty,1)-category.

  • The usual notions of quotient type make little sense without extensional identity types. In the 1-categorical world, quotient types correspond to exact categories, while the appropriate notion of “exactness” for an (,1)(\infty,1)-category deals with groupoid objects in an (∞,1)-category. It remains to be seen how to phrase a corresponding axiom in the type theory.

  • The object classifier in an (,1)(\infty,1)-topos does in fact correspond to a well-known concept in type theory, namely that of a universe such as the type TypeType. However, as a universe, the object classifier in an (,1)(\infty,1)-topos has the special property that the paths between two types AA and BB as elements of TypeType (that is, the path space Id Type(A,B)Id_{Type}(A,B)) is equivalent to the space of equivalences between AA and BB as types (an appropriate subspace of the exponential B AB^A). A type-theoretic axiom asserting this equivalence was introduced by Voevodsky under the name of the equivalence axiom.

Logic over type theory in an (,1)(\infty,1)-category

Now when we go to add logic to the type theory of an (,1)(\infty,1)-category, it seems natural by analogy that it will deal with subobjects, i.e. with monomorphisms in an (∞,1)-category. That is, a proposition φ(x)\varphi(x) with a variable x:Ax:A will be interpreted by a monomorphism [φ][A][\varphi] \rightarrowtail [A]. Just as in the internal logic of a 1-category and of a 2-category, in order to interpret the logical connectives and quantifiers we will then need suitable structure on the posets of subobjects in our (,1)(\infty,1)-category. It is naturally to be expected that any (,1)(\infty,1)-topos will have this necessary structure.

Again, the requisite type theory more or less exists, namely intensional type theory together with a sort of propositions that can depend on types. In fact, this type theory is very closely related to the calculus of constructions used in the proof assistant Coq, making Coq a very convenient place to play around with the type theory that ought to be valid in an (,1)(\infty,1)-topos. In particular, Voevodsky has written out a Coq script up to the statement of his equivalence axiom, to be found on his website.

The problem of finiteness

In describing the internal type theory and logic of an (,1)(\infty,1)-category we encounter the problem that many structures in an (,1)(\infty,1)-category require a (countably) infinite amount of data to describe. For instance, when looking for a way to state the “exactness” property one has to say what is meant by a groupoid object, but since this really means a “coherent” or “A A_\infty” groupoid object, it involves an infinite amount of data. By contrast, the most common type theories are purely finitary systems.

There is the one amazing fact that the entire complicated infinitary structure of a Batanin ω\omega-groupoid can be recovered from the simple finitary rules of identity types. It is not clear, however, whether we can expect this happy occurrence to continue. We might have to bite the bullet and work with an infinitary type theory, i.e. one allowing derivation rules taking as input an infinite list of hypotheses. In fact, this is almost certainly what we will need if we want a good notion of a geometric theory in the (,1)(\infty,1)-case, since that involves infinitary logic even in the 1-categorical case.

However, such a type theory would obviously no longer have “computational content” and couldn’t be modeled in a proof assistant such as Coq, and also wouldn’t provide a fully “elementary,” i.e. finitary first-order, theory such as ETCS provides in the 1-categorical case. It might be helpful to note that infinitary structures can at least sometimes be finitarily described using inductive types and/or coinductive types, but it is not clear yet whether this is useful in the (,1)(\infty,1)-categorical context.


Internal logic in Grpd\infty Grpd

The archetypical (∞,1)-topos is ∞Grpd. This is to be thought of as the (∞,1)-categorification of the archetypical 1-topos Set.

At internal logic - in Set is a step-by-step discussion of how ordinary logic is recovered from the point of view of the internal logic of a topos 𝒯\mathcal{T} when choosing 𝒯:=Set\mathcal{T} := Set.

Here we look at the (,1)(\infty,1)-categorical analog of that discussion, step-by-step, now everything internal to ∞Grpd.



Last revised on June 17, 2022 at 14:29:32. See the history of this page for a list of all contributions to it.