Homotopy Type Theory
Homotopy Type System (Rev #9, changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

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.



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

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, even if we restrict to the fibrant types. It is unclear whether or not this is true; Voevodsky’s conjecture above would imply that model invariance holds if it holds for MLTT.

The following argument, however, shows that model invariance 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)or(¬PR))\prod_{P,Q,R:sProp} (\neg P \to (Q \vee R)) \to ((\neg P \to Q) or (\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.

Revision on October 8, 2014 at 14:51:38 by Bas Spitters. See the history of this page for a list of all contributions to it.