* Re: Joyal's version of the notion of equivalence [not found] <963893a3-bfdf-d9bd-8961-19bab69e0f7c@googlemail.com> @ 2016-10-07 23:51 ` Martin Escardo 2016-10-08 0:21 ` [HoTT] " Martin Escardo 0 siblings, 1 reply; 14+ messages in thread From: Martin Escardo @ 2016-10-07 23:51 UTC (permalink / raw) To: HomotopyT...@googlegroups.com 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. ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-07 23:51 ` Joyal's version of the notion of equivalence Martin Escardo @ 2016-10-08 0:21 ` Martin Escardo 2016-10-08 17:34 ` Joyal, André 0 siblings, 1 reply; 14+ messages in thread From: Martin Escardo @ 2016-10-08 0:21 UTC (permalink / raw) To: HomotopyT...@googlegroups.com 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 ^ permalink raw reply [flat|nested] 14+ messages in thread
* RE: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-08 0:21 ` [HoTT] " Martin Escardo @ 2016-10-08 17:34 ` Joyal, André 2016-10-09 18:31 ` Martin Escardo 0 siblings, 1 reply; 14+ messages in thread From: Joyal, André @ 2016-10-08 17:34 UTC (permalink / raw) To: Martin Escardo, HomotopyT...@googlegroups.com 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. ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-08 17:34 ` Joyal, André @ 2016-10-09 18:31 ` Martin Escardo 2016-10-09 18:56 ` Joyal, André 0 siblings, 1 reply; 14+ messages in thread From: Martin Escardo @ 2016-10-09 18:31 UTC (permalink / raw) To: Joyal, André, HomotopyT...@googlegroups.com 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. > ^ permalink raw reply [flat|nested] 14+ messages in thread
* RE: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-09 18:31 ` Martin Escardo @ 2016-10-09 18:56 ` Joyal, André 2016-10-11 22:54 ` Martin Escardo 0 siblings, 1 reply; 14+ messages in thread From: Joyal, André @ 2016-10-09 18:56 UTC (permalink / raw) To: Martin Escardo, HomotopyT...@googlegroups.com 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. > ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-09 18:56 ` Joyal, André @ 2016-10-11 22:54 ` Martin Escardo 2016-10-12 9:45 ` Peter LeFanu Lumsdaine 0 siblings, 1 reply; 14+ messages in thread From: Martin Escardo @ 2016-10-11 22:54 UTC (permalink / raw) To: Joyal, André, HomotopyT...@googlegroups.com 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 ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-11 22:54 ` Martin Escardo @ 2016-10-12 9:45 ` Peter LeFanu Lumsdaine 2016-10-12 13:21 ` Dan Christensen 2016-10-12 22:17 ` Vladimir Voevodsky 0 siblings, 2 replies; 14+ messages in thread From: Peter LeFanu Lumsdaine @ 2016-10-12 9:45 UTC (permalink / raw) To: Martin Escardo; +Cc: Joyal, André, HomotopyT...@googlegroups.com [-- 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 --] ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: Joyal's version of the notion of equivalence 2016-10-12 9:45 ` Peter LeFanu Lumsdaine @ 2016-10-12 13:21 ` Dan Christensen 2016-10-12 22:45 ` [HoTT] " Martin Escardo 2016-10-12 22:17 ` Vladimir Voevodsky 1 sibling, 1 reply; 14+ messages in thread From: Dan Christensen @ 2016-10-12 13:21 UTC (permalink / raw) To: Homotopy Type Theory List 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 ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-12 13:21 ` Dan Christensen @ 2016-10-12 22:45 ` Martin Escardo 0 siblings, 0 replies; 14+ messages in thread From: Martin Escardo @ 2016-10-12 22:45 UTC (permalink / raw) To: Homotopy Type Theory List 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 ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-12 9:45 ` Peter LeFanu Lumsdaine 2016-10-12 13:21 ` Dan Christensen @ 2016-10-12 22:17 ` Vladimir Voevodsky 2016-10-12 23:55 ` Martin Escardo 2016-10-13 7:14 ` Joyal, André 1 sibling, 2 replies; 14+ messages in thread From: Vladimir Voevodsky @ 2016-10-12 22:17 UTC (permalink / raw) To: Peter LeFanu Lumsdaine Cc: Prof. Vladimir Voevodsky, Martin Escardo, "Joyal, André", HomotopyT...@googlegroups.com [-- 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 --] ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-12 22:17 ` Vladimir Voevodsky @ 2016-10-12 23:55 ` Martin Escardo 2016-10-13 10:14 ` Thomas Streicher 2016-10-13 7:14 ` Joyal, André 1 sibling, 1 reply; 14+ messages in thread From: Martin Escardo @ 2016-10-12 23:55 UTC (permalink / raw) To: Vladimir Voevodsky, Peter LeFanu Lumsdaine Cc: Joyal, André, HomotopyT...@googlegroups.com 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 ^ permalink raw reply [flat|nested] 14+ messages in thread
* Re: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-12 23:55 ` Martin Escardo @ 2016-10-13 10:14 ` Thomas Streicher 0 siblings, 0 replies; 14+ messages in thread From: Thomas Streicher @ 2016-10-13 10:14 UTC (permalink / raw) To: Martin Escardo Cc: Vladimir Voevodsky, Peter LeFanu Lumsdaine, Joyal, André, HomotopyT...@googlegroups.com > 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 ^ permalink raw reply [flat|nested] 14+ messages in thread
* RE: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-12 22:17 ` Vladimir Voevodsky 2016-10-12 23:55 ` Martin Escardo @ 2016-10-13 7:14 ` Joyal, André 2016-10-13 12:48 ` Egbert Rijke 1 sibling, 1 reply; 14+ messages in thread From: Joyal, André @ 2016-10-13 7:14 UTC (permalink / raw) To: Vladimir Voevodsky, Peter LeFanu Lumsdaine Cc: Martin Escardo, HomotopyT...@googlegroups.com [-- 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 --] ^ permalink raw reply [flat|nested] 14+ messages in thread
* RE: [HoTT] Re: Joyal's version of the notion of equivalence 2016-10-13 7:14 ` Joyal, André @ 2016-10-13 12:48 ` Egbert Rijke 0 siblings, 0 replies; 14+ messages in thread From: Egbert Rijke @ 2016-10-13 12:48 UTC (permalink / raw) To: André Joyal Cc: HomotopyT...@googlegroups.com, Martin Escardo, Peter LeFanu Lumsdaine, Vladimir Voevodsky [-- 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 --] ^ permalink raw reply [flat|nested] 14+ messages in thread
end of thread, other threads:[~2016-10-13 12:48 UTC | newest] Thread overview: 14+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- [not found] <963893a3-bfdf-d9bd-8961-19bab69e0f7c@googlemail.com> 2016-10-07 23:51 ` Joyal's version of the notion of equivalence Martin Escardo 2016-10-08 0:21 ` [HoTT] " Martin Escardo 2016-10-08 17:34 ` Joyal, André 2016-10-09 18:31 ` Martin Escardo 2016-10-09 18:56 ` Joyal, André 2016-10-11 22:54 ` Martin Escardo 2016-10-12 9:45 ` Peter LeFanu Lumsdaine 2016-10-12 13:21 ` Dan Christensen 2016-10-12 22:45 ` [HoTT] " Martin Escardo 2016-10-12 22:17 ` Vladimir Voevodsky 2016-10-12 23:55 ` Martin Escardo 2016-10-13 10:14 ` Thomas Streicher 2016-10-13 7:14 ` Joyal, André 2016-10-13 12:48 ` Egbert Rijke
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).