[-- Attachment #1: Type: text/plain, Size: 504 bytes --] Dear all, I am attaching a proof of syllepsis written out, since some people expressed an interest. Best, 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/13804bae-56b3-93cd-c741-a1f41afcae25%40gmail.com. [-- Attachment #2: syllepsis.pdf --] [-- Type: application/pdf, Size: 343945 bytes --]

CALL FOR PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations July 17-18, 2021, The Internet @ Buenos Aires, Argentina https://hott-uf.github.io/2021/ Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Registration Registration is free of charge, but required. Please see https://fscd2021.dc.uba.ar/registration.html # Invited talks * Evan Cavallo (Carnegie Mellon University) Cohesive Internal Parametricity for Cubical Type Theory * Peter LeFanu Lumsdaine (Stockholm University) Categories with attributes are not full split comprehension categories * Anja Petković Komel (University of Ljubljana) Towards an Elaboration Theorem * Matthew Weaver (Princeton University) ([Directed] Higher) Inductive Types in Bicubical Directed Type Theory # Contributed talks 12 talks were accepted by the Program Committee. Their titles and abstracts are available on the event website. # Schedule The event will take place from July 17-18, 2021. The talks are scheduled 2 PM and 8 PM CEST (UTC+2). Detailed schedule is now available on the website. # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario) -- 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/CAEXhy3M7Nkaz7f%2Bg0VkZkwPaJcYGPSj%2BXJFGXSB_DH8oPftF4g%40mail.gmail.com.

This week (5-9 July) is taking place a conference to celebrate 90 years of the publication of Gödel's Incompleteness Theorems. https://uni-tuebingen.de/en/einrichtungen/zentrale-einrichtungen/carl-friedrich-von-weizsaecker-zentrum/veranstaltungen/celebrating-90-years-of-goedels-incompleteness-theorems/ The conference is composed by a series of workshop: - 5.7. Monday afternoon: Opening. Higher proof theory after Gödel - 6.7. Tuesday morning: Type theory in type theory - 6.7. Tuesday afternoon: Computation in face of incompleteness - 7.7. Wednesday morning: Cut-elimination and Herbrand's Theorem - 7.7. Wednesday afternoon: Provability predicates - 8.7. Thursday morning: Diagonalisation - 8.7. Thursday afternoon: Recursion-theoretic approaches to computation and complexity - 9.7. Friday morning: Philosophy of mathematics after Gödel - 9.7. Friday afternoon: Aspects of Gödel's unpublished work; Closing Lecture by Jan von Plato If you would like to participate online, please write to Marcel Ertel events.cfvwz@listserv.uni-tuebingen.de to receive the Zoom link. -- 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/c37ae81c-d30c-b69a-9e04-934373a4214d%40gmail.com.

Dear All, You might be interested in participating in the COST action EuroProofNet, the aim of which is to improve interoperability of computer proof systems - not restricted to HoTT or type theory, but including those. The action is led by Frédéric Blanqui, whose message about the action is copied below. If you are interested, please register for participation at the link https://e-services.cost.eu/action/CA20111/working-groups/apply. Participation is restricted to countries participating in COST - these are, in particular, EU countries, but also countries outside the EU, see https://www.cost.eu/about/members/. Best, Benedikt Dear all, I am happy to announce the launch of a new COST action, EuroProofNet (see https://www.cost.eu/actions/CA20111/). EuroProofNet aims at federating all the European research groups working on proofs in order to improve the interoperability of proof systems. There are currently 6 working groups (WG): - WG1: Proof systems interoperability. - WG2: Automated theorem provers. - WG3: Program verification. - WG4: Libraries of formal proofs. - WG5: Machine learning in proofs. - WG6: Type theory. You will find all the details on the objectives of EuroProofNet in https://e-services.cost.eu/files/domain_files/CA/Action_CA20111/mou/CA20111-e.pdf . A COST action can fund visits to other labs, and participation to summer schools, workshops and conferences. Anyone willing to contribute to the goals of the action is eligible. If you are interested, you just need to register on https://e-services.cost.eu/action/CA20111/working-groups/apply . Best regards, Frédéric Blanqui, chair of EuroProofNet. -- 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/73181596-108f-4370-074e-f2d25ce5ca78%40gmail.com.

[-- Attachment #1.1: Type: text/plain, Size: 948 bytes --] Dear colleague, The ILLC (part of the University of Amsterdam) is advertising an open PhD position (at the Faculty of Science); the deadline is 13 June 2021. The vacancy can be found here: https://www.uva.nl/shared-content/uva/en/vacancies/2021/05/21-315-phd-in-logic-language-and-computation.html?origin=RrhWo%2FMXSgW7Uzvhwnl%2B%2Fg Please pass this on to potential candidates. And candidates who are interested in category theory, (homotopy) type theory, proof theory or constructive maths, should feel free to contact me. Best wishes, Benno -- 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/2c0e4b11-1859-4bde-bbaf-550c2f6115d4n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1426 bytes --]

~ Topos Institute Colloquium ~ Michael Shulman: Two-dimensional semantics of homotopy type theory Abstract: The general higher-categorical semantics of homotopy type theory involves (∞,1)-toposes and Quillen model categories. However, for many applications it suffices to consider (2,1)-toposes, which are reasonably concrete categorical objects built out of ordinary groupoids. In this talk I'll describe how to interpret homotopy type theory in (2,1)-toposes, and some of the applications we can get from such an interpretation. I will assume a little exposure to type theory, as in Dan Christensen's talk from April, but no experience with higher toposes or homotopy theory. This talk will also serve as an introduction to some basic notions of Quillen model categories. Time: May 27, 2021 05:00 PM Universal Time UTC (13:00 in PGH) Zoom: https://topos-institute.zoom.us/j/5344862882?pwd=Znh3UlUrek41T3RLQXJVRVNkM3Ewdz09 Meeting ID: 534 486 2882 Passcode: 65537 -- 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/787184CD-C528-4D0A-9281-BD576C12C2C6%40cmu.edu.

A PhD position [1] is open in the Programming Languages group [2] at TU Delft, in the area of HoTT/UF. The student will be supervised by Benedikt Ahrens [3]. Information about the position is available on the dedicated website [1]. If you have any questions or consider applying, please get in touch with Benedikt (benedikt.ahrens@gmail.com). [1] https://pl.ewi.tudelft.nl/hiring/2021/phd-student-hottuf/ [2] https://pl.ewi.tudelft.nl/ [3] https://benediktahrens.gitlab.io/ -- 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/8e3de31d-1bd7-0fd3-2192-53de73fedb25%40gmail.com.

Dear All, I am advertising a short (7 months) postdoc position with me. The job is physically located in Birmingham, UK, but can be done remotely. The starting date is flexible, but the end date is fixed at 28 February 2022 (which is the end of the project that funds this position). Background: the current post holder, Jacopo Emmenegger, is moving on to a prestigious fellowship [1]. The official advertisement and application form are located at [2]. For any questions, please contact me at b.ahrens@cs.bham.ac.uk . Best, Benedikt [1] https://kaw.wallenberg.org/en/jacopo-emmenegger [2] https://bham.taleo.net/careersection/external/jobdetail.ftl?job=210000PQ -- 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/808c01ba-ee2e-d8eb-e57a-a60dfd38e922%40gmail.com.

This is the Second Call for Contributions for the (Virtual) Workshop on Homotopy Type Theory and Univalent Foundations July 17-18, 2021, The Internet @ Buenos Aires, Argentina https://hott-uf.github.io/2021/ Co-located with FSCD 2021 https://fscd2021.dc.uba.ar/ Abstract submission deadline: May 25, 2021 Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Invited talks * Evan Cavallo (Carnegie Mellon University) * Peter LeFanu Lumsdaine (Stockholm University) * Anja Petkovic (University of Ljubljana) * Matthew Weaver (Princeton University) # Submissions * Abstract submission deadline: May 25, 2021 * Author notification: mid-June 2021 Submissions should consist of a title and an abstract, in pdf format, of no more than 2 pages, submitted via http://easychair.org/conferences/?conf=hottuf2021 Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. # Program committee * Benedikt Ahrens (University of Birmingham) * Carlo Angiuli (Carnegie Mellon University) * Paolo Capriotti (Technische Universität Darmstadt) * Floris van Doorn (University of Pittsburgh) * Favonia (University of Minnesota) * Eric Finster (University of Cambridge) * Chris Kapulkin (University of Western Ontario) * Paige Randall North (University of Pennsylvania) * Emily Riehl (Johns Hopkins University) * Christian Sattler (Chalmers University of Technology) * Andrew Swan (Carnegie Mellon University) # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario) -- 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/CAEXhy3OfN2r-zi0jTNyUzEpeH7-rrP%2BwrEhK5gB7WPNbm4y0dQ%40mail.gmail.com.

~~~ Bohemian Logical & Philosophical Café ~~~ Speaker: Michael Shulman Title: The derivator of setoids. May 4 at 16.00 Prague time (GMT+2) The zoom link is on the page: https://bohemianlpc.github.io -- 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/50A33FC8-D7FD-4B84-9BDB-D9868D2018E1%40cmu.edu.

~~~ Bohemian Logical & Philosophical Café ~~~ Speaker: Michael Shulman Title: The derivator of setoids. May 4 at 16.00 Prague time (GMT+1) The zoom link is on the page: https://bohemianlpc.github.io Abstract: Can homotopy theory be developed in constructive mathematics, or even in ZF set theory without the axiom of choice? Recent work inspired by homotopy type theory has yielded two constructive homotopy theories (simplicial sets and equivariant cubical sets) that are classically equivalent to that of spaces, but it is unknown if they are constructively equivalent to each other. If they are not, then which one is correct? Or are they both correct, or both incorrect? What do these questions even mean? I will propose one criterion for the correctness of a constructive homotopy theory of spaces: as a derivator, it should be the free cocompletion of a point. (A derivator is an enhancement of the homotopy category that remains 1-categorical, but can still express universal properties of this sort.) Then I will give some evidence that any such homotopy theory must have the curious property that its 1-truncation contains, not only sets, but also setoids. Specifically, the ex/lex completion of the category of sets defines a derivator that satisfies a relative version of the aforementioned universal property; thus it should be a localization of any derivator satisfying the absolute condition. This suggests that either setoids are an unavoidable aspect of constructive homotopy theory, or the criterion needs to be modified. -- 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/BEDBD6A8-A6FB-436F-AB1E-45162A257848%40cmu.edu.

*** Yorkshire and Midlands Category Theory Seminar *** Thursday 29th April, 2:00-5:30pm (UK time) *** via Zoom Dear all, I am pleased to announce the 24th meeting of the Yorkshire and Midlands Category Theory Seminar, to be held online on Thursday 29th April, 2:00-5:30pm (UK time). The program will be as follows: 2:00-3:00 Karol Szumilo (Leeds), Infty-groupoids in lextensive categories 3:00-4:00 Anna Laura Suarez (Universite’ Cote, d’Azur), The category of finitary biframes as the category of pointfree bispaces 4:00-5:00 Ivan Di Liberti (Czech Academy of Sciences), Formal model theory and Higher Topology. 5:00-5:30 Tea/coffee Please see below for abstracts. The Zoom link is Join Zoom Meeting: https://universityofleeds.zoom.us/j/88049499094?pwd=UEVyTEdDWnZyV2NNMGNwaTBaaDlSZz09 Meeting ID: 880 4949 9094 Passcode: Z*9qfq Please do not post the Zoom link on websites. With best regards, Nicola == Karol Szumilo (Leeds), Infty-groupoids in lextensive categories Abstract: I will discuss a construction of a new model structure on simplicial objects in a countably lextensive category (i.e., a category with well behaved finite limits and countable coproducts). This builds on previous work on a constructive model structure on simplicial sets, originally motivated by modelling Homotopy Type Theory, but now applicable in a much wider context. This is joint work with Nicola Gambino, Simon Henry and Christian Sattler. == Anna Laura Suarez (Universite’ Cote, d’Azur), The category of finitary biframes as the category of pointfree bispaces Bitopological spaces have found numerous applications: they appear naturally when dealing with uniform spaces (already introduced by Weil in [1]), as well as providing a particularly elegant view of Priestley duality (see [4], but also [3]). We explore the theory of finitary biframes, introduced in [5], as a category of pointfree bitopological spaces. In particular, we compare it to the existing theory of biframes ([2]) and the more recent one of d-frames ([4]). We illustrate some of the advantages that finitary biframes present when compared to both biframes and d-frames. One of the main strengths of the theory of finitary biframes is that for every finitary biframe L one may construct a finitary biframe A(L) whose main component is order-isomorphic to the collection of all quotients of L. [1] Andre', W. Sur les espaces a structure uniforme et sur la topologie generale / par Andre' Weil. Actualites scientifiques et industrielles. Hermann et cie, Paris, 1937. [2] Banaschewski, B., Brummer, G. C., and Hardie, K. A. Biframes and bispaces. Quaestiones Mathematicae 6, 1-3 (1983), 13–25. [3] Bezhanishvili, G., Bezhanishvili, N., Gabelaia, D., and Kurz, A. Bitopological duality for distributive lattices and Heyting algebras. Mathematical Structures in Computer Science 20, 3 (2010), 359–393. [4] Jung, A., and Moshier, M. A. On the bitopological nature of Stone duality. Tech. Rep. CSR-06-13, University of Birmingham, 2006. 110 pages. == Ivan Di Liberti (Czech Academy of Sciences), Formal model theory and Higher Topology. Abstract. Motivated by the abstract study of semantics, we study the interaction between topoi, accessible categories with directed colimits and ionads. This theory amounts to a categorification of famous construction from general topology: the Scott topology on a poset and the adjunction between locales and topological spaces. This technology is then used in order to establish syntax-semantics dualities. Among the significant contributions, we provide a logical understanding of ionads that encompasses Makkai ultracategories. References. PhD thesis, arXiv:2009.07320. General facts on the Scott Adjunction, ArXiv:2009.14023. Towards Higher Topology, ArXiv:2009.14145. Formal Model Theory & Higher Topology, ArXiv:2010.00319. == Dr Nicola Gambino Associate Professor in Pure Mathematics and Director of Research and Innovation School of Mathematics, University of Leeds Dr Nicola Gambino Associate Professor in Pure Mathematics and Director of Research and Innovation School of Mathematics, University of Leeds -- 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/1D982A50-EB3E-4D35-A5E3-1C0373ECB9B7%40leeds.ac.uk.

[-- Attachment #1: Type: text/plain, Size: 1443 bytes --] Dear all, I’m happy to announce that we’re recruiting for PhD students in HoTT (besides other topics) at Stockholm University, starting September 2021. Note that the deadline for applications is next Friday, 23 April — sorry I missed advertising it here sooner. Full details and application are through https://www.su.se/english/about-the-university/work-at-su/available-jobs/phd-student-positions-1.507588?rmpage=job&rmjob=14472&rmlang=UK Please let me know if you have any questions about the position! And (for advisors) please pass this on to any interested masters-level students. Answers to a few common questions: - PhD positions in Sweden are fully funded, with a livable salary. - The position includes up to 20% teaching. - Swedish speaking isn’t required, either formally or practically (though learning it during the PhD is encouraged) — all higher-level teaching is done in English, and most administrative business (including all necessities) can be. Best wishes, –Peter. -- 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/CAAkwb-%3DQCO9fw1BVjTtyihBphuoOaNbuviygm%2BaCMg8K5bTfjA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1985 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2102 bytes --] Dear all, A quick reminder of the researcher position in HoTT that I advertised a couple of weeks ago, with deadline this Friday (9 April). One point a couple of people asked about: Yes, this is effectively a postdoc — it’s formally called a “researcher” position here for administrative reasons. We are interested in applicants at any post-PhD stage (or expecting to complete their PhD before the position starts). Application link: https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=14506&rmlang=UK Once again, let me know if you have any questions! Best wishes, –Peter. On Mon, Mar 22, 2021 at 12:31 PM Peter LeFanu Lumsdaine < p.l.lumsdaine@gmail.com> wrote: > > Dear all, > > I’m pleased to announce that we’re hiring for a researcher position in Homotopy Type Theory at Stockholm University. It’s a 2 year position, provisionally starting this August, in the logic group of the Mathematics Department, supported by the Wallenberg Foundation project grant “Type Theory for Mathematics and Computer Science” (PI Thierry Coquand). The application deadline is 9 April. > > We welcome all applicants interested in working on homotopy type theory and related topics — either with previous background in HoTT, or with background in related fields but interested in moving into HoTT. > > Full details and application at > https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=14506&rmlang=UK > Departmental webpage: https://www.math.su.se > > Please get in touch with me if you have any questions about the position! > > Best, > –Peter. -- 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/CAAkwb-mW5%2BPShAxP1duTdB%2BFNZ-2Hfys%2BSEFDwWvv3gShMEPWg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2870 bytes --]

We are hiring lecturers / senior lecturers (corresponding to assistant / associate professors https://en.wikipedia.org/wiki/Senior_lecturer) at the School of Computer Science, University of Birmingham, UK. The official advert is here: https://bham.taleo.net/careersection/external/jobdetail.ftl?job=210000DX&tz=GMT%2B00%3A00&tzname=Europe%2FLondon In particular, applicants with interests close to our Theory Group are very welcome: https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-computation/index.aspx The interests of this group include, among other things, higher category theory, homotopy type theory, constructive mathematics, string diagrams and graphical calculi, proof assistants, topology and domain theory, game semantics, quantum computation, programming languages, verification and model checking, algorithms and complexity. Feel free to approach me or other members of the theory group for further information 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/7b586bcf-3906-e5ba-d68e-e533d779bfc3%40googlemail.com.

[-- Attachment #1: Type: text/plain, Size: 1332 bytes --] Dear all, I’m pleased to announce that we’re hiring for a researcher position in Homotopy Type Theory at Stockholm University. It’s a 2 year position, provisionally starting this August, in the logic group of the Mathematics Department, supported by the Wallenberg Foundation project grant “Type Theory for Mathematics and Computer Science” (PI Thierry Coquand). The application deadline is 9 April. We welcome all applicants interested in working on homotopy type theory and related topics — either with previous background in HoTT, or with background in related fields but interested in moving into HoTT. Full details and application at https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=14506&rmlang=UK Departmental webpage: https://www.math.su.se Please get in touch with me if you have any questions about the position! Best, –Peter. -- 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/CAAkwb-%3DHUbq3ucV4EMtshU37F8eefs6bAugDzcCo7N9ktLu2-Q%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1958 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3254 bytes --] We are hiring a research programmer at University of Minnesota to work with us on building next-generation proof assistant technology (broadly defined) based on homotopy type theory and cubical type theory. The ideal candidate would have some knowledge and interest in homotopy and cubical type theory, combined with concrete experience implementing type theoretic proof assistants using modern algorithms, such as bidirectional type checking and normalization-by-evaluation. You will be exposed to the latest research in the field and can get involved in theoretical development of the research ideas. We welcome applicants who do not have a Ph.D. degree---a BA/BS degree is sufficient. The research project is funded by the AFOSR through their MURI program, and your official affiliation would be the University of Minnesota with Favonia being your supervisor. However, you will frequently meet and collaborate with other researchers from Carnegie Mellon University, Wesleyan University, University of San Diego, and other institutions. Especially during the COVID-19 pandemic, most activities will be online, though you will have to be physically in the US. (We may be able to sponsor visas. Contact Favonia <kbh@umn.edu> for details.) We are interviewing candidates on a rolling basis until a match is found. Candidates applying by the end of March (2021/3/31) would be given priority. Here is the official link for application: https://hr.myu.umn.edu/jobs/ext/339220 Please also drop an email to Favonia <kbh@umn.edu> so that we can confirm that your application correctly enters the system. If you are a current employee of the University of Minnesota, please use https://hr.myu.umn.edu/jobs/int/339220 instead. # Some further information - What is the annual salary? About $60,000 USD. - When is the expected start date? As soon as you are ready. - How long does this position last? The position will last as long as the project can support it and benefit from it. However, the expectation is that you will be in this position around 1-3 years (negotiable) and may choose to leave early (for example, to start a Ph.D.). Your official contract will be one-year but renewable. - I see that there’s a “work experience” requirement. What counts as “work experience”? This requirement exists to satisfy an administrative requirement of the job code at the University of Minnesota. We will recognize a wide range of activities as “work experience”, such as contributions on GitHub during weekends. **Please document related activities in your CV.** If you are not sure if something counts as work experience, please ask Favonia <kbh@umn.edu >. - I have more questions! Please send an email to Favonia <kbh@umn.edu>. Best, Favonia they/them/theirs -- 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/CAH_%2Brvc0nayUNeSQvprodnpdQTfuXSLHeEicWTddRUhFRSDSxA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 11177 bytes --]

[-- Attachment #1: Type: text/plain, Size: 9747 bytes --] I remember multiple people (including me) discovered relatively short proofs. Some history on GitHub: https://github.com/HoTT/book/issues/27 Best, Favonia they/them/theirs On Mon, Mar 8, 2021 at 10:54 AM Egbert Rijke <e.m.rijke@gmail.com> wrote: > My agda file with the the interchange laws and EH is here > > https://github.com/HoTT-Intro/Agda/blob/master/extra/interchange.agda > > And the coherence law is here > > https://github.com/HoTT-Intro/Agda/blob/master/extra/syllepsis.agda > > For anyone who is interested. > > On Mon, Mar 8, 2021 at 5:38 PM Kristina Sojakova < > sojakova.kristina@gmail.com> wrote: > >> If I'm not mistaken, Favonia also found a very short proof of EH some >> years ago. >> >> 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/8de81acf-3a00-ae98-7003-9eaf404d0b89%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/CAGqv1ODEzmBLWmOvgVmtBO7D_xttUKDW6NSNF2Q2_3K7wfYcCA%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODEzmBLWmOvgVmtBO7D_xttUKDW6NSNF2Q2_3K7wfYcCA%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/CAH_%2Brvd184QS__yNafR5835opTA6DiZ1Wy%2BuGsDKp3%3DtG0TWPw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 14604 bytes --]

[-- Attachment #1: Type: text/plain, Size: 8683 bytes --] My agda file with the the interchange laws and EH is here https://github.com/HoTT-Intro/Agda/blob/master/extra/interchange.agda And the coherence law is here https://github.com/HoTT-Intro/Agda/blob/master/extra/syllepsis.agda For anyone who is interested. On Mon, Mar 8, 2021 at 5:38 PM Kristina Sojakova < sojakova.kristina@gmail.com> wrote: > If I'm not mistaken, Favonia also found a very short proof of EH some > years ago. > > 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/8de81acf-3a00-ae98-7003-9eaf404d0b89%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/CAGqv1ODEzmBLWmOvgVmtBO7D_xttUKDW6NSNF2Q2_3K7wfYcCA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 13031 bytes --]

If I'm not mistaken, Favonia also found a very short proof of EH some years ago. 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/8de81acf-3a00-ae98-7003-9eaf404d0b89%40gmail.com.

Is there a geometric interpretation for the proof I gave? On 3/8/21 5:25 PM, Dan Christensen wrote: > On Mar 8, 2021, Egbert Rijke <e.m.rijke@gmail.com> wrote: > >> 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. > In case anyone wants to play with this in Coq, in this branch > > https://github.com/jdchristensen/HoTT/tree/Hurewicz > > the file Smashing.v contains similar facts, e.g. pmagma_loops_shuffle. > (But no coherence law is proved.) > > Dan > -- 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/c4d0d50f-8a11-3d63-7c32-3fa3aae1fd96%40gmail.com.

On Mar 8, 2021, Egbert Rijke <e.m.rijke@gmail.com> wrote: > 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. In case anyone wants to play with this in Coq, in this branch https://github.com/jdchristensen/HoTT/tree/Hurewicz the file Smashing.v contains similar facts, e.g. pmagma_loops_shuffle. (But no coherence law is proved.) Dan -- 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/87pn09ipd5.fsf%40uwo.ca.

[-- Attachment #1: Type: text/plain, Size: 15384 bytes --] Thanks Egbert, I think it will be useful to have both proofs, as they offer different insights. On 3/8/21 4:46 PM, Egbert Rijke wrote: > 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 > <mailto: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 > <mailto: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 > <mailto: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 > <mailto: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 <mailto: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 > <mailto: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 > <mailto: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 > <mailto: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 > <mailto:HomotopyTypeTheory%2Bunsubscribe@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 > <mailto:HomotopyTypeTheory%2Bunsubscribe@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 > <mailto:HomotopyTypeTheory%2Bunsubscribe@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 > <mailto: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/d0c29b9f-842a-f418-4c76-df1f040c422e%40gmail.com. [-- Attachment #2: Type: text/html, Size: 23388 bytes --]

[-- 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 --]

[-- Attachment #1: Type: text/plain, Size: 9764 bytes --] 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. [-- Attachment #2: Type: text/html, Size: 14047 bytes --]