Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

March 24, 2011

Homotopy Type Theory, III

Posted by Mike Shulman

It’s a dangerous business making promises about what will happen “next time” when I don’t have “next time” written yet. I said last time that I intended to talk about the univalence axiom next, but then I realized there is more I want to say about equivalences first, and perhaps functional extensionality.

But before I get into that, I’d like to mention that Steve Awodey has written a very nice post about intensional type theory and its relation to homotopy type theory from an intensional type theorists’ point of view; read it at the HoTT blog!

Now, recall that the proposition (that is, the (-1)-type) “f:XYf\colon X\to Y is an equivalence” was defined as

IsEquiv(f)Π yYIsContr(Fiber(f,y)) IsEquiv(f) \coloneqq \Pi_{y\in Y} IsContr( Fiber(f,y))

where Fiber(f,y)Σ xXPaths Y(f(x),y)Fiber(f,y) \coloneqq \Sigma_{x\in X} Paths_Y(f(x),y). I claimed that this is equivalent to the following type (which I didn’t write down in gory detail before):

IsAdjointEquiv(f)Σ g:YXΣ pΠ xXPaths X(g(f(x)),x)Σ qΠ yYPaths Y(f(g(y)),y)Π xXPaths Paths Y(f(g(f(x))),f(x))(f(p(x)),q(f(x))). IsAdjointEquiv(f) \coloneqq \Sigma_{g\colon Y\to X} \Sigma_{p\in \Pi_{x\in X} Paths_X(g(f(x)),x)} \Sigma_{q\in \Pi_{y\in Y} Paths_Y(f(g(y)),y)} \Pi_{x\in X} Paths_{Paths_Y(f(g(f(x))),f(x))}(f(p(x)),q(f(x))).

Ugh! If you unravel this, it means that a point of IsAdjointEquiv(f)IsAdjointEquiv(f) consists of:

  1. a map g:YXg\colon Y\to X,
  2. a “homotopy” p:gf1 Xp\colon g\circ f\simeq 1_X,
  3. a “homotopy” q:fg1 Yq\colon f\circ g\simeq 1_Y, and
  4. a “higher homotopy” t:f(p)q ft\colon f(p) \simeq q_f.

If all of our types were 1-types, i.e. groupoids, then this would be exactly an adjoint equivalence of groupoids: the two homotopies pp and qq are the unit and counit, and the higher homotopy asserts one triangle identity. The other triangle identity then follows; see the nLab page.

I didn’t really say anything about why these types should be equivalent, though. Suppose that we have a point of IsEquiv(f)IsEquiv(f). This consists of, for every yYy\in Y, a point of IsContr(Fiber(f,y))IsContr( Fiber(f,y)). The latter consists of a point of Fiber(f,y)Fiber(f,y) together with a contraction to that point. Now a point of Fiber(f,y)Fiber(f,y) consists of a point of XX along with a path from ff of that point to yy. Call this point g(y)g(y) and the path q yPaths Y(f(g(y)),y)q_y\in Paths_Y(f(g(y)),y). In this way we extract our map gg and homotopy qq.

What remains in the data is the contraction of Fiber(f,y)Fiber(f,y) to (g(y),q y)(g(y),q_y). This consists of, for every point (x,r:f(x)y)(x,r\colon f(x) \simeq y) of Fiber(f,y)Fiber(f,y), a path from (x,r)(x,r) to (g(y),q y)(g(y),q_y). Now Fiber(f,y)Fiber(f,y) is the total space of a “fibration” (i.e. dependent type) over XX, whose fiber over xXx\in X is Paths Y(f(x),y)Paths_Y(f(x),y)—and so a path (x,r)(g(y),q y)(x,r)\simeq (g(y),q_y) in Fiber(f,y)Fiber(f,y) is determined by a path a:xg(y)a\colon x\simeq g(y) in the base space XX, together with a path bb in the fiber Paths Y(f(g(y)),y)Paths_Y(f(g(y)),y) from a *(r)a_\ast(r) to q yq_y, where a *a_\ast denotes fiber transport along the path aa. But fiber transport in the fibration of paths is just composition of paths, so the latter is a homotopy from rf(a 1)r\circ f(a^{-1}) to q yq_y.

Now consider, for any xXx\in X, the point (x,1 f(x))Fiber(f,f(x))(x,1_{f(x)})\in Fiber(f,f(x)). Then the path aa above can be called p x 1:xg(f(x))p_x^{-1}\colon x \simeq g(f(x)), and bb goes from 1 f(x)f(p x)f(p x)1_{f(x)} \circ f(p_x) \simeq f(p_x) to q f(x)q_{f(x)}. So we obtain exactly the data of a point of IsAdjointEquiv(f)IsAdjointEquiv(f).

Conversely, the data of gg and qq in a point of IsAdjointEquiv(f)IsAdjointEquiv(f) is exactly what we need to specify, for every yYy\in Y, a point of Fiber(f,y)Fiber(f,y) (which is to say, a point of Π yYFiber(f,y)\Pi_{y\in Y} Fiber(f,y)). For the rest, given any (x,r)(x,r) in Fiber(f,y)Fiber(f,y), we can take aa to be g(r)p x 1g(r) \circ p_x^{-1}, and the remaining homotopy to be rf(p xg(r 1))rf(p x)f(g(r 1))trq f(x)f(g(r 1))q yf(g(r))f(g(r 1))q y. r \circ f(p_x \circ g(r^{-1})) \simeq r\circ f(p_x) \circ f(g(r^{-1})) \overset{t}{\simeq} r \circ q_{f(x)} \circ f(g(r^{-1})) \simeq q_{y} \circ f(g(r)) \circ f(g(r^{-1})) \simeq q_{y}.

This gives us maps in both directions between IsEquiv(f)IsEquiv(f) and IsAdjointEquiv(f)IsAdjointEquiv(f). (Note that because all the above manipulations are completely formulaic, they formalize directly into type-theoretic constructions. I’m sure of this, because I’ve coded both of these maps in Coq, using Andrej Bauer’s convenient “tactics”—maybe I’ll get around to talking about Coq in a later post. In particular, operations such as composing and inverting paths, and acting on them by functions, are easily definable in terms of the rules for identity types that I mentioned in the first post.)

Thus, if either of the two types above is inhabited, so is the other. Ideally, we’d like them to actually be equivalent. Since IsEquiv(f)IsEquiv(f) is a (-1)-type, if IsAdjointEquiv(f)IsAdjointEquiv(f) were also a (-1)-type, having morphisms in both directions would be enough for them to be equivalent. Or we could also try to enrich the above two maps into an (adjoint) equivalence, which would then imply that IsAdjointEquiv(f)IsAdjointEquiv(f) is a (-1)-type. I haven’t managed to get either of these approaches to work in Coq yet, but I believe that it should be true. (We will need to use functional extensionality, since the points of these two types contain functions.)

Now recall also that I disparaged the naive notion of “homotopy equivalence” which lacks the higher homotopy tt, as not giving rise to a (-1)-type. If written out explicitly, this type would be

IncoherentEquiv(f)Σ g:YX(Π xXPaths X(g(f(x)),x))×(Π yYPaths Y(f(g(y)),y)) IncoherentEquiv(f) \coloneqq \Sigma_{g\colon Y\to X}\; ( \Pi_{x\in X} Paths_X(g(f(x)),x) ) \; \times \; ( \Pi_{y\in Y} Paths_Y(f(g(y)),y) )

However, perhaps I didn’t emphasize enough that as soon as f:XYf\colon X\to Y admits some choice of “homotopy equivalence data” (i.e. IncoherentEquiv(f)IncoherentEquiv(f) is inhabited) then ff is necessarily an equivalence in either of the above “coherent senses.” In fact, we can construct a map IncoherentEquiv(f)IsAdjointEquiv(f)IncoherentEquiv(f) \to IsAdjointEquiv(f) by copying the usual 2-categorical proof that any non-adjoint equivalence can be improved to an adjoint equivalence (by changing one of the natural isomorphisms). See the nLab page for a string diagram proof. Of course, in practice, this is often a convenient way to prove that a given map is an equivalence.


I also neglected to mention that Voevodsky currently refers to these equivalence as weak equivalences. I don’t, because as you can see there is nothing “weak” about them. Usually “weak” is prefixed to maps that we want to think of as equivalences, but which don’t necessarily admit inverses (even up to homotopy). But these equivalences do have homotopy inverses. (The term “h-isomorphism” was also proposed at Oberwolfach, but I prefer simply “equivalence.”)

One might ask, though, is there a notion of weak equivalence in homotopy type theory? In classical homotopy theory, we define a “weak homotopy equivalence” to be one inducing an isomorphism on all homotopy groups. Can we define homotopy groups in homotopy type theory?

We definitely have a notion of “based loop space” (or rather “based loop type”), namely Ω xXPaths X(x,x).\Omega_x X \coloneqq Paths_X(x,x). So if we had an operation “π 0\pi_0” or “τ 0\tau_{\le 0}” which reflects types into sets (i.e. 0-types), then we could define a set π n(X,x)π 0(Ω x nX)\pi_n(X,x) \coloneqq \pi_0 (\Omega_x^n X) for any type XX. (This is the internal-language version of categorical homotopy groups in an (,1)(\infty,1)-topos.) And of course, when restricted to sets, the above notion of equivalence for types can be regarded as the familiar notion of isomorphism (= bijection). So we could define a “weak equivalence” to be a map inducing an isomorphism on π n\pi_n, for all nn and all basepoints.

The quantifier “for all basepoints” means that π n\pi_n should really be not just a single set, but a set indexed by XX. And the quantifer “for all nn” here could be either in the metatheory or in the theory itself. But the more important point is that we shouldn’t expect to prove in homotopy type theory that every weak equivalence, in this sense, is an actual equivalence. In other words, “Whitehead’s theorem” should not be provable.

In fact, the fragment of the theory that I’ve described so far has a model in topological spaces—arbitrary topological spaces, not necessarily even of the homotopy type of CW complexes. (Probably; see this comment.) If this model has a π 0\pi_0, then Whitehead’s theorem will probably fail as usual for spaces that aren’t of the homotopy type of a CW complex. This model might lead you to think that the failure of Whitehead’s theorem is a bad thing: the (,1)(\infty,1)-category of all topological spaces is a pretty weird beast by (,1)(\infty,1)-categorical standards, although it contains as a full sub-(,1)(\infty,1)-category the prototypical (,1)(\infty,1)-category of \infty-groupoids (modeled by CW complexes).

But actually, there are also important, interesting, and otherwise well-behaved “homotopy theories” in which Whitehead’s theorem fails. I’m thinking of non-hypercomplete (,1)(\infty,1)-topoi, and this isn’t really the time to talk more about them, except to say that they include many (,1)(\infty,1)-topoi of interest, including (in general) \infty-sheaves on topological spaces. Moreover, as (,1)(\infty,1)-topoi, they have all the other good properties we might ask of an (,1)(\infty,1)-category.

It took me a little while to come to terms with this. Now I think we can think of Whitehead’s theorem as a “classicality” axiom which can fail in (,1)(\infty,1)-topoi, akin to the law of excluded middle and the axiom of choice (which can already fail in 1-topoi). It’s curious in that we don’t notice it until we go all the way to \infty. But once I got over being sad about losing Whitehead’s theorem, I got excited that the \infty-categorical world has displayed to us this new structure, which was totally invisible to the nn-categorical world for all finite nn.

Put another way, Whitehead’s theorem should be regarded as a foundational axiom of mathematics, but one which only a “natively homotopical” foundational system is subtle enough to perceive (and in particular, to allow to be violated). If we insist on building \infty-groupoids out of sets, then we will automatically be forced to accept Whitehead’s theorem; but if instead we define sets as particular \infty-groupoids, then we are allowed to explore a world where Whitehead’s theorem may fail.

Posted at March 24, 2011 10:44 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2375

26 Comments & 2 Trackbacks

Re: Homotopy Type Theory, III

another great posting full of things to think about and discuss! First, though, with respect to the definition of weak equivalence: without function extensionality (FE), there is of course a difference between Πx:XId X(g(f(x)),x)\Pi x:X\, \mathrm{Id}_{X}(g(f(x)),x) and Id X X(gf,1 X)\mathrm{Id}_{X^X}(g\circ f,1_X). So although you used the former (weaker) notion in the writing out the type IsAdjointEquiv(f), in the “unravelled” explanation that follows you said “a “homotopy” p:gf1 Xp:g\circ f \simeq 1_X” – which is maybe better formalized in the stronger way.

So, without FE there are indeed weak and strong notions of equivalence: roughly “pointwise equivalence”, and “intensional isomorphism”. Of course, Univalence collapses the difference.

Posted by: Steve Awodey on March 25, 2011 12:39 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

That’s why I put “homotopy” in quotes. (-:

I’m not too bothered about that difference except at a technical level, though, because it seems to me that homotopy type theory, regarded as an \infty-groupoidal foundation, doesn’t really work without FE. For instance, without FE, types like IsContrIsContr and IsPropIsProp and IsEquivIsEquiv can’t even be shown to be (-1)-types.

In fact, here’s a question: in the absence of FE, is there any way to construct a path between two functions which aren’t definitionally equal? I mean, it might happen in some model that two unequal functions are connected by a path, but could we ever prove it to be so in type theory without knowing that the functions are definitionally equal? It seems to me like the answer should be no, from intuitive semantic considerations, but I could be way off.

But if that’s the case, then I think in the absence of FE it would be perfectly reasonable to say just “isomorphism” for the stronger notion, leaving just plain “equivalence” for the weaker one.

Posted by: Mike Shulman on March 25, 2011 2:48 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

In fact, here’s a question: in the absence of FE, is there any way to construct a path between two functions which aren’t definitionally equal?

The answer is yes, but not in many cases you’d probably care about. Here is an example:

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero  + n = n
suc m + n = suc (m + n)

data Path (A : Set) (x : A) : A -> Set where
  refl : Path A x x

J : {A : Set} {x : A} (P : (y : A) -> Path A x y -> Set)
  -> {y : A} -> (p : Path A x y) -> P x refl -> P y p
J P refl Pxr = Pxr

cong : {A B : Set} -> (f : A -> B) -> {x y : A}
     -> Path A x y -> Path B (f x) (f y)
cong f p = J (\z _ -> Path _ (f _) (f z)) p refl

lemma : (n : Nat) -> Path Nat (n + zero) n
lemma zero    = refl
lemma (suc n) = cong suc (lemma n)

path : (n : Nat) -> Path (Nat -> Nat) (\_ -> n + zero) (\_ -> n)
{- path n = refl -- error -}
path n = cong (\n _ -> n) (lemma n)

so, const (n + 0) is propositionally but not definitionally equal to const n for all n by induction on n.

Of course, for any particular (closed term) n, definitional equality should hold, so this may or may not be what you want.

Posted by: Dan Doel on March 25, 2011 6:19 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Interesting, thanks! Is there any characterization of the sorts of functions for which one can do that? Can it ever happen for functions defined in the empty context?

Posted by: Mike Shulman on March 25, 2011 7:08 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

I believe all the functions for which you can do this are of the form f <v> : A -> B, where <v> is a sequence of terms. If we can have two sequences <v> and <v'> where at least one pair of terms is propositionally equal but not definitionally equal, then it may also be the case that f <v> is propositionally equal but not definitionally equal to f <v'>. This is of course because function application provably respects propositional equality.

As for when this can happen… Assuming the above is the only way to produce function terms that are propositionally but not definitionally equal, the situations reduce to those for non-function terms. And I think only open such terms can be propositionally but not definitionally equal in normal intuitionistic type theory. So no two functions (or terms in general) definable in the empty context satisfy the condition. It’s possible I’m overlooking something, though.

Posted by: Dan Doel on March 25, 2011 12:57 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

This is actually not quite true as you can prove things like

fun x => (x + 0) = fun x => x

In Coq. Though this may not be a counter-example to what you propose, as it can be “eta-expanded” to the form which you describe.

Posted by: cody on March 28, 2011 5:02 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

How? I’ve never been able to figure out how to prove that in Agda. As far as I know, it requires extensionality for functions.

Posted by: Dan Doel on March 29, 2011 2:22 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

You can’t prove it in Coq without axioms. (Coq’s plus recurs on the first argument, just like in Agda.)

Posted by: Neel Krishnaswami on March 29, 2011 8:56 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

That seems plausible, at least. Thanks!

Posted by: Mike Shulman on March 25, 2011 6:23 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Actually, I can defend my use of the word “homotopy” better than that. In abstract homotopy theory in a model category (or category with a WFS, or category of fibrant objects) we have two types of “homotopy”. Left homotopies are maps Cyl(X)YCyl(X)\to Y out of a cylinder object; right homotopies are maps XPath(Y)X\to Path(Y) into a path object. If the cylinder and path object are given by multiplying and exponentiating with an interval object, Cyl(X)=X×ICyl(X) = X\times I and Path(Y)=Y IPath(Y) = Y^I, then the two types of homotopies agree, and can also be identified with maps IY XI\to Y^X (paths between functions) if Y XY^X exists.

In homotopy type theory, we don’t have an interval object or a cylinder object (at least, not without additional axioms), but the identity types do give us a path object. So it makes sense to say that a “homotopy” between maps f,g:XYf,g\colon X\rightrightarrows Y is a map XPath(Y)X\to Path(Y) over (f,g)(f,g), which is to say a point of Π xXPaths Y(f(x),g(y))\Pi_{x\in X} Paths_Y(f(x),g(y)).

Posted by: Mike Shulman on March 25, 2011 6:44 AM | Permalink | PGP Sig | Reply to this

Re: Homotopy Type Theory, III

I agree: Path(Y)=Id Y\mathrm{Path}(Y) = \mathrm{Id}_Y classifies homotopies into YY. So without FE homotopy equivalence is a weaker notion than (propositional) isomorphism. Definitional isomorphism is even stronger, rarely occurs, and is less interesting. Univalence collapses homotopy equivalence and propositional isomorphism – which is a good thing.

Posted by: Steve Awodey on March 25, 2011 2:05 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Okay, so in pure intensional type theory I guess we actually have five notions of “sameness” for types:

  • Definitional equality: A=BA=B.
  • Propositional equality: a path pPaths Type(A,B)p\in Paths_{Type}(A,B).
  • Definitional isomorphism: A function f:ABf\colon A\to B so that there exists g:BAg\colon B\to A such that gf=1 Ag f = 1_A and fg=1 Bf g = 1_B definitionally.
  • Propositional isomorphism: a function f:ABf\colon A\to B so that there exists g:BAg\colon B\to A with paths (or equality proofs) pPaths AA(gf,1 A)p\in Paths_{A\to A}(g f, 1_A) and qPaths BB(fg,1 B)q\in Paths_{B\to B}(f g,1_B).
  • Homotopy equivalence: a function f:ABf\colon A\to B so that there exists g:BAg\colon B\to A with homotopies pΠ xAPaths A(g(f(x)),x)p\in \Pi_{x\in A} Paths_{A}(g(f(x)), x) and qΠ yBPaths B(f(g(y)),y)q\in \Pi_{y\in B} Paths_{B}(f(g(y)),y).

We have implications Propeq Defeq Propiso Htpyequiv Defiso \array{ && Prop eq \\ & \nearrow && \searrow \\ Def eq &&&& Prop iso & \to & Htpy equiv\\ & \searrow && \nearrow\\ && Def iso}

And

  • UIP collapses definitional and propositional isomorphism, and definitional and propositional equality,
  • Functional extensionality collapses propositional isomorphism and homotopy equivalence, and
  • Univalence collapses homotopy equivalence, propositional isomorphism, and propositional equality.
Posted by: Mike Shulman on March 25, 2011 7:56 PM | Permalink | PGP Sig | Reply to this

Re: Homotopy Type Theory, III

UIP collapses definitional and propositional isomorphism, and definitional and propositional equality

This doesn’t sound right. My example was Agda, which has K, but it there’s no way, to my knowledge, to use that to make constnconst \; n and const(n+0)const \; (n + 0) definitionallty equal.

Extensional type theory is, I think, defined by the collapsing of definitional and propositional equality (by adding an inference rule from propositional equality of two values to definitional equality thereof).

Posted by: Dan Doel on March 26, 2011 2:11 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

I guess I can never get this terminology right! I thought back here you told me I should say “UIP” instead of “extensional type theory”; now you seem to be saying the opposite. I must be confused.

Posted by: Mike Shulman on March 26, 2011 2:18 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

I think I said that I thought “unique identity proofs” was preferable to “extensional identity types.”

If we think merely about collapsing definitional and propositional equality with a rule like:

p:Id Axyx=y:A\frac{p : Id_A x y}{x = y : A}

Then it isn’t obvious to me that we have, on this basis alone:

id 1,id 2:Id Axyid 1=id 2:Id Axy\frac{id_1, id_2 : Id_A x y}{id_1 = id_2 : Id_A x y}

or similar.

So, I don’t think collapsing definitional/judgmental equality and propositional equality the way extensional type theory does necessitates identity proofs being unique. Many extensional type theories probably do take UIP as an additional axiom, but it is not necessary to the first rule above.

The collapse above is already enough to make type checking undecidable, too, I believe, because deciding T(v 1)=T(v 2)T(v_1) = T(v_2) requires deciding whether v 1v_1 is provably equal to v 2v_2 by induction, which doesn’t sound possible to me. And that’s before adding function extensionality.

Now, Agda (and OTT, I think) has unique identity proofs, but only up to propositional equality. It is equivalent to having an extra eliminator for equality:

K : (A : Type) (x : A) (P : Id A x x -> Type) (id : Id A x x) -> P refl -> P id
K A x P refl e = e

Which corresponds to adding an extra elimination and compute rule to regular intuitionistic type theory. But, this doesn’t mean that identity proofs become definitionally equal, just like squashing propositional and definitional equality together doesn’t imply that identity proofs are unique (although I’m more sure about the former).

(And the above is all you need for unrestricted dependent pattern matching. The desugaring uses K, not any definitional equality of identity proofs. Also, it’s at least a little surprising that this isn’t built-in. Id A x y is often looked at as being defined by induction, with the one constructor being refl : Id A x x. So it seems obvious that K is warranted as an induction principle of Id A x x, but it’s not derivable from J, and of course, this whole series is about models of type theory where K is wrong.)

And of course, my position in the first sentence of this post was based on the idea that “extensional identity type” suggested to me a propositional equality for which “propositional isomorphism” and “homotopy equivalence” were collapsed.

Does that clear things up?

Posted by: Dan Doel on March 26, 2011 3:52 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

extensional type theory includes both of the following rules:

p:Id(a,b)a=bp : \mathrm{Id}(a,b) \Rightarrow a=b p:Id(a,b)p=r(a)p : \mathrm{Id}(a,b) \Rightarrow p=r(a)

so in particular UIP follows.

Posted by: steve Awodey on March 26, 2011 1:41 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

in fact, if you’re talking about *adding* rules to the usual ones, then (as Peter Lumsdaine pointed out to me),

p:Id(a,b)a=bp:\mathrm{Id}(a,b) \Rightarrow a=b

implies

p:Id(a,b)p=r(a)p:\mathrm{Id}(a,b) \Rightarrow p=r(a)

using Id\mathrm{Id}-Elim. So in particular, UIP follows.

Posted by: steve Awodey on March 27, 2011 4:13 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Okay. I guess I see how that’d work. Since Id A x y leads to x = y,

P z p := Id (Id A x x) p refl

is a well defined predicate for z : A and p : Id A x z, and so J gets us p = refl (after lifting) on the conditions that p : Id A x y and refl : Id (Id A x x) refl refl, the second of which is trivial.

I’ll cop to not knowing a lot about extensional type theory. So, squashing definitional and propositional equality together implies uniqueness of identity proofs, but the converse isn’t true. At least, inasmuch as Agda has unique identity proofs, which is propositionally, but not definitionally.

Posted by: Dan Doel on March 27, 2011 5:38 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

I guess there is not universal agreement on what “extensional type theory” means. (-: I would prefer it to mean what Steve said.

Posted by: Mike Shulman on March 27, 2011 4:00 AM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Since you’re comparing isEquiv and isAdjointEquiv here, I hope you won’t mind my plugging a third alternative, which André Joyal suggested in Oberwolfach.  This was what he called “homotopy isomorphism” (I rather like that term), but for now let’s call it being a “two-sided equivalence”, isTwoSidedEquiv.

A left homotopy inverse for f:XYf : X \to Y is a function g:YXg : Y \to X, together with a homotopy gf1g\cdot f \rightsquigarrow 1, i.e. a function giving for each x:Xx:X a path g(f(x))xg(f(x)) \rightsquigarrow x.  A right homotopy inverse is defined analogously.

A two-sided equivalence structure on ff is just a choice of a left homotopy inverse, and of a right.

In gory syntax: for f:XYf \colon X \to Y,

RightHInv(f)Σ g:YX y:YPaths X(x,gfx).\text{RightHInv}(f) \coloneqq \Sigma_{g:Y \to X} \forall_{y:Y} \text{Paths}_X (x,gfx).

LeftHInv(f)Σ h:YX x:XPaths X(fhx,x).\text{LeftHInv}(f) \coloneqq \Sigma_{h:Y \to X} \forall_{x:X} \text{Paths}_X (fhx,x).

isTwoSidedEquiv(f)LeftInv(f)×RightInv(f).\text{isTwoSidedEquiv}(f) \coloneqq \text{LeftInv}(f) \times \text{RightInv}(f).

So it’s quite like the naïve type-theoretic definition of “isomorphism”, which would ask for a two-sided inverse, except this allows separate choices of left and right inverse; and that extra freedom makes it a proposition! (Just as the addition of a single triangle inequality does for isAdjointEquiv.)

I’ve often found this version a little nicer to work directly with than the others, since it doesn’t require any two-dimensional reasoning.

Posted by: Peter LeFanu Lumsdaine on March 25, 2011 9:07 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

O crikey, in trying to space my syntax nicely I’ve done something horrible to the TeX — at least, my three browsers all choke on it — and, in fact, also bungled my lefts and rights a bit. Take two:

LeftHInv(f):=Σ g:YX x:XPaths X(gfx,x).\text{LeftHInv}(f) := \Sigma_{g:Y \to X} \forall_{x:X} \text{Paths}_X (gfx,x).

RightHInv(f):=Σ h:YX y:YPaths X(fhy,y).\text{RightHInv}(f) := \Sigma_{h:Y \to X} \forall_{y:Y} \text{Paths}_X (fhy,y).

isTwoSidedEquiv(f):=textLeftHInv(f)×textRightHInv(f).\text{isTwoSidedEquiv}(f) := text{LeftHInv}(f) \times text{RightHInv}(f).

Or in Coq, which should be harder for parsers to mangle,

LeftHInv (f:X->Y) :=
    exists (g:Y->X), forall (x:X), Paths (g (f x)) x.
RightHInv (f:X->Y) :=
    exists (h:Y->X), forall (y:Y), Paths (f (h y)) y.
isTwoSidedEquiv (f:X->Y) :=
    LeftHInv f * RightHInv f.
Posted by: Peter LeFanu Lumsdaine on March 25, 2011 9:19 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Thanks! I forgot entirely about that one. I took the liberty of getting rid of the “Unknown characters” in your first comment; let me now try to make it a little more readable:

LeftHInv(f)Σ g:YX x:XPaths X(gfx,x).LeftHInv(f) \coloneqq \Sigma_{g\colon Y \to X} \forall_{x\colon X} Paths_X (g f x,x).

RightHInv(f)Σ h:YX y:YPaths X(fhy,y).RightHInv(f) \coloneqq \Sigma_{h\colon Y \to X} \forall_{y\colon Y} Paths_X (f h y,y).

isTwoSidedEquiv(f)LeftHInv(f)×RightHInv(f).isTwoSidedEquiv(f) \coloneqq LeftHInv(f) \;\times\; RightHInv(f).

Some iTex tips: unlike TeX, iTex interprets continuous letters as a single identifier if there is no space. So f g x produces fgxf g x while isEquiv(f) produces isEquiv(f)isEquiv(f) (no need for \text). You can use \; and \, for spacing, and \coloneqq for \coloneqq. To display formulas, you can use double dollar signs, as in plain TeX.

And if someone PGP-signs their comment, as I try to do whenever I’m writing a significant amount of iTex, you can click “PGP Sig” to view the source of their comment and see how they did the iTeX.

By the way, in case anyone gets confused by it, I think Peter’s “Coq version” is only “pseudo-Coq”; a version which actually compiles for me is

Definition LeftHInv {X Y} (f:X->Y) :=
  { g:Y->X & forall (x:X), paths (g (f x)) x }.
Definition RightHInv {X Y} (f:X->Y) :=
  { h:Y->X & forall (y:Y), paths (f (h y)) y }.
Definition isTwoSidedEquiv {X Y} (f:X->Y) :=
  (LeftHInv f * RightHInv f)%type.

Have you checked formally that this definition gives a proposition and equivalent to isEquiv (not that I have any doubt, but it would be nice to have)?

Posted by: Mike Shulman on March 25, 2011 10:07 PM | Permalink | PGP Sig | Reply to this

Re: Homotopy Type Theory, III

the following type (which I didn’t write down in gory detail before):

On my system the expression runs out of the blog’s boundaries. Here is what I can see (re-typeset using prods and sums and stackrels. what is it you do not like about them?).

YgX p xXPaths X(g(f(x))) q yYPaths Y(f(g(y))) xXPaths Paths Y(f(g(f(x))))[...] \sum_{Y \stackrel{g}{\to} X} \sum_{p \in \prod_{x \in X} Paths_X(g(f(x)))} \sum_{q \in \prod_{y \in Y} Paths_Y(f(g(y)))} \prod_{x \in X} Paths_{Paths_Y(f(g(f(x))))} [...]

You write about your proof:

I’m sure of this, because I’ve coded both of these maps in CoqCoq

Interesting, this is beginning to answer what I asked earlier, in the first thread: what can homotopy type theory do for homotopy theory, for homotopy theorists, for people not genuinely interested in type theory as such? It seems that the formal language allows to makes quite nontrivial statements in homotopy theory accessible to formal proof and formal proof checking. Before seeing this I would have guessed that the only statements about homotopy theory that you could code in practice in homotopy type theory are rather trivial. But this seems to be far from true.

At some point I would like to see the “code” that does this. How long is it?

Put another way, Whitehead’s theorem should be regarded as a foundational axiom of mathematics, but one which only a “natively homotopical” foundational system is subtle enough to perceive (and in particular, to allow to be violated). If we insist on building ∞-groupoids out of sets, then we will automatically be forced to accept Whitehead’s theorem; but if instead we define sets as particular ∞-groupoids, then we are allowed to explore a world where Whitehead’s theorem may fail.

Thanks for saying that. That’s good.

Posted by: Urs Schreiber on March 25, 2011 9:26 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Nils Anders Danielsson and Thierry Coquand proved:
the groupoid (π n X x) is commutative for n greater than or equal to 2.
The code is here.

Bas

Posted by: Bas Spitters on March 25, 2011 10:23 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Nice! I’ve added a link to the HoTT code page. Of course, that should really be (Ω n X x), as remarked here.

Posted by: Mike Shulman on March 25, 2011 10:56 PM | Permalink | Reply to this

Re: Homotopy Type Theory, III

Well, for one thing, in what you wrote I have a hard time seeing where the subscript on one Σ\Sigma ends and the subscript on the next one begins. I guess one could add extra spacing or parentheses. The last thing being summed over is

Π xXPaths Paths Y(f(g(f(x))),f(x))(f(p(x)),q(f(x))). \Pi_{x\in X} Paths_{Paths_Y(f(g(f(x))),f(x))}(f(p(x)),q(f(x))).

or perhaps more cleanly

Π xXPaths Paths Y(fgfx,fx)(fpx,qfx). \Pi_{x\in X} Paths_{Paths_Y(f g f x,f x)}(f p x ,q f x).

Of course, the subscript on PathsPaths can generally be inferred from the type of the arguments, so we can even just write Π xXPaths(fpx,qfx) \Pi_{x\in X} Paths(f p x ,q f x).

this is beginning to answer what I asked earlier, in the first thread

Excellent! I thought you were asking what new theorems in homotopy theory can we prove this way, and I didn’t have any answers yet. But I think it’s certainly true that existing theorems in homotopy theory are much more accessible to formal proof checking this way than they would be if you tried to build homotopy theory in Coq out of, say, simplicial sets.

At some point I would like to see the “code” that does this. How long is it?

I’ve been working based on Andrej Bauer’s implementation of the basics of homotopy type theory (a more or less direct line to the proof that univalence implies function extensionality), which can be found on github here.

My own fork can be found here. Currently the only change I made to the master branch is to make “weak equivalence” into “equivalence” everywhere, and then in a new branch called “adjoint-equivalences” (click on “Switch branches” to get to it) I’ve added a couple files which implement the two maps IsEquivIsAdjointEquivIsEquiv \to IsAdjointEquiv and IsAdjointEquivIsEquivIsAdjointEquiv \to IsEquiv, and also the adjointification map IncoherentEquivIsAdjointEquivIncoherentEquiv \to IsAdjointEquiv. The definitions of the three maps can be viewed here; the first two fit on a single screen each, while the third takes two screens. They do make use of a bunch of basic lemmas and “tactics” defined in the auxiliary files.

(To anyone reading this post in the distant future: it’s quite likely that the above links will no longer work; go to homotopytypetheory.org to find the most recent code.)

Posted by: Mike Shulman on March 25, 2011 10:44 PM | Permalink | PGP Sig | Reply to this
Read the post Homotopy Type Theory, IV
Weblog: The n-Category Café
Excerpt: Voevodsky's "univalence axiom" for universes in homotopy type theory, and the equivalent principle of "equivalence induction."
Tracked: April 7, 2011 5:21 AM
Read the post Homotopy Type Theory, VI
Weblog: The n-Category Café
Excerpt: A homotopical extension of the notion of "inductive definition" allows us to construct CW complexes and mimic other constructions from homotopy theory in type theory.
Tracked: April 25, 2011 7:56 AM

Post a New Comment