Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Egbert Rijke <e.m.rijke@gmail.com>
To: Noah Snyder <nsnyder@gmail.com>
Cc: Kristina Sojakova <sojakova.kristina@gmail.com>,
	 Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Syllepsis in HoTT
Date: Mon, 8 Mar 2021 16:46:29 +0100	[thread overview]
Message-ID: <CAGqv1OAuHQwnZvvDfkM99o6Za=SrjPYO3J62MPMFxphDzVOiEw@mail.gmail.com> (raw)
In-Reply-To: <CAO0tDg6MCr7skausPPmomQrswRk1umaq3_V=52z60vxMj-hraQ@mail.gmail.com>

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

Congratulations, Kristina, on doing it so fast.

I had a different route in mind, much less efficient. There are three kinds
of concatenations in the third identity type, all three pairs of them
satisfy interchange laws, and there is a coherence law between the three
interchange laws. This is what I had already formalized, and this coherence
law induces the syllepsis. But it takes me a lot more coding to do it in
the way I had in mind, which is why it takes me forever.

Best,
Egbert

On Mon, Mar 8, 2021 at 4:36 PM Noah Snyder <nsnyder@gmail.com> wrote:

> My funny remark is slightly inaccurate.  \pi_3(S^2) just classifies proofs
> of EH where both 2-loops are the same as each other.  It is true that
> there's also a Z-worth of proofs of EH in the general case, but this is a
> subtler fact about \pi_3(S^2 \wedge S^2).  Nonetheless  the point remains
> that any two reasonable proofs of EH will be equal or inverse to each
> other.  Best,
>
> Noah
>
> On Mon, Mar 8, 2021 at 10:23 AM Noah Snyder <nsnyder@gmail.com> wrote:
>
>> One funny remark, that \pi_3(S^2) = Z exactly tells you that any proof of
>> Eckman-Hilton is given by repeatedly applying either the standard proof or
>> its inverse.
>>
>> In a sense there are exactly two “good” proofs of EH (the standard one
>> and it’s inverse).  In principle it’s not so automatic to see that a given
>> proof is one of the good two, but in practice it’d be hard to give a bad
>> one accidentally.  By contrast, put two people in two separate rooms and
>> there’s a good chance they’ll produce the two different good proofs (ie the
>> clockwise proof and the counterclockwise proof).  Best,
>>
>> Noah
>>
>> On Mon, Mar 8, 2021 at 10:15 AM Kristina Sojakova <
>> sojakova.kristina@gmail.com> wrote:
>>
>>> Thanks Dan! I think we should have no trouble showing that what I used
>>> is equal to your proof but packaged a bit differently.
>>>
>>> On 3/8/21 4:10 PM, Dan Christensen wrote:
>>> > It's great to see this proved!
>>> >
>>> > As a tangential remark, I mentioned after Jamie's talk that I had a
>>> > very short proof of Eckmann-Hilton, so I thought I should share it.
>>> > Kristina's proof is slightly different and is probably designed to
>>> > make the proof of syllepsis go through more easily, but here is mine.
>>> >
>>> > Dan
>>> >
>>> >
>>> > Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p
>>> = 1) (k : 1 = q)
>>> >    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
>>> > Proof.
>>> >    by induction k; revert p h; rapply paths_ind_r.
>>> > Defined.
>>> >
>>> > Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h :
>>> p = 1) (k : 1 = q)
>>> >    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
>>> > Proof.
>>> >    by induction k; revert p h; rapply paths_ind_r.
>>> > Defined.
>>> >
>>> > Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x))
>>> : h @ k = k @ h
>>> >    := (horizontal_vertical h k) @ (horizontal_vertical' k h)^.
>>> >
>>> >
>>> >
>>> > On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com>
>>> wrote:
>>> >
>>> >> Dear all,
>>> >>
>>> >> I formalized my proof of syllepsis in Coq:
>>> >>
>>> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
>>> >>
>>> >>
>>> >> I am looking forward to see how it compares to the argument Egbert has
>>> >> been working on.
>>> >>
>>> >> Best,
>>> >>
>>> >> Kristina
>>> >>
>>> >> On 3/8/2021 2:38 PM, Noah Snyder wrote:
>>> >>
>>> >>      The generator of \pi_4(S^3) is the image of the generator of
>>> \pi_3
>>> >>      (S^2) under stabilization.  This is just the surjective the part
>>> >>      of Freudenthal.  So to see that this generator has order dividing
>>> >>      2 one needs exactly two things: the syllepsis, and my follow-up
>>> >>      question about EH giving the generator of \pi_3(S^2).  This is
>>> why
>>> >>      I asked the follow-up question.
>>> >>
>>> >>      Note that putting formalization aside, that EH gives the
>>> generator
>>> >>      of \pi_4(S^3) and the syllepsis the proof that it has order 2,
>>> are
>>> >>      well-known among mathematicians via framed bordism theory
>>> (already
>>> >>      Pontryagin knew these two facts almost a hundred years ago).  So
>>> >>      informally it’s clear to mathematicians that the syllepsis shows
>>> >>      this number is 1 or 2.  Formalizing this well-known result
>>> remains
>>> >>      an interesting question of course.
>>> >>
>>> >>      Best,
>>> >>
>>> >>      Noah
>>> >>
>>> >>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com
>>> >
>>> >>      wrote:
>>> >>
>>> >>          Dear Noah,
>>> >>
>>> >>          I don't think that your claim that syllepsis gives a proof
>>> >>          that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
>>> >>          you that a certain element of pi_4(S^3) has order 1 or 2, but
>>> >>          it is an entirely different matter to show that this element
>>> >>          generates the group. There could be many elements of order 2.
>>> >>
>>> >>          Best wishes,
>>> >>          Egbert
>>> >>
>>> >>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
>>> >>          <e.m.rijke@gmail.com> wrote:
>>> >>
>>> >>              Hi Kristina,
>>> >>
>>> >>              I've been on it already, because I was in that talk, and
>>> >>              while my formalization isn't yet finished, I do have all
>>> >>              the pseudocode already.
>>> >>
>>> >>              Best wishes,
>>> >>              Egbert
>>> >>
>>> >>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
>>> >>              <nsnyder@gmail.com> wrote:
>>> >>
>>> >>                  On the subject of formalization and the syllepsis,
>>> has
>>> >>                  it ever been formalized that Eckman-Hilton gives the
>>> >>                  generator of \pi_3(S^2)?  That is, we can build a
>>> >>                  3-loop for S^2 by refl_refl_base --> surf \circ surf^
>>> >>                  {-1} --EH--> surf^{-1} \circ surf -->
>>> refl_refl_base,
>>> >>                  and we want to show that under the equivalence \pi_3
>>> >>                  (S^2) --> Z constructed in the book that this 3-loop
>>> >>                  maps to \pm 1 (which sign you end up getting will
>>> >>                  depend on conventions).
>>> >>
>>> >>                  There's another explicit way to construct a
>>> generating
>>> >>                  a 3-loop on S^2, namely refl_refl_base --> surf \circ
>>> >>                  surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>>> >>                  refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
>>> >>                  -> refl_refl_base, where I've suppressed a lot of
>>> >>                  associators and other details.  One could also ask
>>> >>                  whether this generator is the same as the one in my
>>> >>                  first paragraph.  This should be of comparable
>>> >>                  difficulty to the syllepsis (perhaps easier), but is
>>> >>                  another good example of something that's "easy" with
>>> >>                  string diagrams but a lot of work to translate into
>>> >>                  formalized HoTT.
>>> >>
>>> >>                  Best,
>>> >>
>>> >>                  Noah
>>> >>
>>> >>                  On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>>> >>                  <sojakova.kristina@gmail.com> wrote:
>>> >>
>>> >>                      Dear all,
>>> >>
>>> >>                      Ali told me that apparently the following problem
>>> >>                      could be of interest
>>> >>                      to some people
>>> >>                      (
>>> https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s):
>>> >>
>>> >>
>>> >>                      Given two higher paths p, q : 1_x = 1_x,
>>> >>                      Eckmann-Hilton gives us a path
>>> >>                      EH(p,q) : p @ = q @ p. Show that EH(p,q) @
>>> EH(q,p)
>>> >>                      = 1_{p@q=q_p}.
>>> >>
>>> >>                      I just established the above in HoTT and am
>>> >>                      thinking of formalizing it,
>>> >>                      unless someone already did it.
>>> >>
>>> >>                      Thanks,
>>> >>
>>> >>                      Kristina
>>> >>
>>> >>                      --
>>> >>                      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+unsubscribe@googlegroups.com.
>>> >>                      To view this discussion on the web visit
>>> >>
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com
>>> .
>>> >>
>>> >>
>>> >>                  --
>>> >>                  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+unsubscribe@googlegroups.com.
>>> >>                  To view this discussion on the web visit
>>> >>
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com
>>> .
>>>
>>> --
>>> 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+unsubscribe@googlegroups.com.
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/1f7bbcb8-ee50-0c24-174e-d3852e52bbee%40gmail.com
>>> .
>>>
>> --
> 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+unsubscribe@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg6MCr7skausPPmomQrswRk1umaq3_V%3D52z60vxMj-hraQ%40mail.gmail.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg6MCr7skausPPmomQrswRk1umaq3_V%3D52z60vxMj-hraQ%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>

-- 
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1OAuHQwnZvvDfkM99o6Za%3DSrjPYO3J62MPMFxphDzVOiEw%40mail.gmail.com.

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

  reply	other threads:[~2021-03-08 15:46 UTC|newest]

Thread overview: 19+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-03-05 18:27 Kristina Sojakova
2021-03-05 18:40 ` Jamie Vicary
2021-03-05 19:18   ` Noah Snyder
2021-03-07 18:00 ` Noah Snyder
2021-03-08  8:44   ` Egbert Rijke
2021-03-08  8:53     ` Egbert Rijke
2021-03-08 13:38       ` Noah Snyder
2021-03-08 14:31         ` Kristina Sojakova
2021-03-08 15:10           ` Dan Christensen
2021-03-08 15:15             ` Kristina Sojakova
2021-03-08 15:23               ` Noah Snyder
2021-03-08 15:35                 ` Noah Snyder
2021-03-08 15:46                   ` Egbert Rijke [this message]
2021-03-08 15:49                     ` Kristina Sojakova
2021-03-08 16:25                     ` Dan Christensen
2021-03-08 16:27                       ` Kristina Sojakova
2021-03-08 16:38             ` Kristina Sojakova
2021-03-08 16:54               ` Egbert Rijke
2021-03-08 19:55                 ` 'Favonia' via Homotopy Type Theory

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAGqv1OAuHQwnZvvDfkM99o6Za=SrjPYO3J62MPMFxphDzVOiEw@mail.gmail.com' \
    --to=e.m.rijke@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=nsnyder@gmail.com \
    --cc=sojakova.kristina@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).