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

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

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.