Dear Vladimir,

I completely agree with you.

André

---

From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of Vladimir Voevodsky [vlad...@ias.edu]
Sent: Wednesday, October 12, 2016 6:17 PM
To: Peter LeFanu Lumsdaine
Cc: Prof. Vladimir Voevodsky; Martin Escardo; Joyal, André; HomotopyTypeTheory@googlegroups.com
Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence

I think the clearest formulation is my original one - as the condition of contractibility of the h-fibers.

This is also the first form in which it was introduced and the first explicit formulation and proof of the fact that it is a proposition. 

Vladimir.

On Oct 12, 2016, at 5:45 AM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

> Although I can see formal proofs that Joyal-equivalence is a proposition (or h-proposition), I am still trying to find the best formal proof that uncovers the essence of this fact. This is why I asked the question of were this formulation of equivalence comes from.

Like André suggested, I feel the nicest viewpoint is the fact that the “free (∞,1)-category on a Joyal-equivalence” is contractible.  At least in terms of intuition, the conceptually clearest argument I know for that is as follows.

Look at the *∞-groupoidification* of this free (∞,1)-category, considered as a space.  This is a cell complex which we can easily picture: two points x, y, three paths f, g, g' between x and y, and 2-cells giving homotopies f ~ g, f ~ g'.  It’s very clear geometrically that this is contractible.

But — the “free (∞,1)-category on a Joyal equivalence” is already an ∞-groupoid — and ∞-groupoidification is idempotent, since groupoids are a full subcategory.  So the original (∞,1)-category is equivalent to its groupoidification, so is contractible.

The same approach works for seeing why half-adjoint equivalences are good, but non-adjoint and bi-adjoint equivalences are not.  So as regards intuition, I think this is very nice.  However, I suspect that if one looks at all the work that goes into setting up the framework needed, then somewhere one will have already used some form of “equivalence is a proposition”.  So this is perhaps a little unsatisfactory formally, as it (a) needs a lot of background, and (b) may need to rely on some more elementary proof of the same fact.

The earliest explicit discussion I know of this issue (i.e.“contractibility of the walking equivalence as a quality criterion for structured notions of equivalence) is in Steve Lack’s “A Quillen Model Structure for Bicategories”, fixing an error in his earlier “A Quillen Model Structure for 2-categories”, where he had used non-adjoint equivalences — see http://maths.mq.edu.au/~slack/papers/qmc2cat.html  Since it’s just 2-categorical, he’s able to use fully adjoint equivalences — doesn’t have to worry about half-adjointness/coherent-adjointness.  Adjoint equivalences of course go back much further — but I don’t know anywhere that this *reason* why they’re better is articulated, before Lack. 

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!

–p.

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.