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.

[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

[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

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.

[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

[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

[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

[Peter LeFanu Lumsdaine]

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

[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

[Vladimir Voevodsky]

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.

[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

[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

[Joyal, André]

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

[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

[Egbert Rijke]

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