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

["Joyal, André" <"joyal..."@uqam.ca>]

Dear Martin,

There are many variations. For example, a homotopy equivalence can be defined to
be a pair of maps  f:a--->b and g:b--->a equipped with a pair of homotopies 
alpha:gf--->id_a and beta:fg --->id_b satisfying *one*(and only one) of the adjunction (=triangle) identities.

 Best,
André
________________________________________
From: Martin Escardo [escardo...@googlemail.com]
Sent: Sunday, October 09, 2016 2:31 PM
To: Joyal, André; HomotopyT...@googlegroups.com
Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence

Thanks, Andre.

I guess I will have to learn more to understand/appreciate this.

Nevertheless, it is still quite interesting that (1) Joyal-equivalence
is always a proposition in MLTT + funext, and that (2) it is MLTT+funext
(logically) equivalent to Voevodsky equivalence. Independently of the
homotopical motivation, this formulation of equivalence is intriguing
and elegant.

Best,
Martin

On 08/10/16 18:34, Joyal, André wrote:
> Dear Martin,
>
> I would be surprised if this characterisation of (homotopy) equivalence has not been considered by other peoples.
> The characterisation arises naturally in the theory of quasi-categories.
> Let me try to explain.
>
> Let J is the nerve of the groupoid generated by one isomorphism u:0--->1.
> It happens that an arrow $f$ in a quasi-category C is invertible in the homotopy category Ho(C) if
> and only if it is the image of the arrow $u$ by a map J--->C.
> The n-skeleton S^n of the simplicial set J is a simplicial model of the n-sphere (with two nodes 0 and 1).
> For example, the 1-skeleton S^1 is a graph with two nodes 0 and 1 and two arrows u:0--->1 and v:1--->0.
> The 2-skeleton S^2 is a obtained from S^1 by attaching two triangles (=2-simplices) representing two
> homotopies  vu-->id_0 and uv-->id_1. But none of the inclusions S^n--->J
> is a weak categorical equivalence (in fact none is a weak homotopy equivalence).
> Let me say that an extension Delta[1]--->K (=monomorphism) is a *good approximation* of J
> if the map K-->pt is a weak  categorical equivalence (ie if K is weakly categorically contractible)
> For example, the n-skeleton S^n of J is the union of two n-disks S^n(+) and S^n(-).
> If n\geq 3, then the disks S^n(+) and S^n(-) are good approximation if J.
> In general, an extension Delta[1]--->K is a good approximation of J if and only
> if Ho(K) is a groupoid and the map K--->1 is a weak homotopy equivalence (ie $K$ is weakly homotopy contractible).
> For example, let U be the union of the outer faces \partial_3Delta[3] and  \partial_0Delta[3]
> of the 3-simplex Delta[3]. The simplicial set U consists of two triangles  0-->1--->2  and
> 1--->2---->3 glued together along the edge 1-->2. Consider the quotient q:U--->K
> obtained by identifying the edge 0-->2 to a point q(0)=q(2) and the edge 1-->3 of to a point q(1)=q(3).
> The simplicial set K has two vertices, q(0) and q(1), and three edges
> a:q(0)-->q(1), b:q(1)--->q(0) and c:q(0)-->q(1) respectively the image by q of the edges 0-->1, 1--->2 and 2--->3.
> It is easy to verify that Ho(K) is a groupoid and that K is weakly homotopy contractible.
>
>
> I hope these explanations are not too obscure!
>
>
> Best regards,
> André
>
>
> ________________________________________
> From: 'Martin Escardo' via Homotopy Type Theory [HomotopyT...@googlegroups.com]
> Sent: Friday, October 07, 2016 8:21 PM
> To: HomotopyT...@googlegroups.com
> Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence
>
> On 08/10/16 00:51, 'Martin Escardo' via Homotopy Type Theory wrote:
>> This shouldn't have happened (it seems like a bug):
>
> Oh, well. Let me retype everything again from memory, in a shorter
> way, and then this time send it to everybody.
>
> The main insight of univalent type theory is the formulation of
> equivalence (as e.g. the contractibility of all fibers) so that it is
> a proposition.
>
> An equivalent formulation, attributed to Joyal, and discussed in the
> Book, is that the function has a given left inverse and that the
> function also has a given right inverse, where both "given" are
> expressed with Sigma. One can prove that this notion of
> Joyal-equivalence is a proposition, in MLTT, assuming funext, which is
> nice and slightly surprising at first sight.
>
> But where does this formulation of the notion of equiavelence come from?
>
> Best,
> Martin
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>