A basic fact in homotopy type theory is that homotopy equivalences are (coherent) equivalences. This is important because on the one hand, homotopy equivalences are the “correct” sort of equivalence, but on the other hand, for a function *f* the type of “homotopy equivalence data for *f*” is not an h-proposition. There are at least three definitions of “equivalence” which do give an h-proposition (assuming function extensionality) and are all equivalent:

- Voevodsky’s definition: all homotopy fibers are contractible.
- Adjoint equivalences: the two homotopies in a homotopy equivalence are compatible with one higher homotopy.
- h-isomorphisms: a homotopy section and a homotopy retraction.

Of these, the first two require *more* data than a homotopy equivalence. So in practice, when proving some map to be an equivalence, we want to be able to just show that it is a homotopy equivalence. Thus we need some way to recover that extra data if we are just given a homotopy equivalence.

(The third definition, h-isomorphisms, requires *less* data than a homotopy equivalence (the section and retraction don’t need to be the same, *a priori*), but as far as I know, showing that this definition gives an h-proposition is no easier than showing that every homotopy equivalence is a Voevodsky equivalence.)

Voevodsky’s proof that every homotopy equivalence is a (Voevodsky) equivalence shows that the homotopy fiber of *f* is a retract of a homotopy fiber of *gf*, while *gf* is an equivalence since it is homotopic to the identity. On the other hand, the proof currently in the HoTT repository uses a different approach motivated by higher category theory: we show that every homotopy equivalence can be “rectified” to an adjoint equivalence by changing one of the homotopies, and then from there we have essentially the data to make a Voevodsky equivalence after massaging it a bit.

I want to present a third approach to this fundamental theorem, which is motivated more by model category theory. Recall that a dependent type in type theory corresponds to a fibration in a model category. To say that each is contractible (with contraction varying continuously in *x*, as always) is equivalently to say that the projection *p* admits a (strict) section, *s* say, such that the composite is *fiberwise* homotopic to the identity. In this case we may say that *s* is a *deformation section* of *p*.

Now given any map , the dependent type represents the “mapping path fibration” which occurs in the (acyclic cofibration, fibration) factorization of *f*. (This is how Gambino and Garner constructed the identity type weak factorization system.) Therefore, to say that *f* is a Voevodsky equivalence is equivalently to say that the fibration part of this factorization has a deformation section, as above.

However, it’s easy to show that homotopy equivalences have the 2-out-of-3 property, and that every acyclic cofibration is a homotopy equivalence (in fact, it has a deformation retraction; Gambino and Garner showed this as well). Thus, if *f* is a homotopy equivalence, so is its mapping path fibration. Therefore, to show that any homotopy equivalence is a Voevodsky equivalence, it suffices to prove that a fibration which is a homotopy equivalence has a deformation section.

Using the path-lifting property of a fibration, it’s easy to modify a homotopy inverse to a fibration to become a strict section of it. Thus all that remains is to modify the one remaining homotopy to become fiberwise, which we can do by concatenating it with the inverse of . This is a degenerate case of “adjointification” when one of the homotopies is constant, but I think it is significantly simpler to understand than the general case. In particular, it avoids the confusing “play with naturality” bit (which is most comprehensible when written with string diagrams, and probably least comprehensible when written in terms that Coq can understand). It’s also the same way that the corresponding fact is proven in homotopy theory; see e.g. Prop. 7.8.2 in Hirschhorn’s book on model categories.

An implementation of this third proof in Coq is here. Once you take into account that it simplifies the later proofs of 2-out-of-3 for Voevodsky equivalences, I think it comes out to be a little bit shorter than the adjointification proof.

I enjoyed this so much, and so liked the coq file you wrote for it, I decided to play a bit myself — or rather, to ask what the folks around here think of my play, at github._/jcmckeown/HoTT-local (local for local-to-me, nothing to do with patches or covers). I wrote a note here about the immediate question. But really, this is very nice!

Thanks, I’m glad you liked it! Your file is quite interesting too. I would like to see the version that uses “homotopies” rather than paths between functions; I feel like perhaps the distinction there is somehow fundamental to the question of the relationship between the definitions.

Also, a small point: you claim that

{ f: A -> B & is_hiso f }is “definitionally equivalent” toin the sense that “there are functions going in both directions and their two composites unfold to a trivial identity on each side”. But I don’t see how this could be true unless your -types satisfy a definitional -conversion rule (which those of Coq don’t). Am I missing something?

Ah; I’m working with coq 8.4beta2, which seems to be quite happy identifying eta-equivalent things; whether this is a bug or feature I can’t be sure. The only beta documentation that mentions eta says coq *doesn’t* automatically look for eta-conversions, so between coq and doc there *is* a bug. I’m treating it as a feature, because we eventually assume it anyways, and it makes things much simpler at the beginning.

Does that address your concern, or am I missing something?

What do you mean by “we eventually assume it anyways”?

I knew that Coq 8.4 had definitional -conversion for dependent product types, but I didn’t know or didn’t remember that it also had it for dependent sums. I wonder how it manages that, given that dependent sums in Coq are just a special case of inductive types, and presumably not

allinductive types have definitional -conversion. (In particular, if identity types have definitional -conversion, then they are extensional!)Perhaps I don’t understand what you mean by eta; in any case, the functions (programs) I have in mind converting an hiso to a section with a section is just a constructor applied to the results of destructor; there is no path induction involved — specifically, the hiso

(f ; ( (g ; s) , (h ; r))) is mapped to the map with a section with a section ( h ; (f ; r ; ( g ; s))). Perhaps we’re surprised that ( r : is_retr f h ) also typechecks as ( r : is_sect h f ) ? I was! But I’m not about to complain.

“… if identity types have definition η-conversion, then they are extensional”

Perhaps elaborating on this (or pointing to somewhere it’s already been done) would help my confusion?

The fact that -conversion for identity types implies extensionality is described here. However, that’s not directly relevant to the function at hand; I only mentioned it as an example of why one can’t assume -conversion for

allinductive types (since identity types are a particular inductive type). The question at hand is about -conversion for dependent sum types (which are a different, particular, inductive type).The issue is that in the absence of definitional -conversion, not every term belonging to an inductive type (such as a dependent sum) is definitionally equal to one obtained from a constructor. So when you define a function using “the results of a destructor”, you are (perhaps implicitly) using the induction principle for that inductive type. If I start with an hiso H, I have to apply “match” or “destruct” or “induction” to break it down into something of the form (f ; ( (g ; s) , (h ; r))), before I can map it to ( h ; (f ; r ; ( g ; s))). If I then do the reverse operation, I’ll end up with the broken-down form (f ; ( (g ; s) , (h ; r))), which is not definitionally equal to H (unless the dependent sum type has definitional -conversion).

Does that make sense?

OK; I think I see where “definitional” is defined differently from my working-mental-impression. In any case, the thrust of what I’m trying (clumsily, I admit) to express in the phrase you don’t like is that the two maps back there fit into an hiso (or an hequiv or a…) and furthermore that no new paths have to be constructed to do so — constructing the hiso really is trivial. Maybe I should call that “convergent”…

In defense of my ignorance, the most I’ve gleaned from how others make use of the adjective “definitionally equivalent” *around*here* was that whatever it means, it’s a property one speaks of in the metatheory — something like “here’s a term that does what we want, and the proof that it does what it does is by computing it”; following links after your link… I still have to think about it. Since this is getting rather far from HoTT-proper, I’m going to duck into the nForum.

Arguably, “definitional” is a poor word; “judgmental” or “computational” is maybe better. The meaning is that it is that sort of equality which arises from reduction rules such as and , rather than the sort of equality represented by a term inhabiting an identity type. And you’re right that it’s a metaproperty, not expressible inside the type theory.

Here’s a way to test in Coq whether two functions and are a definitional/judgmental/etc. isomorphism. Does the following code

typecheck? This is I guess what you mean by “no new paths have to be constructed”. But in Coq 8.3, at least, this is not the case for the functions in question; you need to preceed the idpath with a match or destruct or something.