Re: Joyal's version of the notion of equivalence

Re: Joyal's version of the notion of equivalence

[Martin Escardo]

This shouldn't have happened (it seems like a bug):

On 08/10/16 00:09, Martin Escardo wrote:
> Questions:
>
> f:X->Y is a Joyal-equivalence := (Sigma(g:Y->X).g.f~id)x(Sigma()
>
> (1) How

I intended to send a complete message to somebody else (did you get 
it?), but instead it seems somehow we got a double bug: wrong recipient, 
and 1% of the message.

Apologies. I don't know how such a thing can happen. (From Thunderbird.)

M.

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

[Martin Escardo]

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

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

[Joyal, André]

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.

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

[Martin Escardo]

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.
>

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

[Joyal, André]

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.
>

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

[Martin Escardo]

On 09/10/16 19:56, Joyal, André wrote:
> 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.

I am aware of that, but thanks for bringing it up again.

Perhaps what you bring up is related to the fact that if the type R x y 
is a retract of the type Id_X x y for all x,y:X, then in fact the two 
types are equivalent for all x,y. (Where R : X -> X -> U is arbitrary.)

(So in my example only *one* composition to the identity is enough to 
get the *other* composition to be the identity too.)

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.

This seems similar to trying to understand, as discussed in other 
messages in this list, the J combinator, expressing induction on Id, as 
a reformulation of the Yoneda Lemma, when types are seeing as 
omega-groupoids.

Best,
Martin

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

[Peter LeFanu Lumsdaine]

[-- Attachment #1: Type: text/plain, Size: 2600 bytes --]

> 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.

[-- Attachment #2: Type: text/html, Size: 2864 bytes --]

Re: Joyal's version of the notion of equivalence

[Dan Christensen]

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.

I'm pretty sure this was already there in the original 2002 edition.

Of course, this is an easy categorical fact that was well-known, but
this is at least an explicit mention of this in the case of homotopy
equivalences.

Dan

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

[Martin Escardo]

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

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

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 3401 bytes --]

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 <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 HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #1.2: Type: text/html, Size: 4702 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

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

[Martin Escardo]

On 12/10/16 23:17, Vladimir Voevodsky wrote:
> 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, I agree with what you say above.

I was just trying to understand a particular, interesting case of a 
situation where we have types P(f) and Q(f) that are not hpropositions 
in general, but such that the product type P(f)xQ(f) is always an 
hproposition, as explained in my previous messages.

I hoped to get a motivation from homotopy theory, and Andre tried to 
explain this to me.

I do find it rather interesting that the cartesian product of two such 
types that are not in general hpropositions is always an hproposition.

A function can have a section in zillions of ways, and also have 
retraction in just as many ways, and we know in set theory that a 
function can have both a section and a retraction in at most one way. 
This is not surprising. But it does surprise me, for the moment, that 
this is the case in univalent mathematics too, given that we do know 
that the type of two-sided inverses is in general *not* an hproposition.

Best,
Martin

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

[Thomas Streicher]

> I do find it rather interesting that the cartesian product of two such types
> that are not in general hpropositions is always an hproposition.

Well, it rarely happens that li(f) and ri(f) are both inhabited and if
so then both contain morally just one element (in case of Set).
The point seeeems to be that the type li(f) x ri(f)  is connected. If
you intersect it with the diagonal then it is not connected anymore.

That subobjects of connected objects need not be connected anymore is
geometrically quite intuitive.

For example (\Sigma y:A) Path_A(x,y) is always connected though its
subobject Path_A(x,x) is not.

Thomas

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

[Joyal, André]

[-- Attachment #1: Type: text/plain, Size: 4042 bytes --]

Dear Vladimir,

I completely agree with you.

André
________________________________
From: homotopyt...@googlegroups.com [homotopyt...@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é; HomotopyT...@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<mailto: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!

?Cp.

--
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<mailto:HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 6273 bytes --]

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

[Egbert Rijke]

[-- Attachment #1: Type: text/plain, Size: 4919 bytes --]

Dear all,

I agree with Vladimir that his notion of equivalence is a very clear one,
but that doesn't take away that on some occasions it is really helpful to
have Joyal's notion around.

For instance, in the definition of localization as a higher inductive type
we use Joyal-equivalence, simply to avoid 2-path constructors.

With kind regards,
Egbert

On Oct 13, 2016 3:14 AM, "Joyal, André" <joyal...@uqam.ca> wrote:

> Dear Vladimir,
>
> I completely agree with you.
>
> André
> ------------------------------
> *From:* homotopyt...@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é;
> HomotopyT...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #2: Type: text/html, Size: 7128 bytes --]