Look at the *=E2=88=9E-groupoidification* of this free (=E2=88=9E,1)=
-category, considered as a space.=C2=A0 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'.=C2=A0 It=E2=80=99s very c=
lear geometrically that this is contractible.
But =
=E2=80=94 the =E2=80=9Cfree (=E2=88=9E,1)-category on a Joyal equivalence=
=E2=80=9D is already an =E2=88=9E-groupoid =E2=80=94 and =E2=88=9E-groupoid=
ification is idempotent, since groupoids are a full subcategory.=C2=A0 So t=
he original (=E2=88=9E,1)-category is equivalent to its groupoidification, =
so is contractible.
The same approach works for se=
eing why half-adjoint equivalences are good, but non-adjoint and bi-adjoint=
equivalences are not.=C2=A0 So as regards intuition, I think this is very =
nice.=C2=A0 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 =E2=80=9Cequivalence is a proposition=E2=80=9D.=C2=A0 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 s=
ame fact.
The earliest ex=
plicit discussion I know of this issue (i.e.=E2=80=9Ccontractibility of the=
walking equivalence as a quality criterion for structured notions of equiv=
alence) is in Steve Lack=E2=80=99s =E2=80=9CA Quillen Model Structure for B=
icategories=E2=80=9D, fixing an error in his earlier =E2=80=9CA Quillen Mod=
el Structure for 2-categories=E2=80=9D, where he had used non-adjoint equiv=
alences =E2=80=94 see
http://maths.mq.edu.au/~slack/papers/qmc2cat.html =C2=A0Since =
it=E2=80=99s just 2-categorical, he=E2=80=99s able to use fully adjoint equ=
ivalences =E2=80=94 doesn=E2=80=99t have to worry about half-adjointness/co=
herent-adjointness.=C2=A0 Adjoint equivalences of course go back much furth=
er =E2=80=94 but I don=E2=80=99t know anywhere that this *reason* why they=
=E2=80=99re better is articulated, before Lack.=C2=A0
<=
div>And for Joyal-equivalences, I don=E2=80=99t know anywhere they=E2=80=99=
re explicitly discussed at all, before HoTT.=C2=A0 Like Mart=C3=ADn, I=E2=
=80=99d be really interested if anyone does know any earlier sources for th=
em!