New proof that equivalences are contractible maps using fiber induction

[emilyriehl]

Last week @TashiWalde defined ind-fib an induction principle for types depending on an arbitrary fiber of a map. Using this I've reproven that equivalences are contractible maps in a more efficient way. This version shows both the new proof and the old one for sake of comparison but before merging we should delete the old one and steal some of its names; in the new version I've written is-hae for is-half-adjoint-equiv in term names.

Like the old proof, the new one first proves that half adjoint equivalences are contractible. I attempted to skip this step but found it too difficult to define the coherence term needed by the ind-fib function, which requires precisely the coherence data of a half adjoint equivalence (though presented in a different form).

Let me know what you think.

[TashiWalde]

There is also a nice proof that does not use half adjoint equivalences which I read in Escardó's notes:

It roughly goes as follows: 1) Prove that for every g: Y -> X with a section f : X -> Y and every B : X -> U, the type Sigma_X B is a retract of Sigma (y:Y) B(g y). This is a statement which is useful to have anyway. 1') For each z : Y, specialising B x to be f x = z then yields that fib f z is a retract of Sigma (y:Y) f (g y) = z 2) For every f : X -> Y with a section g, and every y, z : Y have y=z equivalent to f (g y)=z. This is just transport along the path f (g y) = y exhibition g as a section. 2') Sum up these equivalences to get an equivalence between Sigma (y:Y) y=z and Sigma (y:Y) f (g y) = z. 3) Putting 1') and 2') together in the case where f and g are mutually inverse, obtain that for each z: Y, the fiber fib f z is a retract of the contractible type Sigma (y:Y) y=z, hence itself contractible.

The only disadvantage of this proof in our current setup is that for (2 -> 2') it uses that equivalences \ (x : A) -> C x \simeq D x induce equivalences Sigma A C \simeq Sigma A D, which is a fact we currently only prove in document 08. It does not seem like that proof really relies on anything before it though (for example, see #85 where this fact is reimplemented), so one could just move it forward.

[emilyriehl]

Very nice. We could certainly implement that here instead.

A thing I kind of like about the proof we have now is it helps illustrate what the coherence in a half adjoint equivalence is good for. Without some applications of this nature, it's not so clear that this notion is as interesting as the other ways of encoding the property of being an equivalence.

But I don't have strong feelings either way. Would anyone else like to weigh in?

[emilyriehl]

Here's a proposed path forward. Let's go ahead and merge this new (since it's much better than the original proof) and I'd be happy to have it as part of the history of the repository. Then later if @TashiWalde (or someone else) wants to implement the other version we've discussed to avoid the use of half adjoint equivalences, they can.

[emilyriehl]

This pull request also fixes a markdown formatting error in the extension types file that I'd love to get merged soon, especially before @fizruk's talk tomorrow. So @fizruk or @jonweinb could you review this when you get the chance?