Re: [HoTT] Re: Joyal's version of the notion of equivalence

[Martin Escardo <escardo...@googlemail.com>]

On 12/10/16 14:21, Dan Christensen wrote:
> On Oct 12, 2016, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
>
>> And for Joyal-equivalences, I don’t know anywhere they’re explicitly
>> discussed at all, before HoTT.  Like Martín, I’d be really interested if
>> anyone does know any earlier sources for them!
>
> I'm not sure if this is what you are looking for, but Exercise 11 in
> Chapter 0 of Hatcher's "Algebraic Topology" says:
>
>   Show that f : X -> Y is a homotopy equivalence if there exist maps
>   g, h : Y -> X such that fg ≃ 1 and hf ≃ 1.  More generally, show that
>   f is a homotopy equivalence if fg and hf are homotopy equivalences.

Nice for the historical record as asked by Peter L.

But let me try dissect this from the point of view of univalent type
theory, and relate it to my question.

    Joyal-equivalence(f:X->Y) := f has a section * f has a retraction.
    f has a section    := Sigma(g:Y->X), fg ≃ 1.
    f has a retraction := Sigma(h:Y->X), hf ≃ 1.

Remark 1. "Sigma" is not the same thing as "exists".

Remark 2. The type "f has a section" is not an hproposition. This
means that having a section is structure rather than property.
Similarly for "f has a retraction".

Remark 3. Existence is truncated structure. So there is no problem *at
all* in seeing that

       f is an equivalence := ||f has a section|| *
                              ||f has a retraction||.

(Which is what the above exercise says a priori.)

But my question was why, although each of

     f has a section

and

     f has a retraction

individually are structure on f, they become property of f when put
together.

I know why, as I said, because I am in possession of a proof. But I
don't feel I am in possession of a conceptual explanation.

Best,
Martin