nLab Homotopy Type System

Contents

Context

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
propositionsetobjecttype
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

semantics

Deduction and Induction

Constructivism, Realizability, Computability

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

Proposed by Vladimir Voevodsky, Homotopy Type System (HTS) is a type theory with two equality types, an “exact” or “strict” one which satisfies a reflection rule?, and a “path” or “homotopical” one which does not. It also distinguishes between “fibrant” and “non-fibrant” types: the path type only eliminates into fibrant types.

Specification

Implementation

Remarks and Variations

Points that are homotopic but not strictly equal

Let II be the type of pointed fibrant types that are merely equal to BoolBool, i.e.

I= (A:U F)A.I = \sum_{(A:U_F)} A.

Define zero,one:Izero,one:I by

zero=(Bool,false)zero = (Bool,false)
one=(Bool,true)one = (Bool,true)

Then we have Paths(zero,one)Paths(zero,one), since by univalence we have a p:Paths(Bool,Bool)p:Paths(Bool,Bool) such that p *(false)=truep_*(false) = true.

However, if e:Id(zero,one)e:Id(zero,one), then by apdapd for strict equality, we have Id(q *(false),true)Id(q_*(false),true), where qq is the image of ee under the map proj 1:IU Fproj_1:I \to U_F. But all strict equalities are equal to reflexivity, so Id(q *(false),false)Id(q_*(false),false), and thus Id(false,true)Id(false,true), a contradiction.

Therefore, the fibrant type II contains two points zero,onezero,one such that Paths(zero,one)Paths(zero,one), but ¬Id(zero,one)\neg Id(zero,one) (both provable inside the theory).

The universe of non-fibrant types

The universe UU of non-fibrant types is itself fibrant. Moreover, in standard models (such as the simplicial set model, and other model-category-theoretic models) it is contractible (in the usual sense of homotopy type theory, with respect to the PathsPaths identity type).

The reason that the universe of non-fibrant types (type families) is contractible is that if you have a type II with two objects ab:Ia b : I and an object e:Paths Iabe : Paths_I a b such that for any two types A,BA, B there is a function (AB)I(A \coprod B ) \to I whose strict fiber over aa is isomorphic to AA and strict fiber over bb is isomorphic to BB then the family of fibers of this function gives a map from II to the universe of all types which, when applied to ee, gives an isomorphism in this universe from AA to BB. This is sufficient to create a path from a type which is isomorphic to empty to a type which is isomorphic to unit and therefore a path from 0 to 1 in nat.

It is not provably contractible in the theory, since we can take its coproduct with pretty much any other type and still have a universe of non-fibrant types. However, it is “almost” contractible by the following argument. Let AA and BB be arbitrary types, and let I,zero,oneI,zero,one be as defined above. Define f:A+BIf:A+B \to I by f(inl(a))=zerof(inl(a)) = zero and f(inr(b))=onef(inr(b)) = one, and define P:IU SP:I\to U_S (the universe of non-fibrant types) by

P(i)= x:A+BId(f(x),i).P(i) = \sum_{x:A+B} Id(f(x),i).

In other words, P(i)P(i) is the fiber of ff over ii, computed using strict equality. It’s straightforward to show that P(zero)AP(zero) \cong A and P(one)BP(one)\cong B. However, since II and U SU_S are both fibrant, we can apply PP to the path Paths(zero,one)Paths(zero,one) to obtain a Paths(P(zero),P(one))Paths(P(zero),P(one)). This is not the same as a path Paths(A,B)Paths(A,B), of course.

Fibrant replacement

It is natural to wonder whether we can have a “fibrant replacement” type former which makes non-fibrant types into fibrant ones. However, surprisingly, this is actually inconsistent, essentially because it cannot be made to respect substitution.

Suppose we had a type forming rule

ΓATypeΓRAFib\frac{\Gamma \vdash A \, Type}{\Gamma \vdash R A \, Fib}

with introduction rule

Γa:AΓra:RA\frac{\Gamma \vdash a:A}{\Gamma \vdash r a : R A}

and elimination rule

Γ,(x:RA)TFibΓ,(a:A)t:T[x:=ra]Γ,(x:RA)Relim(a.t,x):T.\frac{\Gamma,(x:R A) \vdash T\, Fib\qquad \Gamma,(a:A) \vdash t:T[x:=r a]}{\Gamma,(x:R A) \vdash Relim(a.t,x) : T}.

Let A=0A=0 and B=1B=1, and let P:IU SP:I\to U_S be defined as above, so that P(zero)0P(zero) \cong 0 and P(one)1P(one)\cong 1. Now consider

(x:I)R(P(x))Fib. (x:I) \vdash R(P(x))\,Fib.

Since this is a fibrant type family over a fibrant type, we can transport the element r():R(P(one))r(\star) : R(P(one)) along the known Paths(zero,one)Paths(zero,one) to obtain an element of R(P(zero))R(P(zero)). However, by RelimRelim, we can define a map R(P(zero))0R(P(zero))\to 0 by defining a map P(zero)0P(zero)\to 0, which we have. Thus, we obtain an element of 00.

It does, however, seem to be possible to allow fibrant replacement of types in the empty context. In other words, we could have a rule

ATypeRAFib\frac{\vdash A \, Type}{\vdash R A \, Fib}

and so on. Of course, this does not fit very well in the usual framework of type theory.

Fibrancy of inductive types

Mike Shulman has argued that rather than assuming the natural numbers type to be fibrant and yet able to eliminate into non-fibrant types, there should be two natural numbers types: a fibrant one which can only eliminate into fibrant types, and a non-fibrant one which can eliminate into all types. The same applies to other positive inductive types such as coproducts (even coproducts of fibrant types) and the empty type.

This is because while these types in simplicial sets happens to be fibrant, that is not the case in other categorical models. It may also pose similar problems for constructing new models of HTS out of old ones.

Semisimplicial types

Vladimir Voevodsky claims that HTS allows a definition of semisimplicial types and other infinite objects, in which diagrams of types commute strictly using the exact equality. See the comments in the file:

Voevodsky’s conjecture

Voevodsky has conjectured that any fibrant type definable in HTS is equivalent to one definable in MLTT?, i.e. without using the strict equality.

Model invariance

The model invariance problem seems more likely to fail for HTS than for theories that do not include strict equality. In other words, distinct model categories presenting the same (,1)(\infty,1)-topos might have different “internal languages” according to HTS. This can obviously happen if by “internal language” we include the non-fibrant types, but if we restrict to the fibrant types the answer is unclear. It may be related to Voevodsky’s conjecture above.

The following argument, however, shows that model invariance (even for fibrant types) definitely fails if we include fibrant replacement (of types in the empty context), and split inductive types into fibrant and non-fibrant versions (or simply don’t include inductive types in the system).

Let EE be the poset with four objects a,b,c,da,b,c,d such that d<ad\lt a, d<bd\lt b, and d<cd\lt c are the only nonidentity relations; thus an EE-diagram is four objects X aX_a, X bX_b, X cX_c, X dX_d with maps X dX aX_d \to X_a, X dX bX_d \to X_b, and X dX cX_d \to X_c. Since EE is an inverse category, there is a Reedy model structure on sSet EsSet^E in which the cofibrations are levelwise monomorphisms, the weak equivalences are levelwise weak equivalences, and the fibrant objects are diagrams such that X aX_a, X bX_b, and X cX_c are fibrant and the induced map X d(X a×X b×X c)X_d \to (X_a \times X_b \times X_c) is a fibration. Moreover, this model has univalent universes induced from those of sSetsSet: if UU is a univalent universe in sSetsSet, then VV is a univalent universe in sSet EsSet^E, where V a=V b=V c=UV_a = V_b = V_c = U, and the fiber of V dV_d over (A,B,C)(A,B,C) is the type ABCUA \to B \to C \to U.

Now we can localize this Reedy model structure at the maps 0a0\to a, 0b0\to b, and 0c0\to c, where aa, bb, and cc denote the corresponding representables. A local object is a fibrant object such that X aX_a, X bX_b, and X cX_c are contractible, and the local weak equivalences are just the maps that induce a weak equivalence on dd-components. In particular, the homotopy category of the localized model structure is equivalent to that of sSetsSet. Moreover, locality and localization (of fibrant objects) can be represented internally as a subobject and an endomorphism, respectively, of the universe VV. Because localization is left exact, the subuniverse of local objects is itself local, and thus provides a univalent universe for the localized model structure.

In conclusion, we have two model structures, one on sSetsSet and one on sSet EsSet^E, which both model homotopy type theory with univalent universes, and have equivalent homotopy categories. Both model HTS as well, although their inductive types come in fibrant and non-fibrant versions.

Now, inside HTS, define a (non-fibrant) type YY to be a “strict hprop” if (x,y:Y)Id(x,y)\prod_{(x,y:Y)} Id(x,y). Write sPropsProp for the subtype of the universe of non-fibrant types determined by the strict hprops. Consider the following type

P,Q,R:sProp(¬P(QR))((¬PQ)(¬PR))\prod_{P,Q,R:sProp} (\neg P \to (Q \vee R)) \to ((\neg P \to Q) \vee (\neg P \to R))

Call this type KP (for Kreisel-Putnam). Note that “false” and “or” for strict hprops can be defined impredicatively by quantification over sPropsProp.

For semantics of HTS in a model category whose underlying category is a topos, the type sPropsProp will be interpreted by the subobject classifier of that topos (independently of what the model structure might look like). Thus, KP will be interpreted by the assertion, in the internal language of that topos (again independently of the model structure), that the Kreisel-Putnam axiom holds.

Now as pointed out by Francois Dorais, the Kreisel-Putnam axiom holds in the internal logic of (the 1-topos) sSetsSet; thus the interpretation of KP there is globally inhabited. However, the Kreisel-Putnam axiom does not hold in the internal logic of (the 1-topos) sSet EsSet^E. For this it suffices to exhibit subterminal objects P,Q,RP,Q,R such that (¬P(QR))(\neg P \to (Q \vee R)) is not contained in ((¬PQ)(¬PR))((\neg P \to Q) \vee (\neg P \to R)). Let P=aP = a, Q=bQ = b, and R=cR = c. Then (¬P)=(QR)={b,c}(\neg P) = (Q \vee R) = \{b,c\}, so that (¬P(QR))=1={a,b,c,d}(\neg P \to (Q \vee R)) = 1 = \{a,b,c,d\}, but (¬PQ)={a,b}(\neg P \to Q) = \{a,b\} and (¬PR)={a,c}(\neg P \to R) = \{a,c\}, so that ((¬PQ)(¬PR))={a,b,c}((\neg P \to Q) \vee (\neg P \to R)) = \{a,b,c\}. Thus, the interpretation of KP in sSet EsSet^E is not globally inhabited.

It follows that R(KP)R(KP) is a fibrant type which is inhabited in the model in sSetsSet, but not in the model in sSet EsSet^E.

See also

References

Last revised on July 13, 2023 at 14:42:35. See the history of this page for a list of all contributions to it.