[-- Attachment #1.1: Type: text/plain, Size: 7318 bytes --] SIXTH SYMPOSIUM ON COMPOSITIONAL STRUCTURES (SYCO 6) -- including a Category Theory PhD Recruitment Fair -- University of Leicester, UK 16-17 December, 2019 http://events.cs.bham.ac.uk/syco/6/ The Symposium on Compositional Structures (SYCO) is an interdisciplinary series of meetings aiming to support the growing community of researchers interested in the phenomenon of compositionality, from both applied and abstract perspectives, and in particular where category theory serves as a unifying common language. Previous SYCO events have been held at University of Birmingham, University of Strathclyde, University of Oxford, and Chapman University. We welcome submissions from researchers across computer science, mathematics, physics, philosophy, and beyond, with the aim of fostering friendly discussion, disseminating new ideas, and spreading knowledge between fields. Submission is encouraged for both mature research and work in progress, and by both established academics and junior researchers, including students. Submission is easy, with no format requirements or page restrictions. The meeting does not have proceedings, so work can be submitted even if it has been submitted or published elsewhere. Think creatively--- you could submit a recent paper, or notes on work in progress, or even a recent Masters or PhD thesis. While no list of topics could be exhaustive, SYCO welcomes submissions with a compositional focus related to any of the following areas, in particular from the perspective of category theory: - logical methods in computer science, including classical and quantum programming, type theory, concurrency, natural language processing and machine learning; - graphical calculi, including string diagrams, Petri nets and reaction networks; - languages and frameworks, including process algebras, proof nets, type theory and game semantics; - abstract algebra and pure category theory, including monoidal category theory, higher category theory, operads, polygraphs, and relationships to homotopy theory; - quantum algebra, including quantum computation and representation theory; - tools and techniques, including rewriting, formal proofs and proof assistants, and game theory; - industrial applications, including case studies and real-world problem descriptions. This new series aims to bring together the communities behind many previous successful events which have taken place over the last decade, including "Categories, Logic and Physics", "Categories, Logic and Physics (Scotland)", "Higher-Dimensional Rewriting and Applications", "String Diagrams in Computation, Logic and Physics", "Applied Category Theory", "Simons Workshop on Compositionality", and the "Peripatetic Seminar in Sheaves and Logic". SYCO is a regular fixture in the academic calendar, running regularly throughout the year, and becoming over time a recognized venue for presentation and discussion of results in an informal and friendly atmosphere. To help create this community, and to avoid the need to make difficult choices between strong submissions, in the event that more good-quality submissions are received than can be accommodated in the timetable, the programme committee may choose to *defer* some submissions to a future meeting, rather than reject them. This would be done based largely on submission order, giving an incentive for early submission, but would also take into account other requirements, such as ensuring a broad scientific programme. Deferred submissions can be re-submitted to any future SYCO meeting, where they would not need peer review, and where they would be prioritised for inclusion in the programme. This will allow us to ensure that speakers have enough time to present their ideas, without creating an unnecessarily competitive reviewing process. Meetings will be held sufficiently frequently to avoid a backlog of deferred papers. # INVITED SPEAKERS Gabriella Bohm, Wigner Research Centre for Physics Jennifer Hackett, University of Nottingham # PhD RECRUITMENT FAIR This event will include a poster session advertising PhD opportunities in category theory and related disciplines. If you are interested in advertising PhD opportunities at your institution, please email Simona Paoli at <sp424@leicester.ac.uk>. We expect significant participation from Masters students and final-year undergraduates who are considering further study in this area. # ACCEPTED PAPERS Dorette Pronk and Laura Scull - New Results on Bicategories of Fractions Applied to Orbifolds Amar Hadzihasanovic - Representable diagrammatic sets as a model of weak higher categories Drew Moshier and Steve Vickers - Cartesian bicategories and their Karoubi envelopes Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski and Fabio Zanasi - Contextual Equivalence for Signal Flow Graphs (Extended Abstract) Vincent Wang - Graphical Grammar + Graphical Completion of Monoidal Categories John Stell - Mathematical Morphology on Graphs: The role of relations on hypergraphs Quanlong Wang - An algebraic axiomatisation of ZX-calculus Morgan Rogers and Jens Hemelaer Monoid Properties as Topos-Theoretic Invariants Maaike Zwart and Dan Marsden - Composite Theories, and how to use them to prove no-go theorems for distributive laws Louis Parlant - Monoidal Monads and Preservation of Equations Callum Reader - Probability Monads for Enriched Categories Guillaume Boisseau - String diagrams for optics Dan Shiebler, Alexis Toumi and Mehrnoosh Sadrzadeh - Incremental Monoidal Grammars # IMPORTANT DATES Registration deadline: Monday 9th December 2019 Symposium dates: Monday 16th and Tuesday 17th December 2019 # Programme Committee Miriam Backens, University of Birmingham Nicolas Behr, Institut de Recherche en Informatique Fondamentale (IRIF), Universite Paris-Diderot - Paris 7 Carmen Maria Constantin, University of Oxford Chris Heunen, University of Edinburgh, Dominic Horsman, University of Grenoble Aleks Kissinger, University of Oxford Eliana Lorch, Thiel Fellowship Dan Marsden, University of Oxford (PC Chair) Samuel Mimram, Ecole Polytechnique Koko Muroya, RIMS, Kyoto University & University of Birmingham Simona Paoli, University of Leicester Mehrnoosh Sadrzadeh, University College London Alessio Santamaria, Queen Mary University of London Alexandra Silva, University College London Pawel Sobocinski, Tallinn University of Technology Jamie Vicary, University of Birmingham and University of Oxford Philip Zahn, University of St Gallen Tamara von Glehn # Steering Committee Ross Duncan, University of Strathclyde Chris Heunen, University of Edinburgh Dominic Horsman, University of Grenoble Alek Kissinger, University of Oxford Samuel Mimram, Ecole Polytechnique Simona Paoli, University of Leicester Mehrnoosh Sadrzadeh, University College London Pawel Sobocinski, Tallinn University of Technology Jamie Vicary, University of Birmingham and University of Oxford -- 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/4000b3ab-8717-4aaa-9157-74ef41d568a7%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 9341 bytes --] <div dir="ltr"><div>SIXTH SYMPOSIUM ON COMPOSITIONAL STRUCTURES (SYCO 6)</div><div>-- including a Category Theory PhD Recruitment Fair --</div><div><br></div><div>University of Leicester, UK</div><div> 16-17 December, 2019</div><div><br></div><div> http://events.cs.bham.ac.uk/syco/6/</div><div><br></div><div>The Symposium on Compositional Structures (SYCO) is an</div><div>interdisciplinary series of meetings aiming to support the growing</div><div>community of researchers interested in the phenomenon of</div><div>compositionality, from both applied and abstract perspectives, and in</div><div>particular where category theory serves as a unifying common language.</div><div>Previous SYCO events have been held at University of Birmingham,</div><div>University of Strathclyde, University of Oxford, and Chapman University.</div><div><br></div><div>We welcome submissions from researchers across computer science,</div><div>mathematics, physics, philosophy, and beyond, with the aim of</div><div>fostering friendly discussion, disseminating new ideas, and spreading</div><div>knowledge between fields. Submission is encouraged for both mature</div><div>research and work in progress, and by both established academics and</div><div>junior researchers, including students.</div><div><br></div><div>Submission is easy, with no format requirements or page restrictions.</div><div>The meeting does not have proceedings, so work can be submitted even</div><div>if it has been submitted or published elsewhere. Think creatively---</div><div>you could submit a recent paper, or notes on work in progress, or even</div><div>a recent Masters or PhD thesis.</div><div><br></div><div>While no list of topics could be exhaustive, SYCO welcomes submissions</div><div>with a compositional focus related to any of the following areas, in</div><div>particular from the perspective of category theory:</div><div><br></div><div>- logical methods in computer science, including classical and</div><div>quantum programming, type theory, concurrency, natural language</div><div>processing and machine learning;</div><div><br></div><div>- graphical calculi, including string diagrams, Petri nets and</div><div>reaction networks;</div><div><br></div><div>- languages and frameworks, including process algebras, proof nets,</div><div>type theory and game semantics;</div><div><br></div><div>- abstract algebra and pure category theory, including monoidal</div><div>category theory, higher category theory, operads, polygraphs, and</div><div>relationships to homotopy theory;</div><div><br></div><div>- quantum algebra, including quantum computation and representation</div><div>theory;</div><div><br></div><div>- tools and techniques, including rewriting, formal proofs and proof</div><div>assistants, and game theory;</div><div><br></div><div>- industrial applications, including case studies and real-world</div><div>problem descriptions.</div><div><br></div><div>This new series aims to bring together the communities behind many</div><div>previous successful events which have taken place over the last</div><div>decade, including "Categories, Logic and Physics", "Categories, Logic</div><div>and Physics (Scotland)", "Higher-Dimensional Rewriting and</div><div>Applications", "String Diagrams in Computation, Logic and Physics",</div><div>"Applied Category Theory", "Simons Workshop on Compositionality", and</div><div>the "Peripatetic Seminar in Sheaves and Logic".</div><div><br></div><div>SYCO is a regular fixture in the academic calendar, running</div><div>regularly throughout the year, and becoming over time a recognized</div><div>venue for presentation and discussion of results in an informal and</div><div>friendly atmosphere. To help create this community, and to avoid the</div><div>need to make difficult choices between strong submissions, in the</div><div>event that more good-quality submissions are received than can be</div><div>accommodated in the timetable, the programme committee may choose to</div><div>*defer* some submissions to a future meeting, rather than reject them.</div><div>This would be done based largely on submission order, giving an</div><div>incentive for early submission, but would also take into account other</div><div>requirements, such as ensuring a broad scientific programme. Deferred</div><div>submissions can be re-submitted to any future SYCO meeting, where they</div><div>would not need peer review, and where they would be prioritised for</div><div>inclusion in the programme. This will allow us to ensure that speakers</div><div>have enough time to present their ideas, without creating an</div><div>unnecessarily competitive reviewing process. Meetings will be held</div><div>sufficiently frequently to avoid a backlog of deferred papers.</div><div><br></div><div># INVITED SPEAKERS</div><div><br></div><div>Gabriella Bohm, Wigner Research Centre for Physics</div><div>Jennifer Hackett, University of Nottingham</div><div><br></div><div># PhD RECRUITMENT FAIR</div><div><br></div><div>This event will include a poster session advertising PhD opportunities</div><div>in category theory and related disciplines. If you are interested in</div><div>advertising PhD opportunities at your institution, please email Simona</div><div>Paoli at <sp424@leicester.ac.uk>. We expect significant participation</div><div>from Masters students and final-year undergraduates who are</div><div>considering further study in this area.</div><div><br></div><div># ACCEPTED PAPERS</div><div><br></div><div>Dorette Pronk and Laura Scull - New Results on Bicategories of Fractions Applied to Orbifolds</div><div>Amar Hadzihasanovic - Representable diagrammatic sets as a model of weak higher categories</div><div>Drew Moshier and Steve Vickers - Cartesian bicategories and their Karoubi envelopes</div><div>Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski and Fabio Zanasi - Contextual Equivalence for Signal Flow Graphs (Extended Abstract)</div><div>Vincent Wang - Graphical Grammar + Graphical Completion of Monoidal Categories</div><div>John Stell - Mathematical Morphology on Graphs: The role of relations on hypergraphs</div><div>Quanlong Wang - An algebraic axiomatisation of ZX-calculus</div><div>Morgan Rogers and Jens Hemelaer<span style="white-space:pre"> </span>Monoid Properties as Topos-Theoretic Invariants</div><div>Maaike Zwart and Dan Marsden - Composite Theories, and how to use them to prove no-go theorems for distributive laws</div><div>Louis Parlant - Monoidal Monads and Preservation of Equations</div><div>Callum Reader - Probability Monads for Enriched Categories</div><div>Guillaume Boisseau - String diagrams for optics</div><div>Dan Shiebler, Alexis Toumi and Mehrnoosh Sadrzadeh - Incremental Monoidal Grammars</div><div><br></div><div># IMPORTANT DATES</div><div><br></div><div>Registration deadline: Monday 9th December 2019</div><div>Symposium dates: Monday 16th and Tuesday 17th December 2019</div><div><br></div><div># Programme Committee</div><div><br></div><div>Miriam Backens, University of Birmingham</div><div>Nicolas Behr, Institut de Recherche en Informatique Fondamentale (IRIF), Universite Paris-Diderot - Paris 7</div><div>Carmen Maria Constantin, University of Oxford</div><div>Chris Heunen, University of Edinburgh,</div><div>Dominic Horsman, University of Grenoble</div><div>Aleks Kissinger, University of Oxford</div><div>Eliana Lorch, Thiel Fellowship</div><div>Dan Marsden, University of Oxford (PC Chair)</div><div>Samuel Mimram, Ecole Polytechnique</div><div>Koko Muroya, RIMS, Kyoto University & University of Birmingham</div><div>Simona Paoli, University of Leicester</div><div>Mehrnoosh Sadrzadeh, University College London</div><div>Alessio Santamaria, Queen Mary University of London</div><div>Alexandra Silva, University College London</div><div>Pawel Sobocinski, Tallinn University of Technology</div><div>Jamie Vicary, University of Birmingham and University of Oxford</div><div>Philip Zahn, University of St Gallen</div><div>Tamara von Glehn</div><div><br></div><div># Steering Committee</div><div><br></div><div>Ross Duncan, University of Strathclyde</div><div>Chris Heunen, University of Edinburgh</div><div>Dominic Horsman, University of Grenoble</div><div>Alek Kissinger, University of Oxford</div><div>Samuel Mimram, Ecole Polytechnique</div><div>Simona Paoli, University of Leicester</div><div>Mehrnoosh Sadrzadeh, University College London</div><div>Pawel Sobocinski, Tallinn University of Technology</div><div>Jamie Vicary, University of Birmingham and University of Oxford</div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/4000b3ab-8717-4aaa-9157-74ef41d568a7%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/4000b3ab-8717-4aaa-9157-74ef41d568a7%40googlegroups.com</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 3295 bytes --] Probably just for amusement only. (1) In the category of topological spaces (not up to homotopy), if X and Y are exponentiable and we topologize the space (X ≃ Y) of homeomorphisms of X and Y with the subspace topology, we get that co-derived-set (Y+1) × (X ≃ Y) ≃ (X+1 ≃ Y+1). The proof relies on classical logic. Exponentiability is only needed to make sense of (X ≃ Y) as a space, and hence we could alternatively work with compactly generated spaces, which have all exponentials, but I haven't checked the above in that case (yet). The derived set, in the sense of Cantor, is the set of limit points. Here we consider its complement, with the subspace topology, which of course is the discrete topology. When X is the same space as Y, the above specializes to co-derived-set (X+1) × Aut X ≃ Aut (X+1), where Aut X is the space of auto (homeo)morphisms of X. Hence when X is discrete, so that it is its own coderived set, the above specializes to the "factorial equation" (X+1) × Aut X ≃ Aut (X+1). But if X is perfect in the sense of Cantor (has no isolated points), then instead we get Aux X = Aut (X+1) because the coderived set of X+1 is homeomorphic to 1. (2) The above holds if we replace "space" by "homotopy type" and can be proved in HoTT/UF, *this time without appealing to classical logic* (and I doubt appealing to classical logic can simplify the argument, because the argument seems to be as simple and direct as it can be). For this, we need the following definitions in HoTT/UF: * A point x is *isolated* if the type x=y is decidable for all y:X. (Counter-example: any point of the circle.) * A type is *discrete* if all its points are isolated. (Example: natural numbers, the finite type Fin n with n elements.) * A space is *perfect* if it has no isolated points. (Example: the circle.) There is also a notion that doesn't arise above but that does arise in the proofs/constructions: * A point x is *h(omotopy)-isolated* if the type x=y is a proposition, or a subsingleton, for every point y. By local Hedberg, every isolated point is h-isolated. (3) In particular, if Fin n is the type with n elements, Fin (n+1) × Aut (Fin n) ≃ Aut (Fin (n+1)) from which we get Fin (n!) ≃ Aut (Fin n) by induction on n, as expected. (4) Although the above development uses HoTT/UF ideas crucially, only function extensionality is needed to carry out the constructions and proofs (in particular, propositional extensionality and univalence are not needed). I had fun formalizing the above ideas in Agda: https://www.cs.bham.ac.uk/~mhe/agda-new/UF-Factorial.html https://www.cs.bham.ac.uk/~mhe/agda-new/ArithmeticViaEquivalence.html and so I wanted to share it here. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 4449 bytes --] <div dir="ltr"><div>Probably just for amusement only.</div><div><br></div><div>(1) In the category of topological spaces (not up to homotopy), if X and Y are exponentiable and we topologize the space (X ≃ Y) of homeomorphisms of X and Y with the subspace topology, we get that</div><div><br></div><div> co-derived-set (Y+1) × (X ≃ Y) ≃ (X+1 ≃ Y+1).</div><div><br></div><div>The proof relies on classical logic.</div><div><br></div><div>Exponentiability is only needed to make sense of (X ≃ Y) as a space, and hence we could alternatively work with compactly generated spaces, which have all exponentials, but I haven't checked the above in that case (yet).</div><div><br></div><div>The derived set, in the sense of Cantor, is the set of limit points. Here we consider its complement, with the subspace topology, which of course is the discrete topology.</div><div><br></div><div>When X is the same space as Y, the above specializes to </div><div><br></div><div> co-derived-set (X+1) × Aut X ≃ Aut (X+1),</div><div><br></div><div>where Aut X is the space of auto (homeo)morphisms of X.</div><div><br></div><div>Hence when X is discrete, so that it is its own coderived set, the above specializes to the "factorial equation"</div><div><br></div><div> (X+1) × Aut X ≃ Aut (X+1).</div><div><br></div><div>But if X is perfect in the sense of Cantor (has no isolated points), then instead we get </div><div><br></div><div> Aux X = Aut (X+1)</div><div><br></div><div>because the coderived set of X+1 is homeomorphic to 1.</div><div><br></div><div>(2) The above holds if we replace "space" by "homotopy type" and can be proved in HoTT/UF, *this time without appealing to classical logic* (and I doubt appealing to classical logic can simplify the argument, because the argument seems to be as simple and direct as it can be).</div><div><br></div><div>For this, we need the following definitions in HoTT/UF:</div><div><br></div><div> * A point x is *isolated* if the type x=y is decidable for all y:X.</div><div> (Counter-example: any point of the circle.)</div><div><br></div><div> * A type is *discrete* if all its points are isolated.</div><div> (Example: natural numbers, the finite type Fin n with n elements.)</div><div><br></div><div> * A space is *perfect* if it has no isolated points.</div><div> (Example: the circle.)</div><div><br></div><div>There is also a notion that doesn't arise above but that does arise in the proofs/constructions:</div><div><br></div><div> * A point x is *h(omotopy)-isolated* if the type x=y is a proposition, </div><div> or a subsingleton, for every point y. </div><div><br></div><div> By local Hedberg, every isolated point is h-isolated.</div><div><br></div><div><br></div><div>(3) In particular, if Fin n is the type with n elements, </div><div><br></div><div> Fin (n+1) × Aut (Fin n) ≃ Aut (Fin (n+1))</div><div><br></div><div>from which we get</div><div><br></div><div> Fin (n!) ≃ Aut (Fin n)</div><div><br></div><div>by induction on n, as expected.</div><div><br></div><div>(4) Although the above development uses HoTT/UF ideas crucially, only function extensionality is needed to carry out the constructions and proofs (in particular, propositional extensionality and univalence are not needed).</div><div><br></div><div>I had fun formalizing the above ideas in Agda:</div><div><br></div><div> https://www.cs.bham.ac.uk/~mhe/agda-new/UF-Factorial.html</div><div> https://www.cs.bham.ac.uk/~mhe/agda-new/ArithmeticViaEquivalence.html</div><div><br></div><div>and so I wanted to share it here.</div><div><br></div><div>Best,</div><div>Martin</div><div><br></div><div><br></div><div> </div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googlegroups.com</a>.<br />

Thank you Kevin, for taking the time to write this very detailed response. After taking a look at your original approach and the improved one of your student, I am under the impression that the difficulties you encountered actually had little to do with the proof assistant you were working in. Perhaps this impression is just uninformed, and e.g. in a system based on cubical type theory these problems would disappear. Of course, the only way to tell is to go ahead and formalize this result in such a system. But to me it seems that the "commutative diagram hell" you faced really stems from an issue that already exists within mathematics, namely the two conflicting viewpoints on localization: viewing it as a property (the honest viewpoint) or viewing it as an operation (the convenient illusion). As far as I understood, in your original approach you proved the "standard affine covering lemma" (https://stacks.math.columbia.edu/tag/00EJ) under the operational viewpoint, making it nontrivial to apply this lemma to "nonstandard" localizations, whereas your student proved the lemma under the property viewpoint, i.e. for "all" localizations at the same time. To a "proper" mathematician this distinction must seem silly, and if he doesn't outright dismiss it as fruitless philosophical nonsense, he will most likely claim that one can safely pretend it doesn't exist due to "existence of canonical isomorphisms yada yada yada". And yet, even the (presumably "proper") author(s) of https://stacks.math.columbia.edu/tag/01HR somehow felt the need to justify the application of lemma 10.23.1 with a sentence like "[...] and hence we can rewrite this sequence as the sequence [...]", which seems to admit the issue. Thus instead of pathologies, one may view the difficulties arising in formalization as merely pointing out existing gaps in the proper mathematician's operational theory, that he can in principle fill out all the details in his proofs to arbitrary precision. This problem and its solution remind me of something I encountered a few years ago, when I tried to convince myself of the well-known fact that the abstract braid group B(W) := < T_w for w \in W | \ell(w) + \ell(w') = \ell(ww') \Rightarrow T_w T_{w'} = T_{ww'} > attached to a finite reflection group W can be viewed as the fundamental group of its complexified hyperplane complement X. My ambition was only to explicitly construct the map \rho: B(W) --> \pi_1(X,x_0), but even that turned out to be more difficult than expected. The first naive attempt---of writing down explicit representative paths in the classes \rho(T_w) and proving that these satisfy the "braid relations" up to homotopy---was completely impractical. In fact, even writing down representative paths seemed not merely difficult but hopeless. Eventually I realized that the solution is to attach to a generator T_w not a representative (operational viewpoint) but a canonical subspace of the path-space (property viewpoint), showing that the latter is contractible and that the collection of these subspaces satisfy the braid relations (in the obvious sense). After that realization, everything was completely straightforward. -- Nicolas Am 24.11.19 um 19:11 schrieb Kevin Buzzard: > > Kevin, I would like to second Michael's interest in seeing these 20 > commutative diagrams. Moreover, I'd also be very interested in seeing > your "spaghetti code" (quote from the slides of your Big Proof > talk): it > seems it should be informative to see where your initial approach went > wrong, and how much these problems and their solution had anything > to do > at all with the formal system you were working in. Are your original > files perhaps available somewhere? > > > Sorry for the delay. > > My original repo with a "bad" theorem is here: > > https://github.com/kbuzzard/lean-stacks-project > > The bad theorem is this: > > https://stacks.math.columbia.edu/tag/00EJ > > The problem is that the rings denoted R_{f_i} (localisations of rings) > are typically defined to mathematicians as "this explicit construction > here" as opposed to "the unique up to unique isomorphism ring having > some explicit property" and, as a mathematician, I formalised (or more > precisely got Imperial College maths undergraduates Chris Hughes and > Kenny Lau to formalise) the explicit construction of the localisation > and then the explicit theorem as stated in the stacks project, not > understanding at the time that this would lead to trouble. When I came > to apply it, I ran into the issue that on this page > > https://stacks.math.columbia.edu/tag/01HR > > we have the quote: "If f, g in R are such that D(f)=D(g), then by > Lemma 26.5.1 there are canonical maps M_f->M_g and M_g->M_f which are > mutually inverse. Hence [we can regard M_f and M_g as equal]". > > This is a typical mathematician's usage of the word "canonical" -- it > means "I give you my mathematician's guarantee that I will never do > anything to M_f which won't work in exactly the same way as M_g so you > can replace one by the other and I won't mind". > > As I explained earlier, by the time I noticed this subtlety it was too > late, and this led to this horrorshow: > > https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268 > > plus the lines following, all of which is applied here > > https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208 > > . That last link is justifying a whole bunch of rewrites along > canonical isomorphisms. These were the general lemmas I needed to > prove that if A -> B was a map, and if A was canonically isomorphic to > A' and if B was canonically isomorphic to B' and A' -> B' was the > corresponding map, then the image of A was canonically isomorphic to > the image of A' etc, all in some very specific situation where > "canonically isomorphic" was typically replaced by "unique isomorphism > satisfying this list of properties". Note that this is crappy old code > written by me when I had no idea what I was doing. One very > interesting twist was this: the universal property of localisation for > the localised ring R_f is a statement which says that under certain > circumstances there is a unique ring homomorphism from R_f; however in > https://stacks.math.columbia.edu/tag/00EJ the map beta in the > statement of the lemma is *not* a ring homomorphism and so a naive > application the universal property was actually *not enough*! One has > to reformulate the lemma in terms of equalisers of ring homomorphisms > and remove mention of beta. None of this is mentioned in the stacks > project website because we are covered by the fact that everything is > "canonical" so it's all bound to work -- and actually this is *true* > -- we are very good at using this black magic word. > > All of this is fixed in Ramon Mir's MSc project > > https://github.com/ramonfmir/lean-scheme > > and the explanations of how it was fixed are in his write-up here > > https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf > > Briefly, one crucial input was that the localisation map R -> R_f > could be characterised up to unique isomorphism in the category of > R-algebras by something far more concrete than the universal property, > and Ramon used this instead. > > In HoTT one might naively say that these problems would not arise > because isomorphic things are equal. However my *current* opinion is > that it is not as easy as this, because I believe that the correct > "axiom" is that "canonically" isomorphic objects are equal and that > the HoTT axiom is too strong. I developed some rather primitive tools > to rewrite certain statements along certain kinds of isomorphisms with > some naturality properties, and mathematicians would be happy with > these ideas. I can quite believe that if you stick to homotopy types > with the model in your mind as being topological spaces up to homotopy > then the HoTT axiom is perfect. However there are things other than > topological spaces in mathematics, for example commutative rings, and > in my mind the HoTT axiom just looks weird and wrong in ring theory, > and I expect it to backfire when HoTT people start doing some serious > ring theory. I might be wrong. Part of me hopes I'm wrong, in fact. > But this will remain my opinion until someone comes along and > formalises the definition of a scheme in one of the HoTT theories and > proves the "theorem" that an affine scheme is a scheme (I write > "theorem" in quotes because it is a construction, not a theorem). I > had the pleasure of meeting Thorsten Altenkirch earlier this week and > I asked him why this had not been done yet, and he told me that they > were just waiting for the right person to come along and do it. A year > or so ago I was of the opinion that more mathematicians should be > using Lean but now I have come to the conclusion that actually more > mathematicians should be engaging with *all* of the theorem provers, > so we can find out which provers are the most appropriate for which > areas. By "mathematicians" here I really mean my ugly phrase "proper > mathematicians", i.e. people doing algebra/number > theory/geometry/topology etc, people who have absolutely no idea what > a type is and would even struggle to list the axioms of set theory. > These people with their "canonical" constructions (a phrase which has > no meaning) are the problem, and they're very hard to reach because > currently these systems offer them nothing they need. I wrote a silly game > > http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ > > to help my 1st years revise for my exam (and the game takes things > much further than the contents of the course), and I'm writing a real > number game too, to help my 1st years revise analysis for their > January exam. It would not be hard to write analogous such games in > one of the HoTT theories, I would imagine. > > From what I have seen, it seems to me that Isabelle is a fabulous tool > for classical analysis, Coq is great for finite group theory, the > Kepler conjecture is proved in other HOL systems, and the HoTT systems > are great for the theory of topological spaces up to homotopy. But > number theory has been around for millennia and unfortunately uses > analysis, group theory and topological spaces, and I want one system > which can do all of them. I think that we can only find out the > limitations of these systems by doing a whole bunch of "proper > mathematics" in all of them. I think it's appalling that none of them > can even *state* the Hodge conjecture, for example. For me, that is a > very simple reason for a "proper mathematician" to immediately reject > all of them in 2019. But I digress. > > Kevin > > > > -- > > Nicolas > > > > > -- > 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/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz. > -- 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/c25dfb49-6b6e-d926-f8c3-4c590ca6f507%40fromzerotoinfinity.xyz.

I find the wide variety of opinions as to the meaning of "canonical" to be evidence for my contention that the notion is not formalizable. (-: Personally, I feel that the closest semiformal approximation to a "canonical" isomorphism is one that's declared as a coercion. -- 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/CAOvivQzEF4sqoKtaRNVA_wN-vfEDV3UEzE0U1E%2B9i0jbjpHC_Q%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 7827 bytes --] So writing "x = y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. Two mathematical objects are equal if they have the same properties. This is exactly what equals means in HoTT and hence we should use the same symbol and call it equality. Everything else is confusing especially for the newcomer: “we have something in HoTT which is basically equality but we call it by a different name and we use a different symbol”??? Yes, it is different because equality of structures is not a proposition but a structure. But to insist that equality of structure is a proposition is just a confusion of conventional Mathematics. Independent of conventional Mathematics there is something like a naïve idea of equality which is preformal. And equality in HoTT is just a way to make this preformal notion precise. And why is it so strange to say there is more than one way to objects can be equal? As far is the notion of “canonical isomorphism”, Kevin is interested in, is concerned, I think this is an intensional aspect of an equality and hence not expressible within HoTT. E.g. 3+4 and 7 are the same natural number but 7 is canonical. Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo.martin@gmail.com> Date: Tuesday, 26 November 2019 at 19:15 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: HoTT instead expands the notion of "equality" to essentially mean "isomorphism" and requires transporting along it as a nontrivial action. I doubt that that's what you have in mind, but maybe you could explain what you do mean? I think terminology and notation alone cause a lot of confusion (and I have said this many times in this list in the past, before Kevin joined in). Much of the disagreement is not a real disagreement but a misunderstanding. * In HoTT, or in univalent mathematics, we use the terminology "equals" and the notation "=" for something that is not the same notion as in "traditional mathematics". * Before the univalence axiom, we had Martin-Loef's identity type. * It was *intended* to capture equality *as used by mathematicians* (constructive or not). * But it didn't. Hofmann and Streicher proved that. * The identity type captures something else. It certainly doesn't capture truth-valued equality by default. In particular, Voevosdky showed that it captures isomorphism of sets, and more generality equivalence of ∞-groupoids. But this is distorting history a bit. In the initial drafts of his "homotopy lambda calculus", he tried come up with a new construction in type theory to capture equivalence. It was only later that he found out that what he needed was precisely Martin-Loef's identity type. * So writing "x = y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. * Similarly, writing "X ≃ Y" is a bit perverse, too. In truth-valued mathematics, "X ≃ Y" is most of the time intended to be truth-valued, not set-valued. (Exception: category theory. E.g. we write a long chain of isomorphisms to establish that two objects are isomorphic. Then we learn that the author of such a proof was not interested in the existence of an isomorphism, but instead to provide an example. Such a proof/construction is usually concluded by saying something like "by chasing the isomorphism, we see that we can take [...] as our desired isomorphism.) * With the above out of the way, we can consider the imprecise slogan "isomorphic types are equal". The one thing that the univalence axiom doesn't say is that isomorphic type are equal. What it does say is that the *identity type* Id X Y is in canonical bijection with the type X ≃ Y of equivalences. * What is the effect of this? - That the identity type behaves like isomorphism, rather than like equality. - And that isomorphism behaves a little bit like equality. The important thing above is "a little bit". In particular, we cannot *substitute* things by isomorphic things. We can only *transport* them (just like things work as usual with isomorphisms). * Usually, the univalence axioms is expressed as a relation between equality and isomorphism. Where by equality we don't mean equality but instead the identity type. A way to avoid these terminological problems is to formulate univalence as a property of isomorphisms, or more precisely equivalences. To show that all equivalences satisfy a given property, it is enough to prove that all the identity equivalence between any two types have this property. * So, as Mike says above, most of the time we can work with type equivalence rather than "type equality". And I do too. Something that is not well explained at all in the literature is when and how the univalence axiom *actually makes a difference*. (I guess this is not well understood. I used to thing that the univalence axioms makes a difference only for types that are not sets. But actually, for example, the univalence axiom is needed (in the absence of the K axiom) to prove that the type of ordinals is a set.) * One example: object classifiers, subtype classifiers, ... * Sometimes the univalence axiom may be *convenient* but *not needed*. I guess that Kevin is, in particular, saying precisely that. In all cases where he needs to transport constructions along isomorphisms, he is confident that this can be done without univalence. And I would agree with this assessment. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com?utm_medium=email&utm_source=footer>. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- 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/F89C9786-6661-4F12-951D-3D58B1D71C6E%40nottingham.ac.uk. [-- Attachment #2: Type: text/html, Size: 20765 bytes --] <html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"> <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> <meta name="Generator" content="Microsoft Word 15 (filtered medium)"> <style><!-- /* Font Definitions */ @font-face {font-family:"Cambria Math"; panose-1:2 4 5 3 5 4 6 3 2 4;} @font-face {font-family:Calibri; panose-1:2 15 5 2 2 2 4 3 2 4;} @font-face {font-family:-webkit-standard; panose-1:2 11 6 4 2 2 2 2 2 4;} /* Style Definitions */ p.MsoNormal, li.MsoNormal, div.MsoNormal {margin:0cm; margin-bottom:.0001pt; font-size:11.0pt; font-family:"Calibri",sans-serif;} a:link, span.MsoHyperlink {mso-style-priority:99; color:blue; text-decoration:underline;} a:visited, span.MsoHyperlinkFollowed {mso-style-priority:99; color:purple; text-decoration:underline;} p.msonormal0, li.msonormal0, div.msonormal0 {mso-style-name:msonormal; mso-margin-top-alt:auto; margin-right:0cm; mso-margin-bottom-alt:auto; margin-left:0cm; font-size:11.0pt; font-family:"Calibri",sans-serif;} span.EmailStyle19 {mso-style-type:personal-reply; font-family:"Calibri",sans-serif; color:windowtext;} .MsoChpDefault {mso-style-type:export-only; font-size:10.0pt;} @page WordSection1 {size:612.0pt 792.0pt; margin:72.0pt 72.0pt 72.0pt 72.0pt;} div.WordSection1 {page:WordSection1;} --></style><!--[if gte mso 9]><xml> <o:shapedefaults v:ext="edit" spidmax="1026" /> </xml><![endif]--><!--[if gte mso 9]><xml> <o:shapelayout v:ext="edit"> <o:idmap v:ext="edit" data="1" /> </o:shapelayout></xml><![endif]--> </head> <body lang="EN-GB" link="blue" vlink="purple"> <div class="WordSection1"> <p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"-webkit-standard",serif;color:black">So writing "x = y" for the identity type is a bit perverse.<o:p></o:p></span></p> <p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"-webkit-standard",serif;color:black"> People may say, and they have said "but there is no other sensible<o:p></o:p></span></p> <p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"-webkit-standard",serif;color:black"> notion of equality for such type theories.<o:p></o:p></span></p> <p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"-webkit-standard",serif;color:black"> That may be so, but because, in any case, *it is not the same<o:p></o:p></span></p> <p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"-webkit-standard",serif;color:black"> notion of equality*, we should not use the same symbol.<o:p></o:p></span></p> <p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black">Two mathematical objects are equal if they have the same properties. This is exactly what equals means in HoTT and hence we should use the same symbol and call it equality. Everything else is confusing especially for the newcomer: “we have something in HoTT which is basically equality but we call it by a different name and we use a different symbol”???<o:p></o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black">Yes, it is different because equality of structures is not a proposition but a structure. But to insist that equality of structure is a proposition is just a confusion of conventional Mathematics.<o:p></o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black">Independent of conventional Mathematics there is something like a naïve idea of equality which is preformal. And equality in HoTT is just a way to make this preformal notion precise. And why is it so strange to say there is more than one way to objects can be equal?<o:p></o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black">As far is the notion of “canonical isomorphism”, Kevin is interested in, is concerned, I think this is an intensional aspect of an equality and hence not expressible within HoTT. E.g. 3+4 and 7 are the same natural number but 7 is canonical.<o:p></o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black">Thorsten<o:p></o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black"><o:p> </o:p></span></p> <p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p> <p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p> <p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p> <div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm"> <p class="MsoNormal"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black"><homotopytypetheory@googlegroups.com> on behalf of Martín Hötzel Escardó <escardo.martin@gmail.com><br> <b>Date: </b>Tuesday, 26 November 2019 at 19:15<br> <b>To: </b>Homotopy Type Theory <homotopytypetheory@googlegroups.com><br> <b>Subject: </b>Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?<o:p></o:p></span></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"><br> <br> On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: <o:p></o:p></p> <blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm"> <p class="MsoNormal">HoTT instead expands the notion of "equality" to <br> essentially mean "isomorphism" and requires transporting along it as a <br> nontrivial action. I doubt that that's what you have in mind, but <br> maybe you could explain what you do mean? <o:p></o:p></p> </blockquote> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> I think terminology and notation alone cause a lot of confusion (and I<o:p></o:p></p> </div> <div> <p class="MsoNormal">have said this many times in this list in the past, before Kevin joined in).<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal">Much of the disagreement is not a real disagreement but a<o:p></o:p></p> </div> <div> <p class="MsoNormal">misunderstanding.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * In HoTT, or in univalent mathematics, we use the terminology<o:p></o:p></p> </div> <div> <p class="MsoNormal"> "equals" and the notation "=" for something that is not the same<o:p></o:p></p> </div> <div> <p class="MsoNormal"> notion as in "traditional mathematics".<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * Before the univalence axiom, we had Martin-Loef's identity type.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * It was *intended* to capture equality *as used by mathematicians*<o:p></o:p></p> </div> <div> <p class="MsoNormal"> (constructive or not).<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * But it didn't. Hofmann and Streicher proved that.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * The identity type captures something else.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> It certainly doesn't capture truth-valued equality by default.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> In particular, Voevosdky showed that it captures isomorphism of<o:p></o:p></p> </div> <div> <p class="MsoNormal"> sets, and more generality equivalence of ∞-groupoids.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> But this is distorting history a bit.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> In the initial drafts of his "homotopy lambda calculus", he tried<o:p></o:p></p> </div> <div> <p class="MsoNormal"> come up with a new construction in type theory to capture<o:p></o:p></p> </div> <div> <p class="MsoNormal"> equivalence.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> It was only later that he found out that what he needed was<o:p></o:p></p> </div> <div> <p class="MsoNormal"> precisely Martin-Loef's identity type.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * So writing "x = y" for the identity type is a bit perverse.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> People may say, and they have said "but there is no other sensible<o:p></o:p></p> </div> <div> <p class="MsoNormal"> notion of equality for such type theories.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> That may be so, but because, in any case, *it is not the same<o:p></o:p></p> </div> <div> <p class="MsoNormal"> notion of equality*, we should not use the same symbol.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * Similarly, writing "X <span style="font-family:"Cambria Math",serif"> ≃</span> Y" is a bit perverse, too.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> In truth-valued mathematics, "X <span style="font-family:"Cambria Math",serif"> ≃</span> Y" is most of the time intended<o:p></o:p></p> </div> <div> <p class="MsoNormal"> to be truth-valued, not set-valued.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> (Exception: category theory. E.g. we write a long chain of<o:p></o:p></p> </div> <div> <p class="MsoNormal"> isomorphisms to establish that two objects are isomorphic. Then we<o:p></o:p></p> </div> <div> <p class="MsoNormal"> learn that the author of such a proof was not interested in the<o:p></o:p></p> </div> <div> <p class="MsoNormal"> existence of an isomorphism, but instead to provide an<o:p></o:p></p> </div> <div> <p class="MsoNormal"> example. Such a proof/construction is usually concluded by saying<o:p></o:p></p> </div> <div> <p class="MsoNormal"> something like "by chasing the isomorphism, we see that we can take<o:p></o:p></p> </div> <div> <p class="MsoNormal"> [...] as our desired isomorphism.)<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * With the above out of the way, we can consider the imprecise slogan<o:p></o:p></p> </div> <div> <p class="MsoNormal"> "isomorphic types are equal".<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> The one thing that the univalence axiom doesn't say is that<o:p></o:p></p> </div> <div> <p class="MsoNormal"> isomorphic type are equal.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> What it does say is that the *identity type* Id X Y is in canonical<o:p></o:p></p> </div> <div> <p class="MsoNormal"> bijection with the type X <span style="font-family:"Cambria Math",serif"> ≃</span> Y of equivalences.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * What is the effect of this?<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> - That the identity type behaves like isomorphism, rather than like<o:p></o:p></p> </div> <div> <p class="MsoNormal"> equality.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> - And that isomorphism behaves a little bit like equality.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> The important thing above is "a little bit".<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> In particular, we cannot *substitute* things by isomorphic<o:p></o:p></p> </div> <div> <p class="MsoNormal"> things. We can only *transport* them (just like things work as<o:p></o:p></p> </div> <div> <p class="MsoNormal"> usual with isomorphisms).<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * Usually, the univalence axioms is expressed as a relation between<o:p></o:p></p> </div> <div> <p class="MsoNormal"> equality and isomorphism.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> Where by equality we don't mean equality but instead the identity<o:p></o:p></p> </div> <div> <p class="MsoNormal"> type.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> A way to avoid these terminological problems is to formulate<o:p></o:p></p> </div> <div> <p class="MsoNormal"> univalence as a property of isomorphisms, or more precisely<o:p></o:p></p> </div> <div> <p class="MsoNormal"> equivalences.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> To show that all equivalences satisfy a given property, it is<o:p></o:p></p> </div> <div> <p class="MsoNormal"> enough to prove that all the identity equivalence between any two<o:p></o:p></p> </div> <div> <p class="MsoNormal"> types have this property.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * So, as Mike says above, most of the time we can work with type<o:p></o:p></p> </div> <div> <p class="MsoNormal"> equivalence rather than "type equality". And I do too.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> Something that is not well explained at all in the literature is<o:p></o:p></p> </div> <div> <p class="MsoNormal"> when and how the univalence axiom *actually makes a difference*.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> (I guess this is not well understood. I used to thing that the<o:p></o:p></p> </div> <div> <p class="MsoNormal"> univalence axioms makes a difference only for types that are not<o:p></o:p></p> </div> <div> <p class="MsoNormal"> sets. But actually, for example, the univalence axiom is needed (in<o:p></o:p></p> </div> <div> <p class="MsoNormal"> the absence of the K axiom) to prove that the type of ordinals is a<o:p></o:p></p> </div> <div> <p class="MsoNormal"> set.)<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * One example: object classifiers, subtype classifiers, ...<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> * Sometimes the univalence axiom may be *convenient* but *not needed*.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> I guess that Kevin is, in particular, saying precisely that. In all<o:p></o:p></p> </div> <div> <p class="MsoNormal"> cases where he needs to transport constructions along isomorphisms,<o:p></o:p></p> </div> <div> <p class="MsoNormal"> he is confident that this can be done without univalence. And I<o:p></o:p></p> </div> <div> <p class="MsoNormal"> would agree with this assessment.<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal">Best,<o:p></o:p></p> </div> <div> <p class="MsoNormal">Martin<o:p></o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"><o:p> </o:p></p> </div> <div> <p class="MsoNormal"> <o:p></o:p></p> </div> </div> <p class="MsoNormal">-- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com?utm_medium=email&utm_source=footer"> https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com</a>.<br> <br> <o:p></o:p></p> </div> <PRE> This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. </PRE></body> </html> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/F89C9786-6661-4F12-951D-3D58B1D71C6E%40nottingham.ac.uk?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/F89C9786-6661-4F12-951D-3D58B1D71C6E%40nottingham.ac.uk</a>.<br />

At 2019-11-26T14:18:34-08:00, Michael Shulman wrote: > Personally, I'm doubtful that one can ascribe any precise meaning to > "canonical isomorphism", and therefore doubtful that one will be able > to implement a computer proof assistant that can distinguish a > "canonical isomorphism" from an arbitrary one. I have usually assumed that canonical isomorphism meant functorial isomorphism, i.e., an isomorphism between an appropriate pair of functors (which are generally left unspecified). As has been mentioned, there is no functorial isomorphism from an arbitrary finite-dimensional vector space V to its dual, whereas the usual isomorphism from V to double dual is functorial, so the former is non-canonical, and the latter canonical. Another explanation I've often come across is that a canonical object is independent of the choices (if any) that were made in its definition. I guess the notion of independence depends on the context. Raghu. -- N. Raghavendra <raghu@hri.res.in>, http://www.retrotexts.net/ Harish-Chandra Research Institute, http://www.hri.res.in/ -- 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/87k17lafu9.fsf%40hri.res.in.

> Maybe AI (deep learning) could be trained to recognise the correct > canonical isomorphism from the context (=the proof). Can't we define it more formally as the isomorphism with the smallest proof? Stefan -- 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/jwvmuciqcnn.fsf-monnier%2Bdiro%40gnu.org.

[-- Attachment #1.1: Type: text/plain, Size: 838 bytes --] On Tuesday, November 26, 2019 at 4:18:49 PM UTC-6, Michael Shulman wrote: > > Personally, I'm doubtful that one can ascribe any precise meaning to > "canonical isomorphism", > One standard example of a non-canonical isomorphism is that between a finite dimensional vector space V and its dual V', so perhaps one may define a non-canonical isomorphism to be one that one merely has, and a canonical isomorphism is one that one actually has. -- 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/39769e9d-6de3-422b-b3f7-123dcc2f737f%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1336 bytes --] <div dir="ltr">On Tuesday, November 26, 2019 at 4:18:49 PM UTC-6, Michael Shulman wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">Personally, I'm doubtful that one can ascribe any precise meaning to <br>"canonical isomorphism",<br></blockquote><div><br></div><div><div>One standard example of a non-canonical isomorphism is that between a finite dimensional </div><div>vector space V and its dual V', so perhaps one may define a non-canonical isomorphism</div><div>to be one that one merely has, and a canonical isomorphism is one that one actually has.</div></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/39769e9d-6de3-422b-b3f7-123dcc2f737f%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/39769e9d-6de3-422b-b3f7-123dcc2f737f%40googlegroups.com</a>.<br />

Dear Michael, You wrote: <<Personally, I'm doubtful that one can ascribe any precise meaning to "canonical isomorphism", and therefore doubtful that one will be able to implement a computer proof assistant that can distinguish a "canonical isomorphism" from an arbitrary one. >> The notion of canonical isomorphism depends obviously on the context. For example, the "canonical isomorphism" (AxB)xC = Ax(BxC) is likely to be the associativity isomorphism. Maybe AI (deep learning) could be trained to recognise the correct canonical isomorphism from the context (=the proof). It may automatise what is already automatic in our thinking. Best, André ________________________________________ From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of Michael Shulman [shulman@sandiego.edu] Sent: Tuesday, November 26, 2019 5:18 PM To: Kevin Buzzard Cc: Martín Hötzel Escardó; Homotopy Type Theory Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Personally, I'm doubtful that one can ascribe any precise meaning to "canonical isomorphism", and therefore doubtful that one will be able to implement a computer proof assistant that can distinguish a "canonical isomorphism" from an arbitrary one. It's certainly worth thinking about, but my personal opinion is that instead of designing a proof assistant to match the way mathematicians think about "canonical isomorphisms", mathematicians are going to need to change the way they think. But it's just a question of going all the way down a road that they've already taken one step along. In formal systems like ZFC and Lean, almost no isomorphisms are equalities. Being willing to treat "canonical" isomorphisms as equalities is a first step into the brave new world of homotopy theory and higher category theory, but it's hard to find a place to stand when you've only taken that one step. In trying to make things precise, I think one feels inexorably pulled to the more consistent, and formalizable, position that *all* isomorphisms should be treated as equalities. It's not the same notion of equality, as Martin says, but it's a better replacement for it, which in particular can do everything that the old notion of equality could do when used "correctly" (e.g. equality of numbers and functions). On Tue, Nov 26, 2019 at 11:53 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > Nicolas originally asked > > "So, to put this into one concrete question, how (if at all) is HoTT-Coq > more practical than Mizar for the purpose of formalizing mathematics, > outside the specific realm of synthetic homotopy theory?" > > One issue with this question is that different people mean different things by "mathematics". As someone who was until recently an outsider to formalising but very much a "working mathematician", I think I've made it pretty clear on this forum and others that for the majority of people in e.g. my maths department, they would say that none of the systems have really got anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help change, but it needs a cultural change within mathematics departments. The Mizar stuff I've seen has mostly been undergraduate level mathematics. UniMath seems to be a massive amount of category theory and not much undergraduate level mathematics at all. On the other hand, "there is a lot more category theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more practical than Mizar for category theory" might be an answer to the original question. > > I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that the notation for "canonical isomorphism" (whatever that means) is "=". One can call this "mathematical equality" and it comes with a warning that it is not well-defined. I think one reason it's a challenge to formalise modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal). > > It would not surprise me if different areas of mathematics had different concepts of equality. Mathematicians seem to use the concept very fluidly. Maybe it is the case that the areas where "mathematical equality" is closer to e.g. Lean's `=` or Mizar's `=` or UniMath's `=` or Isabelle/HOL's `=` or whatever, will find that formalising goes more easily in Lean's type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, and there is not enough harder maths formalised in any of these systems (obviously there are several monumental theorems but I'm dreaming about far greater things) for us to start to check. Note that people like Riemann had no idea about set theory but did a lot of complex analysis, and he really only needed to worry about equality of complex numbers and equality of functions from the complexes to the complexes, so I don't think it's a coincidence that a whole bunch of complex analysis is done in Isabelle/HOL, which seems to me to be the "simplest logic" of the lot. Probably all the systems model this equality well. > > Kevin > > > On Tue, 26 Nov 2019 at 19:14, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: >> >> >> >> On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: >>> >>> HoTT instead expands the notion of "equality" to >>> essentially mean "isomorphism" and requires transporting along it as a >>> nontrivial action. I doubt that that's what you have in mind, but >>> maybe you could explain what you do mean? >> >> >> I think terminology and notation alone cause a lot of confusion (and I >> have said this many times in this list in the past, before Kevin joined in). >> >> Much of the disagreement is not a real disagreement but a >> misunderstanding. >> >> * In HoTT, or in univalent mathematics, we use the terminology >> "equals" and the notation "=" for something that is not the same >> notion as in "traditional mathematics". >> >> * Before the univalence axiom, we had Martin-Loef's identity type. >> >> * It was *intended* to capture equality *as used by mathematicians* >> (constructive or not). >> >> * But it didn't. Hofmann and Streicher proved that. >> >> * The identity type captures something else. >> >> It certainly doesn't capture truth-valued equality by default. >> >> In particular, Voevosdky showed that it captures isomorphism of >> sets, and more generality equivalence of ∞-groupoids. >> >> But this is distorting history a bit. >> >> In the initial drafts of his "homotopy lambda calculus", he tried >> come up with a new construction in type theory to capture >> equivalence. >> >> It was only later that he found out that what he needed was >> precisely Martin-Loef's identity type. >> >> * So writing "x = y" for the identity type is a bit perverse. >> >> People may say, and they have said "but there is no other sensible >> notion of equality for such type theories. >> >> That may be so, but because, in any case, *it is not the same >> notion of equality*, we should not use the same symbol. >> >> * Similarly, writing "X ≃ Y" is a bit perverse, too. >> >> In truth-valued mathematics, "X ≃ Y" is most of the time intended >> to be truth-valued, not set-valued. >> >> (Exception: category theory. E.g. we write a long chain of >> isomorphisms to establish that two objects are isomorphic. Then we >> learn that the author of such a proof was not interested in the >> existence of an isomorphism, but instead to provide an >> example. Such a proof/construction is usually concluded by saying >> something like "by chasing the isomorphism, we see that we can take >> [...] as our desired isomorphism.) >> >> >> * With the above out of the way, we can consider the imprecise slogan >> "isomorphic types are equal". >> >> The one thing that the univalence axiom doesn't say is that >> isomorphic type are equal. >> >> What it does say is that the *identity type* Id X Y is in canonical >> bijection with the type X ≃ Y of equivalences. >> >> * What is the effect of this? >> >> - That the identity type behaves like isomorphism, rather than like >> equality. >> >> - And that isomorphism behaves a little bit like equality. >> >> The important thing above is "a little bit". >> >> In particular, we cannot *substitute* things by isomorphic >> things. We can only *transport* them (just like things work as >> usual with isomorphisms). >> >> * Usually, the univalence axioms is expressed as a relation between >> equality and isomorphism. >> >> Where by equality we don't mean equality but instead the identity >> type. >> >> A way to avoid these terminological problems is to formulate >> univalence as a property of isomorphisms, or more precisely >> equivalences. >> >> To show that all equivalences satisfy a given property, it is >> enough to prove that all the identity equivalence between any two >> types have this property. >> >> * So, as Mike says above, most of the time we can work with type >> equivalence rather than "type equality". And I do too. >> >> Something that is not well explained at all in the literature is >> when and how the univalence axiom *actually makes a difference*. >> >> (I guess this is not well understood. I used to thing that the >> univalence axioms makes a difference only for types that are not >> sets. But actually, for example, the univalence axiom is needed (in >> the absence of the K axiom) to prove that the type of ordinals is a >> set.) >> >> * One example: object classifiers, subtype classifiers, ... >> >> * Sometimes the univalence axiom may be *convenient* but *not needed*. >> >> I guess that Kevin is, in particular, saying precisely that. In all >> cases where he needs to transport constructions along isomorphisms, >> he is confident that this can be done without univalence. And I >> would agree with this assessment. >> >> Best, >> Martin >> >> >> >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.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/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%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/CAOvivQyAaJnLeJZHCMqWAu3f%2BOb72%2BMSSLmb8MjkBHoH05k_Rw%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/8C57894C7413F04A98DDF5629FEC90B1652BA70E%40Pli.gst.uqam.ca.

Personally, I'm doubtful that one can ascribe any precise meaning to "canonical isomorphism", and therefore doubtful that one will be able to implement a computer proof assistant that can distinguish a "canonical isomorphism" from an arbitrary one. It's certainly worth thinking about, but my personal opinion is that instead of designing a proof assistant to match the way mathematicians think about "canonical isomorphisms", mathematicians are going to need to change the way they think. But it's just a question of going all the way down a road that they've already taken one step along. In formal systems like ZFC and Lean, almost no isomorphisms are equalities. Being willing to treat "canonical" isomorphisms as equalities is a first step into the brave new world of homotopy theory and higher category theory, but it's hard to find a place to stand when you've only taken that one step. In trying to make things precise, I think one feels inexorably pulled to the more consistent, and formalizable, position that *all* isomorphisms should be treated as equalities. It's not the same notion of equality, as Martin says, but it's a better replacement for it, which in particular can do everything that the old notion of equality could do when used "correctly" (e.g. equality of numbers and functions). On Tue, Nov 26, 2019 at 11:53 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > > Nicolas originally asked > > "So, to put this into one concrete question, how (if at all) is HoTT-Coq > more practical than Mizar for the purpose of formalizing mathematics, > outside the specific realm of synthetic homotopy theory?" > > One issue with this question is that different people mean different things by "mathematics". As someone who was until recently an outsider to formalising but very much a "working mathematician", I think I've made it pretty clear on this forum and others that for the majority of people in e.g. my maths department, they would say that none of the systems have really got anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help change, but it needs a cultural change within mathematics departments. The Mizar stuff I've seen has mostly been undergraduate level mathematics. UniMath seems to be a massive amount of category theory and not much undergraduate level mathematics at all. On the other hand, "there is a lot more category theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more practical than Mizar for category theory" might be an answer to the original question. > > I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that the notation for "canonical isomorphism" (whatever that means) is "=". One can call this "mathematical equality" and it comes with a warning that it is not well-defined. I think one reason it's a challenge to formalise modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal). > > It would not surprise me if different areas of mathematics had different concepts of equality. Mathematicians seem to use the concept very fluidly. Maybe it is the case that the areas where "mathematical equality" is closer to e.g. Lean's `=` or Mizar's `=` or UniMath's `=` or Isabelle/HOL's `=` or whatever, will find that formalising goes more easily in Lean's type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, and there is not enough harder maths formalised in any of these systems (obviously there are several monumental theorems but I'm dreaming about far greater things) for us to start to check. Note that people like Riemann had no idea about set theory but did a lot of complex analysis, and he really only needed to worry about equality of complex numbers and equality of functions from the complexes to the complexes, so I don't think it's a coincidence that a whole bunch of complex analysis is done in Isabelle/HOL, which seems to me to be the "simplest logic" of the lot. Probably all the systems model this equality well. > > Kevin > > > On Tue, 26 Nov 2019 at 19:14, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: >> >> >> >> On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: >>> >>> HoTT instead expands the notion of "equality" to >>> essentially mean "isomorphism" and requires transporting along it as a >>> nontrivial action. I doubt that that's what you have in mind, but >>> maybe you could explain what you do mean? >> >> >> I think terminology and notation alone cause a lot of confusion (and I >> have said this many times in this list in the past, before Kevin joined in). >> >> Much of the disagreement is not a real disagreement but a >> misunderstanding. >> >> * In HoTT, or in univalent mathematics, we use the terminology >> "equals" and the notation "=" for something that is not the same >> notion as in "traditional mathematics". >> >> * Before the univalence axiom, we had Martin-Loef's identity type. >> >> * It was *intended* to capture equality *as used by mathematicians* >> (constructive or not). >> >> * But it didn't. Hofmann and Streicher proved that. >> >> * The identity type captures something else. >> >> It certainly doesn't capture truth-valued equality by default. >> >> In particular, Voevosdky showed that it captures isomorphism of >> sets, and more generality equivalence of ∞-groupoids. >> >> But this is distorting history a bit. >> >> In the initial drafts of his "homotopy lambda calculus", he tried >> come up with a new construction in type theory to capture >> equivalence. >> >> It was only later that he found out that what he needed was >> precisely Martin-Loef's identity type. >> >> * So writing "x = y" for the identity type is a bit perverse. >> >> People may say, and they have said "but there is no other sensible >> notion of equality for such type theories. >> >> That may be so, but because, in any case, *it is not the same >> notion of equality*, we should not use the same symbol. >> >> * Similarly, writing "X ≃ Y" is a bit perverse, too. >> >> In truth-valued mathematics, "X ≃ Y" is most of the time intended >> to be truth-valued, not set-valued. >> >> (Exception: category theory. E.g. we write a long chain of >> isomorphisms to establish that two objects are isomorphic. Then we >> learn that the author of such a proof was not interested in the >> existence of an isomorphism, but instead to provide an >> example. Such a proof/construction is usually concluded by saying >> something like "by chasing the isomorphism, we see that we can take >> [...] as our desired isomorphism.) >> >> >> * With the above out of the way, we can consider the imprecise slogan >> "isomorphic types are equal". >> >> The one thing that the univalence axiom doesn't say is that >> isomorphic type are equal. >> >> What it does say is that the *identity type* Id X Y is in canonical >> bijection with the type X ≃ Y of equivalences. >> >> * What is the effect of this? >> >> - That the identity type behaves like isomorphism, rather than like >> equality. >> >> - And that isomorphism behaves a little bit like equality. >> >> The important thing above is "a little bit". >> >> In particular, we cannot *substitute* things by isomorphic >> things. We can only *transport* them (just like things work as >> usual with isomorphisms). >> >> * Usually, the univalence axioms is expressed as a relation between >> equality and isomorphism. >> >> Where by equality we don't mean equality but instead the identity >> type. >> >> A way to avoid these terminological problems is to formulate >> univalence as a property of isomorphisms, or more precisely >> equivalences. >> >> To show that all equivalences satisfy a given property, it is >> enough to prove that all the identity equivalence between any two >> types have this property. >> >> * So, as Mike says above, most of the time we can work with type >> equivalence rather than "type equality". And I do too. >> >> Something that is not well explained at all in the literature is >> when and how the univalence axiom *actually makes a difference*. >> >> (I guess this is not well understood. I used to thing that the >> univalence axioms makes a difference only for types that are not >> sets. But actually, for example, the univalence axiom is needed (in >> the absence of the K axiom) to prove that the type of ordinals is a >> set.) >> >> * One example: object classifiers, subtype classifiers, ... >> >> * Sometimes the univalence axiom may be *convenient* but *not needed*. >> >> I guess that Kevin is, in particular, saying precisely that. In all >> cases where he needs to transport constructions along isomorphisms, >> he is confident that this can be done without univalence. And I >> would agree with this assessment. >> >> Best, >> Martin >> >> >> >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.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/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%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/CAOvivQyAaJnLeJZHCMqWAu3f%2BOb72%2BMSSLmb8MjkBHoH05k_Rw%40mail.gmail.com.

[-- Attachment #1.1: Type: text/plain, Size: 1594 bytes --] On Tuesday, 26 November 2019 19:53:19 UTC, Kevin Buzzard wrote: > > What I meant by my earlier post was that the `=` I have run into in Lean's > type theory is too weak (canonically isomorphic things can't be proved to > be equal) but the one I have run into in HoTT seems too strong > (non-canonically isomorphic things are equal). > Given a *specific* isomorphism, in HoTT you get a *specific* element of the identity type. Let me say this explicitly: equality in HoTT is not truth-valued. It collects all the possible ways to identify things. In the case of equality of types, the identity type collects the equivalences between them (rather than being the truth value expressing whether they are equivalent). In fact, canonicity is at the heart of the univalence axiom: there is a canonical one-to-one correspondence between elements of the equality type (i.e. the identity type) and elements of the types of equivalences. So, the univalence axiom just says that the elements of the good, old identity type can be understood to be precisely the equivalences. You may wonder what the bonus of this is. This is the content of my last two bullet points in my message. 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/77829d67-ed64-43eb-aaf0-d673df419080%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2231 bytes --] <div dir="ltr"><br><br>On Tuesday, 26 November 2019 19:53:19 UTC, Kevin Buzzard wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir="ltr"><div>What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal).</div></div></blockquote><div><br></div><div>Given a *specific* isomorphism, in HoTT you get a *specific* element of the identity type. </div><div><br></div><div>Let me say this explicitly: equality in HoTT is not truth-valued. It collects all the possible ways to identify things. In the case of equality of types, the identity type collects the equivalences between them (rather than being the truth value expressing whether they are equivalent).</div><div><br></div><div>In fact, canonicity is at the heart of the univalence axiom: there is a canonical one-to-one correspondence between elements of the equality type (i.e. the identity type) and elements of the types of equivalences.</div><div><br></div><div>So, the univalence axiom just says that the elements of the good, old identity type can be understood to be precisely the equivalences. </div><div><br></div><div>You may wonder what the bonus of this is. This is the content of my last two bullet points in my message.</div><div><br></div><div>Martin</div><div><br></div><div><br></div><div> </div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/77829d67-ed64-43eb-aaf0-d673df419080%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/77829d67-ed64-43eb-aaf0-d673df419080%40googlegroups.com</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 9223 bytes --] Nicolas originally asked "So, to put this into one concrete question, how (if at all) is HoTT-Coq more practical than Mizar for the purpose of formalizing mathematics, outside the specific realm of synthetic homotopy theory?" One issue with this question is that different people mean different things by "mathematics". As someone who was until recently an outsider to formalising but very much a "working mathematician", I think I've made it pretty clear on this forum and others that for the majority of people in e.g. my maths department, they would say that none of the systems have really got anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help change, but it needs a cultural change within mathematics departments. The Mizar stuff I've seen has mostly been undergraduate level mathematics. UniMath seems to be a massive amount of category theory and not much undergraduate level mathematics at all. On the other hand, "there is a lot more category theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more practical than Mizar for category theory" might be an answer to the original question. I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that the notation for "canonical isomorphism" (whatever that means) is "=". One can call this "mathematical equality" and it comes with a warning that it is not well-defined. I think one reason it's a challenge to formalise modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal). It would not surprise me if different areas of mathematics had different concepts of equality. Mathematicians seem to use the concept very fluidly. Maybe it is the case that the areas where "mathematical equality" is closer to e.g. Lean's `=` or Mizar's `=` or UniMath's `=` or Isabelle/HOL's `=` or whatever, will find that formalising goes more easily in Lean's type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, and there is not enough harder maths formalised in any of these systems (obviously there are several monumental theorems but I'm dreaming about far greater things) for us to start to check. Note that people like Riemann had no idea about set theory but did a lot of complex analysis, and he really only needed to worry about equality of complex numbers and equality of functions from the complexes to the complexes, so I don't think it's a coincidence that a whole bunch of complex analysis is done in Isabelle/HOL, which seems to me to be the "simplest logic" of the lot. Probably all the systems model this equality well. Kevin On Tue, 26 Nov 2019 at 19:14, Martín Hötzel Escardó < escardo.martin@gmail.com> wrote: > > > On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: >> >> HoTT instead expands the notion of "equality" to >> essentially mean "isomorphism" and requires transporting along it as a >> nontrivial action. I doubt that that's what you have in mind, but >> maybe you could explain what you do mean? >> > > I think terminology and notation alone cause a lot of confusion (and I > have said this many times in this list in the past, before Kevin joined > in). > > Much of the disagreement is not a real disagreement but a > misunderstanding. > > * In HoTT, or in univalent mathematics, we use the terminology > "equals" and the notation "=" for something that is not the same > notion as in "traditional mathematics". > > * Before the univalence axiom, we had Martin-Loef's identity type. > > * It was *intended* to capture equality *as used by mathematicians* > (constructive or not). > > * But it didn't. Hofmann and Streicher proved that. > > * The identity type captures something else. > > It certainly doesn't capture truth-valued equality by default. > > In particular, Voevosdky showed that it captures isomorphism of > sets, and more generality equivalence of ∞-groupoids. > > But this is distorting history a bit. > > In the initial drafts of his "homotopy lambda calculus", he tried > come up with a new construction in type theory to capture > equivalence. > > It was only later that he found out that what he needed was > precisely Martin-Loef's identity type. > > * So writing "x = y" for the identity type is a bit perverse. > > People may say, and they have said "but there is no other sensible > notion of equality for such type theories. > > That may be so, but because, in any case, *it is not the same > notion of equality*, we should not use the same symbol. > > * Similarly, writing "X ≃ Y" is a bit perverse, too. > > In truth-valued mathematics, "X ≃ Y" is most of the time intended > to be truth-valued, not set-valued. > > (Exception: category theory. E.g. we write a long chain of > isomorphisms to establish that two objects are isomorphic. Then we > learn that the author of such a proof was not interested in the > existence of an isomorphism, but instead to provide an > example. Such a proof/construction is usually concluded by saying > something like "by chasing the isomorphism, we see that we can take > [...] as our desired isomorphism.) > > > * With the above out of the way, we can consider the imprecise slogan > "isomorphic types are equal". > > The one thing that the univalence axiom doesn't say is that > isomorphic type are equal. > > What it does say is that the *identity type* Id X Y is in canonical > bijection with the type X ≃ Y of equivalences. > > * What is the effect of this? > > - That the identity type behaves like isomorphism, rather than like > equality. > > - And that isomorphism behaves a little bit like equality. > > The important thing above is "a little bit". > > In particular, we cannot *substitute* things by isomorphic > things. We can only *transport* them (just like things work as > usual with isomorphisms). > > * Usually, the univalence axioms is expressed as a relation between > equality and isomorphism. > > Where by equality we don't mean equality but instead the identity > type. > > A way to avoid these terminological problems is to formulate > univalence as a property of isomorphisms, or more precisely > equivalences. > > To show that all equivalences satisfy a given property, it is > enough to prove that all the identity equivalence between any two > types have this property. > > * So, as Mike says above, most of the time we can work with type > equivalence rather than "type equality". And I do too. > > Something that is not well explained at all in the literature is > when and how the univalence axiom *actually makes a difference*. > > (I guess this is not well understood. I used to thing that the > univalence axioms makes a difference only for types that are not > sets. But actually, for example, the univalence axiom is needed (in > the absence of the K axiom) to prove that the type of ordinals is a > set.) > > * One example: object classifiers, subtype classifiers, ... > > * Sometimes the univalence axiom may be *convenient* but *not needed*. > > I guess that Kevin is, in particular, saying precisely that. In all > cases where he needs to transport constructions along isomorphisms, > he is confident that this can be done without univalence. And I > would agree with this assessment. > > Best, > Martin > > > > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.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/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 11645 bytes --] <div dir="ltr"><div>Nicolas originally asked</div><div><br></div><div>"So, to put this into one concrete question, how (if at all) is HoTT-Coq<br> more practical than Mizar for the purpose of formalizing mathematics,<br> outside the specific realm of synthetic homotopy theory?"</div><div><br></div><div>One issue with this question is that different people mean different things by "mathematics". As someone who was until recently an outsider to formalising but very much a "working mathematician", I think I've made it pretty clear on this forum and others that for the majority of people in e.g. my maths department, they would say that none of the systems have really got anywhere concerning modern day mathematics, which is the kind of mathematics that the majority of mathematicians working in maths departments are interested in. This is a dismal state of affairs and one which I would love to help change, but it needs a cultural change within mathematics departments. The Mizar stuff I've seen has mostly been undergraduate level mathematics. UniMath seems to be a massive amount of category theory and not much undergraduate level mathematics at all. On the other hand, "there is a lot more category theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more practical than Mizar for category theory" might be an answer to the original question.</div><div><br></div><div>I'm interested in algebraic geometry, and in algebraic geometry there is this convention (explicitly flagged in Milne's book on etale cohomology) that the notation for "canonical isomorphism" (whatever that means) is "=". One can call this "mathematical equality" and it comes with a warning that it is not well-defined. I think one reason it's a challenge to formalise modern algebraic geometry is that none of the systems seem to have this kind of equality (perhaps because all of the systems demand well-defined definitions!). What I meant by my earlier post was that the `=` I have run into in Lean's type theory is too weak (canonically isomorphic things can't be proved to be equal) but the one I have run into in HoTT seems too strong (non-canonically isomorphic things are equal). <br></div><div><br></div><div>It would not surprise me if different areas of mathematics had different concepts of equality. Mathematicians seem to use the concept very fluidly. Maybe it is the case that the areas where "mathematical equality" is closer to e.g. Lean's `=` or Mizar's `=` or UniMath's `=` or Isabelle/HOL's `=` or whatever, will find that formalising goes more easily in Lean's type theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjecture is that equality is mostly a cut-and-dried thing at undergraduate level, and there is not enough harder maths formalised in any of these systems (obviously there are several monumental theorems but I'm dreaming about far greater things) for us to start to check. Note that people like Riemann had no idea about set theory but did a lot of complex analysis, and he really only needed to worry about equality of complex numbers and equality of functions from the complexes to the complexes, so I don't think it's a coincidence that a whole bunch of complex analysis is done in Isabelle/HOL, which seems to me to be the "simplest logic" of the lot. Probably all the systems model this equality well.</div><div><br></div><div>Kevin<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 26 Nov 2019 at 19:14, Martín Hötzel Escardó <<a href="mailto:escardo.martin@gmail.com">escardo.martin@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><br><br>On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote:<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">HoTT instead expands the notion of "equality" to <br>essentially mean "isomorphism" and requires transporting along it as a <br>nontrivial action. I doubt that that's what you have in mind, but <br>maybe you could explain what you do mean? <br></blockquote><div><br></div><div> I think terminology and notation alone cause a lot of confusion (and I</div><div>have said this many times in this list in the past, before Kevin joined in).</div><div><br></div><div>Much of the disagreement is not a real disagreement but a</div><div>misunderstanding.</div><div><br></div><div> * In HoTT, or in univalent mathematics, we use the terminology</div><div> "equals" and the notation "=" for something that is not the same</div><div> notion as in "traditional mathematics".</div><div><br></div><div> * Before the univalence axiom, we had Martin-Loef's identity type.</div><div><br></div><div> * It was *intended* to capture equality *as used by mathematicians*</div><div> (constructive or not).</div><div><br></div><div> * But it didn't. Hofmann and Streicher proved that.</div><div><br></div><div> * The identity type captures something else.</div><div><br></div><div> It certainly doesn't capture truth-valued equality by default.</div><div><br></div><div> In particular, Voevosdky showed that it captures isomorphism of</div><div> sets, and more generality equivalence of ∞-groupoids.</div><div><br></div><div> But this is distorting history a bit.</div><div><br></div><div> In the initial drafts of his "homotopy lambda calculus", he tried</div><div> come up with a new construction in type theory to capture</div><div> equivalence.</div><div><br></div><div> It was only later that he found out that what he needed was</div><div> precisely Martin-Loef's identity type.</div><div><br></div><div> * So writing "x = y" for the identity type is a bit perverse.</div><div><br></div><div> People may say, and they have said "but there is no other sensible</div><div> notion of equality for such type theories.</div><div><br></div><div> That may be so, but because, in any case, *it is not the same</div><div> notion of equality*, we should not use the same symbol.</div><div><br></div><div> * Similarly, writing "X ≃ Y" is a bit perverse, too.</div><div><br></div><div> In truth-valued mathematics, "X ≃ Y" is most of the time intended</div><div> to be truth-valued, not set-valued.</div><div><br></div><div> (Exception: category theory. E.g. we write a long chain of</div><div> isomorphisms to establish that two objects are isomorphic. Then we</div><div> learn that the author of such a proof was not interested in the</div><div> existence of an isomorphism, but instead to provide an</div><div> example. Such a proof/construction is usually concluded by saying</div><div> something like "by chasing the isomorphism, we see that we can take</div><div> [...] as our desired isomorphism.)</div><div><br></div><div><br></div><div> * With the above out of the way, we can consider the imprecise slogan</div><div> "isomorphic types are equal".</div><div><br></div><div> The one thing that the univalence axiom doesn't say is that</div><div> isomorphic type are equal.</div><div><br></div><div> What it does say is that the *identity type* Id X Y is in canonical</div><div> bijection with the type X ≃ Y of equivalences.</div><div><br></div><div> * What is the effect of this?</div><div><br></div><div> - That the identity type behaves like isomorphism, rather than like</div><div> equality.</div><div><br></div><div> - And that isomorphism behaves a little bit like equality.</div><div><br></div><div> The important thing above is "a little bit".</div><div><br></div><div> In particular, we cannot *substitute* things by isomorphic</div><div> things. We can only *transport* them (just like things work as</div><div> usual with isomorphisms).</div><div><br></div><div> * Usually, the univalence axioms is expressed as a relation between</div><div> equality and isomorphism.</div><div><br></div><div> Where by equality we don't mean equality but instead the identity</div><div> type.</div><div><br></div><div> A way to avoid these terminological problems is to formulate</div><div> univalence as a property of isomorphisms, or more precisely</div><div> equivalences.</div><div><br></div><div> To show that all equivalences satisfy a given property, it is</div><div> enough to prove that all the identity equivalence between any two</div><div> types have this property.</div><div><br></div><div> * So, as Mike says above, most of the time we can work with type</div><div> equivalence rather than "type equality". And I do too.</div><div><br></div><div> Something that is not well explained at all in the literature is</div><div> when and how the univalence axiom *actually makes a difference*.</div><div><br></div><div> (I guess this is not well understood. I used to thing that the</div><div> univalence axioms makes a difference only for types that are not</div><div> sets. But actually, for example, the univalence axiom is needed (in</div><div> the absence of the K axiom) to prove that the type of ordinals is a</div><div> set.)</div><div><br></div><div> * One example: object classifiers, subtype classifiers, ...</div><div><br></div><div> * Sometimes the univalence axiom may be *convenient* but *not needed*.</div><div><br></div><div> I guess that Kevin is, in particular, saying precisely that. In all</div><div> cases where he needs to transport constructions along isomorphisms,</div><div> he is confident that this can be done without univalence. And I</div><div> would agree with this assessment.</div><div><br></div><div>Best,</div><div>Martin</div><div><br></div><div><br></div><div> </div></div> <p></p> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com?utm_medium=email&utm_source=footer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com</a>.<br> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40mail.gmail.com</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 5058 bytes --] On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: > > HoTT instead expands the notion of "equality" to > essentially mean "isomorphism" and requires transporting along it as a > nontrivial action. I doubt that that's what you have in mind, but > maybe you could explain what you do mean? > I think terminology and notation alone cause a lot of confusion (and I have said this many times in this list in the past, before Kevin joined in). Much of the disagreement is not a real disagreement but a misunderstanding. * In HoTT, or in univalent mathematics, we use the terminology "equals" and the notation "=" for something that is not the same notion as in "traditional mathematics". * Before the univalence axiom, we had Martin-Loef's identity type. * It was *intended* to capture equality *as used by mathematicians* (constructive or not). * But it didn't. Hofmann and Streicher proved that. * The identity type captures something else. It certainly doesn't capture truth-valued equality by default. In particular, Voevosdky showed that it captures isomorphism of sets, and more generality equivalence of ∞-groupoids. But this is distorting history a bit. In the initial drafts of his "homotopy lambda calculus", he tried come up with a new construction in type theory to capture equivalence. It was only later that he found out that what he needed was precisely Martin-Loef's identity type. * So writing "x = y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. * Similarly, writing "X ≃ Y" is a bit perverse, too. In truth-valued mathematics, "X ≃ Y" is most of the time intended to be truth-valued, not set-valued. (Exception: category theory. E.g. we write a long chain of isomorphisms to establish that two objects are isomorphic. Then we learn that the author of such a proof was not interested in the existence of an isomorphism, but instead to provide an example. Such a proof/construction is usually concluded by saying something like "by chasing the isomorphism, we see that we can take [...] as our desired isomorphism.) * With the above out of the way, we can consider the imprecise slogan "isomorphic types are equal". The one thing that the univalence axiom doesn't say is that isomorphic type are equal. What it does say is that the *identity type* Id X Y is in canonical bijection with the type X ≃ Y of equivalences. * What is the effect of this? - That the identity type behaves like isomorphism, rather than like equality. - And that isomorphism behaves a little bit like equality. The important thing above is "a little bit". In particular, we cannot *substitute* things by isomorphic things. We can only *transport* them (just like things work as usual with isomorphisms). * Usually, the univalence axioms is expressed as a relation between equality and isomorphism. Where by equality we don't mean equality but instead the identity type. A way to avoid these terminological problems is to formulate univalence as a property of isomorphisms, or more precisely equivalences. To show that all equivalences satisfy a given property, it is enough to prove that all the identity equivalence between any two types have this property. * So, as Mike says above, most of the time we can work with type equivalence rather than "type equality". And I do too. Something that is not well explained at all in the literature is when and how the univalence axiom *actually makes a difference*. (I guess this is not well understood. I used to thing that the univalence axioms makes a difference only for types that are not sets. But actually, for example, the univalence axiom is needed (in the absence of the K axiom) to prove that the type of ordinals is a set.) * One example: object classifiers, subtype classifiers, ... * Sometimes the univalence axiom may be *convenient* but *not needed*. I guess that Kevin is, in particular, saying precisely that. In all cases where he needs to transport constructions along isomorphisms, he is confident that this can be done without univalence. And I would agree with this assessment. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 6998 bytes --] <div dir="ltr"><br><br>On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">HoTT instead expands the notion of "equality" to <br>essentially mean "isomorphism" and requires transporting along it as a <br>nontrivial action. I doubt that that's what you have in mind, but <br>maybe you could explain what you do mean? <br></blockquote><div><br></div><div> I think terminology and notation alone cause a lot of confusion (and I</div><div>have said this many times in this list in the past, before Kevin joined in).</div><div><br></div><div>Much of the disagreement is not a real disagreement but a</div><div>misunderstanding.</div><div><br></div><div> * In HoTT, or in univalent mathematics, we use the terminology</div><div> "equals" and the notation "=" for something that is not the same</div><div> notion as in "traditional mathematics".</div><div><br></div><div> * Before the univalence axiom, we had Martin-Loef's identity type.</div><div><br></div><div> * It was *intended* to capture equality *as used by mathematicians*</div><div> (constructive or not).</div><div><br></div><div> * But it didn't. Hofmann and Streicher proved that.</div><div><br></div><div> * The identity type captures something else.</div><div><br></div><div> It certainly doesn't capture truth-valued equality by default.</div><div><br></div><div> In particular, Voevosdky showed that it captures isomorphism of</div><div> sets, and more generality equivalence of ∞-groupoids.</div><div><br></div><div> But this is distorting history a bit.</div><div><br></div><div> In the initial drafts of his "homotopy lambda calculus", he tried</div><div> come up with a new construction in type theory to capture</div><div> equivalence.</div><div><br></div><div> It was only later that he found out that what he needed was</div><div> precisely Martin-Loef's identity type.</div><div><br></div><div> * So writing "x = y" for the identity type is a bit perverse.</div><div><br></div><div> People may say, and they have said "but there is no other sensible</div><div> notion of equality for such type theories.</div><div><br></div><div> That may be so, but because, in any case, *it is not the same</div><div> notion of equality*, we should not use the same symbol.</div><div><br></div><div> * Similarly, writing "X ≃ Y" is a bit perverse, too.</div><div><br></div><div> In truth-valued mathematics, "X ≃ Y" is most of the time intended</div><div> to be truth-valued, not set-valued.</div><div><br></div><div> (Exception: category theory. E.g. we write a long chain of</div><div> isomorphisms to establish that two objects are isomorphic. Then we</div><div> learn that the author of such a proof was not interested in the</div><div> existence of an isomorphism, but instead to provide an</div><div> example. Such a proof/construction is usually concluded by saying</div><div> something like "by chasing the isomorphism, we see that we can take</div><div> [...] as our desired isomorphism.)</div><div><br></div><div><br></div><div> * With the above out of the way, we can consider the imprecise slogan</div><div> "isomorphic types are equal".</div><div><br></div><div> The one thing that the univalence axiom doesn't say is that</div><div> isomorphic type are equal.</div><div><br></div><div> What it does say is that the *identity type* Id X Y is in canonical</div><div> bijection with the type X ≃ Y of equivalences.</div><div><br></div><div> * What is the effect of this?</div><div><br></div><div> - That the identity type behaves like isomorphism, rather than like</div><div> equality.</div><div><br></div><div> - And that isomorphism behaves a little bit like equality.</div><div><br></div><div> The important thing above is "a little bit".</div><div><br></div><div> In particular, we cannot *substitute* things by isomorphic</div><div> things. We can only *transport* them (just like things work as</div><div> usual with isomorphisms).</div><div><br></div><div> * Usually, the univalence axioms is expressed as a relation between</div><div> equality and isomorphism.</div><div><br></div><div> Where by equality we don't mean equality but instead the identity</div><div> type.</div><div><br></div><div> A way to avoid these terminological problems is to formulate</div><div> univalence as a property of isomorphisms, or more precisely</div><div> equivalences.</div><div><br></div><div> To show that all equivalences satisfy a given property, it is</div><div> enough to prove that all the identity equivalence between any two</div><div> types have this property.</div><div><br></div><div> * So, as Mike says above, most of the time we can work with type</div><div> equivalence rather than "type equality". And I do too.</div><div><br></div><div> Something that is not well explained at all in the literature is</div><div> when and how the univalence axiom *actually makes a difference*.</div><div><br></div><div> (I guess this is not well understood. I used to thing that the</div><div> univalence axioms makes a difference only for types that are not</div><div> sets. But actually, for example, the univalence axiom is needed (in</div><div> the absence of the K axiom) to prove that the type of ordinals is a</div><div> set.)</div><div><br></div><div> * One example: object classifiers, subtype classifiers, ...</div><div><br></div><div> * Sometimes the univalence axiom may be *convenient* but *not needed*.</div><div><br></div><div> I guess that Kevin is, in particular, saying precisely that. In all</div><div> cases where he needs to transport constructions along isomorphisms,</div><div> he is confident that this can be done without univalence. And I</div><div> would agree with this assessment.</div><div><br></div><div>Best,</div><div>Martin</div><div><br></div><div><br></div><div> </div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 2008 bytes --] On Tuesday, November 26, 2019 at 1:25:37 AM UTC+1, Michael Shulman wrote: > > On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard > > However my *current* opinion is that it is not as easy as this, because > I believe that the correct "axiom" is that "canonically" isomorphic objects > are equal and that the HoTT axiom is too strong. > > This doesn't really make sense to me; I can't figure out what you mean > by "too strong". > Of course I agree with Mike that univalence is not “too strong”: it merely implements the mathematically right notion of identity for types and other structures built from types, such as rings, etc. But if I may venture a guess, I'd say that Kevin wants a “canonical reflection rule”: canonical identifications should correspond to judgmental equalities. We've had some discussions before about the underlying meaning of judgmental equality (invoking Frege's Sinn/Bedeutung distinction among other ideas), but I don't know whether we tried saying judgmental/definitional equality should include canonical equality, whatever that is. This might be really useful, but I think we're still some ways off before we can implement this idea. The first question is whether “all diagrams of canonical identifications commute”. (Besides the obvious question of defining canonical identifications in the first place :-) But the adventurous can start by playing around by adding canonical identities as rewriting rules in Agda: see Jesper Cockx' recent blog post: https://jesper.sikanda.be/posts/hack-your-type-theory.html Ulrik -- 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/2f61877b-b4ef-405a-99cc-85da227c70bc%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2645 bytes --] <div dir="ltr">On Tuesday, November 26, 2019 at 1:25:37 AM UTC+1, Michael Shulman wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard <br>> However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong. <br> <br>This doesn't really make sense to me; I can't figure out what you mean <br>by "too strong".<br></blockquote><div><br></div><div>Of course I agree with Mike that univalence is not “too strong”: it merely implements the mathematically right notion of identity for types and other structures built from types, such as rings, etc.</div><div><br></div><div>But if I may venture a guess, I'd say that Kevin wants a “canonical reflection rule”: canonical identifications should correspond to judgmental equalities. We've had some discussions before about the underlying meaning of judgmental equality (invoking Frege's Sinn/Bedeutung distinction among other ideas), but I don't know whether we tried saying judgmental/definitional equality should include canonical equality, whatever that is.</div><div><br></div><div>This might be really useful, but I think we're still some ways off before we can implement this idea. The first question is whether “all diagrams of canonical identifications commute”. (Besides the obvious question of defining canonical identifications in the first place :-)</div><div><br></div><div>But the adventurous can start by playing around by adding canonical identities as rewriting rules in Agda: see Jesper Cockx' recent blog post: <a href="https://jesper.sikanda.be/posts/hack-your-type-theory.html">https://jesper.sikanda.be/posts/hack-your-type-theory.html</a></div><div><br></div><div>Ulrik</div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/2f61877b-b4ef-405a-99cc-85da227c70bc%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/2f61877b-b4ef-405a-99cc-85da227c70bc%40googlegroups.com</a>.<br />

Thanks for sharing the details, Kevin! On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard <kevin.m.buzzard@gmail.com> wrote: > In HoTT one might naively say that these problems would not arise because isomorphic things are equal. This thought is indeed too naive, but, I think, not for the reason you give. In a non-univalent type theory, you have to prove manually that everything in sight respects isomorphisms. This is I think the point you were making about why the original approach got so messy. HoTT does solve this problem: because isomorphisms can be made into equalities, everything automatically respects isomorphisms. The problem is that in traditional "Book" HoTT, when you make an isomorphism into an equality, the original isomorphism is only remembered "up to homotopy", and then when you apply the transport across that equality (i.e. you use the fact that everything automatically respects it), it takes work to prove that what you get out in fact coincides with what you thought it was supposed to be (i.e. the result of actually applying the isomorphism you started by defining). In fact, dealing with these "univalence-redexes" is so painful that when formalizing mathematics in Book HoTT we (at least, in the HoTT/Coq library) generally avoid making isomorphisms into equalities as much as possible! The only place you might get some mileage is when, as Valery pointed out, what you're transporting is the mere truth of a proposition and so it doesn't matter what the "result" of the transport is. So while it might be interesting to try to formalize schemes in Book HoTT, I wouldn't expect much improvement, and it's not a project I would wish on anyone. What I do think would be worth doing and comparing would be to formalize schemes in some kind of cubical type theory. In that case, univalence actually computes and so you can hope that the proof assistant can actually recover the original isomorphism for you automatically. This may not be quite true (https://groups.google.com/d/topic/homotopytypetheory/wCU0V8RD1LQ/discussion) but it's much closer to true, and I think it would be extremely interesting to formalize schemes in a cubical type theory and compare to your developments. In a nutshell, one could say that the composition algorithms of cubical type theory are a generic implementation of the fact that everything definable in type theory respects isomorphisms, so that essentially all of the nasty lemmas should be proven for you already -- with, moreover, the proofs that you would have given, rather than (as in Book HoTT) a proof that isn't very useful because it takes a lot of effort to extract the "correct" proof. > However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong. This doesn't really make sense to me; I can't figure out what you mean by "too strong". It's certainly not inconsistent, since we have semantic models; in particular, schemes defined in HoTT would specialize in the simplicial set model to the classical notion of scheme. And I can't imagine any way that the presence of univalence could "get in the way" or "backfire". Usually when people say that univalence sounds "wrong", it's because they're thinking of "equality" as a substitutive mere property and "isomorphic types as equal" as somehow collapsing to a categorical skeleton, which is of course a misconception -- HoTT instead expands the notion of "equality" to essentially mean "isomorphism" and requires transporting along it as a nontrivial action. I doubt that that's what you have in mind, but maybe you could explain what you do mean? > By "mathematicians" here I really mean my ugly phrase "proper mathematicians", i.e. people doing algebra/number theory/geometry/topology etc, people who have absolutely no idea what a type is and would even struggle to list the axioms of set theory. It would be nice if there were a phrase for this that didn't sound insulting to us "improper" mathematicians. Mac Lane's similar phrase "working mathematician" is not really any more flattering to the "non-working" mathematicians. (-: Mike -- 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/CAOvivQz3jn5jcjbeeK%2BG2dJ_n_AuZT43pSQ%2Bq5z8Roq_YFzQpw%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 8277 bytes --] > Kevin, I would like to second Michael's interest in seeing these 20 > commutative diagrams. Moreover, I'd also be very interested in seeing > your "spaghetti code" (quote from the slides of your Big Proof talk): it > seems it should be informative to see where your initial approach went > wrong, and how much these problems and their solution had anything to do > at all with the formal system you were working in. Are your original > files perhaps available somewhere? > Sorry for the delay. My original repo with a "bad" theorem is here: https://github.com/kbuzzard/lean-stacks-project The bad theorem is this: https://stacks.math.columbia.edu/tag/00EJ The problem is that the rings denoted R_{f_i} (localisations of rings) are typically defined to mathematicians as "this explicit construction here" as opposed to "the unique up to unique isomorphism ring having some explicit property" and, as a mathematician, I formalised (or more precisely got Imperial College maths undergraduates Chris Hughes and Kenny Lau to formalise) the explicit construction of the localisation and then the explicit theorem as stated in the stacks project, not understanding at the time that this would lead to trouble. When I came to apply it, I ran into the issue that on this page https://stacks.math.columbia.edu/tag/01HR we have the quote: "If f, g in R are such that D(f)=D(g), then by Lemma 26.5.1 there are canonical maps M_f->M_g and M_g->M_f which are mutually inverse. Hence [we can regard M_f and M_g as equal]". This is a typical mathematician's usage of the word "canonical" -- it means "I give you my mathematician's guarantee that I will never do anything to M_f which won't work in exactly the same way as M_g so you can replace one by the other and I won't mind". As I explained earlier, by the time I noticed this subtlety it was too late, and this led to this horrorshow: https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268 plus the lines following, all of which is applied here https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208 . That last link is justifying a whole bunch of rewrites along canonical isomorphisms. These were the general lemmas I needed to prove that if A -> B was a map, and if A was canonically isomorphic to A' and if B was canonically isomorphic to B' and A' -> B' was the corresponding map, then the image of A was canonically isomorphic to the image of A' etc, all in some very specific situation where "canonically isomorphic" was typically replaced by "unique isomorphism satisfying this list of properties". Note that this is crappy old code written by me when I had no idea what I was doing. One very interesting twist was this: the universal property of localisation for the localised ring R_f is a statement which says that under certain circumstances there is a unique ring homomorphism from R_f; however in https://stacks.math.columbia.edu/tag/00EJ the map beta in the statement of the lemma is *not* a ring homomorphism and so a naive application the universal property was actually *not enough*! One has to reformulate the lemma in terms of equalisers of ring homomorphisms and remove mention of beta. None of this is mentioned in the stacks project website because we are covered by the fact that everything is "canonical" so it's all bound to work -- and actually this is *true* -- we are very good at using this black magic word. All of this is fixed in Ramon Mir's MSc project https://github.com/ramonfmir/lean-scheme and the explanations of how it was fixed are in his write-up here https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf Briefly, one crucial input was that the localisation map R -> R_f could be characterised up to unique isomorphism in the category of R-algebras by something far more concrete than the universal property, and Ramon used this instead. In HoTT one might naively say that these problems would not arise because isomorphic things are equal. However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong. I developed some rather primitive tools to rewrite certain statements along certain kinds of isomorphisms with some naturality properties, and mathematicians would be happy with these ideas. I can quite believe that if you stick to homotopy types with the model in your mind as being topological spaces up to homotopy then the HoTT axiom is perfect. However there are things other than topological spaces in mathematics, for example commutative rings, and in my mind the HoTT axiom just looks weird and wrong in ring theory, and I expect it to backfire when HoTT people start doing some serious ring theory. I might be wrong. Part of me hopes I'm wrong, in fact. But this will remain my opinion until someone comes along and formalises the definition of a scheme in one of the HoTT theories and proves the "theorem" that an affine scheme is a scheme (I write "theorem" in quotes because it is a construction, not a theorem). I had the pleasure of meeting Thorsten Altenkirch earlier this week and I asked him why this had not been done yet, and he told me that they were just waiting for the right person to come along and do it. A year or so ago I was of the opinion that more mathematicians should be using Lean but now I have come to the conclusion that actually more mathematicians should be engaging with *all* of the theorem provers, so we can find out which provers are the most appropriate for which areas. By "mathematicians" here I really mean my ugly phrase "proper mathematicians", i.e. people doing algebra/number theory/geometry/topology etc, people who have absolutely no idea what a type is and would even struggle to list the axioms of set theory. These people with their "canonical" constructions (a phrase which has no meaning) are the problem, and they're very hard to reach because currently these systems offer them nothing they need. I wrote a silly game http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ to help my 1st years revise for my exam (and the game takes things much further than the contents of the course), and I'm writing a real number game too, to help my 1st years revise analysis for their January exam. It would not be hard to write analogous such games in one of the HoTT theories, I would imagine. From what I have seen, it seems to me that Isabelle is a fabulous tool for classical analysis, Coq is great for finite group theory, the Kepler conjecture is proved in other HOL systems, and the HoTT systems are great for the theory of topological spaces up to homotopy. But number theory has been around for millennia and unfortunately uses analysis, group theory and topological spaces, and I want one system which can do all of them. I think that we can only find out the limitations of these systems by doing a whole bunch of "proper mathematics" in all of them. I think it's appalling that none of them can even *state* the Hodge conjecture, for example. For me, that is a very simple reason for a "proper mathematician" to immediately reject all of them in 2019. But I digress. Kevin > > > -- > > Nicolas > > > > > -- > 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/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz > . > -- 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/CAH52Xb2AoMWBeCCJ5B8%3DDfa8UgmO1vbWf7a%3DdvfRqTFTdu61qA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 10887 bytes --] <div dir="ltr"><br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> Kevin, I would like to second Michael's interest in seeing these 20<br> commutative diagrams. Moreover, I'd also be very interested in seeing<br> your "spaghetti code" (quote from the slides of your Big Proof talk): it<br> seems it should be informative to see where your initial approach went<br> wrong, and how much these problems and their solution had anything to do<br> at all with the formal system you were working in. Are your original<br> files perhaps available somewhere?<br></blockquote><div><br></div><div>Sorry for the delay.</div><div><br></div><div>My original repo with a "bad" theorem is here:</div><div><br></div><div><a href="https://github.com/kbuzzard/lean-stacks-project">https://github.com/kbuzzard/lean-stacks-project</a></div><div><br></div><div>The bad theorem is this:</div><div><br></div><div><a href="https://stacks.math.columbia.edu/tag/00EJ">https://stacks.math.columbia.edu/tag/00EJ</a></div><div><br></div><div>The problem is that the rings denoted R_{f_i} (localisations of rings) are typically defined to mathematicians as "this explicit construction here" as opposed to "the unique up to unique isomorphism ring having some explicit property" and, as a mathematician, I formalised (or more precisely got Imperial College maths undergraduates Chris Hughes and Kenny Lau to formalise) the explicit construction of the localisation and then the explicit theorem as stated in the stacks project, not understanding at the time that this would lead to trouble. When I came to apply it, I ran into the issue that on this page<br></div><div><br></div><div><a href="https://stacks.math.columbia.edu/tag/01HR">https://stacks.math.columbia.edu/tag/01HR</a></div><div><br></div><div>we have the quote: "If f, g in R are such that D(f)=D(g), then by Lemma 26.5.1 there are canonical maps M_f->M_g and M_g->M_f which are mutually inverse. Hence [we can regard M_f and M_g as equal]".</div><div><br></div><div>This is a typical mathematician's usage of the word "canonical" -- it means "I give you my mathematician's guarantee that I will never do anything to M_f which won't work in exactly the same way as M_g so you can replace one by the other and I won't mind". <br></div><div><br></div><div>As I explained earlier, by the time I noticed this subtlety it was too late, and this led to this horrorshow:</div><div><br></div><div><a href="https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268">https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268</a></div><div><br></div><div>plus the lines following, all of which is applied here</div><div><br></div><div><a href="https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208">https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208</a></div><div><br></div><div>. That last link is justifying a whole bunch of rewrites along canonical isomorphisms. These were the general lemmas I needed to prove that if A -> B was a map, and if A was canonically isomorphic to A' and if B was canonically isomorphic to B' and A' -> B' was the corresponding map, then the image of A was canonically isomorphic to the image of A' etc, all in some very specific situation where "canonically isomorphic" was typically replaced by "unique isomorphism satisfying this list of properties". Note that this is crappy old code written by me when I had no idea what I was doing. One very interesting twist was this: the universal property of localisation for the localised ring R_f is a statement which says that under certain circumstances there is a unique ring homomorphism from R_f; however in <a href="https://stacks.math.columbia.edu/tag/00EJ">https://stacks.math.columbia.edu/tag/00EJ</a> the map beta in the statement of the lemma is *not* a ring homomorphism and so a naive application the universal property was actually *not enough*! One has to reformulate the lemma in terms of equalisers of ring homomorphisms and remove mention of beta. None of this is mentioned in the stacks project website because we are covered by the fact that everything is "canonical" so it's all bound to work -- and actually this is *true* -- we are very good at using this black magic word. <br></div><div><br></div><div>All of this is fixed in Ramon Mir's MSc project<br></div><div><br></div><div><a href="https://github.com/ramonfmir/lean-scheme">https://github.com/ramonfmir/lean-scheme</a></div><div><br></div><div>and the explanations of how it was fixed are in his write-up here</div><div><br></div><div><a href="https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf">https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf</a></div><div><br></div><div>Briefly, one crucial input was that the localisation map R -> R_f could be characterised up to unique isomorphism in the category of R-algebras by something far more concrete than the universal property, and Ramon used this instead.</div><div><br></div><div>In HoTT one might naively say that these problems would not arise because isomorphic things are equal. However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong. I developed some rather primitive tools to rewrite certain statements along certain kinds of isomorphisms with some naturality properties, and mathematicians would be happy with these ideas. I can quite believe that if you stick to homotopy types with the model in your mind as being topological spaces up to homotopy then the HoTT axiom is perfect. However there are things other than topological spaces in mathematics, for example commutative rings, and in my mind the HoTT axiom just looks weird and wrong in ring theory, and I expect it to backfire when HoTT people start doing some serious ring theory. I might be wrong. Part of me hopes I'm wrong, in fact. But this will remain my opinion until someone comes along and formalises the definition of a scheme in one of the HoTT theories and proves the "theorem" that an affine scheme is a scheme (I write "theorem" in quotes because it is a construction, not a theorem). I had the pleasure of meeting Thorsten Altenkirch earlier this week and I asked him why this had not been done yet, and he told me that they were just waiting for the right person to come along and do it. A year or so ago I was of the opinion that more mathematicians should be using Lean but now I have come to the conclusion that actually more mathematicians should be engaging with *all* of the theorem provers, so we can find out which provers are the most appropriate for which areas. By "mathematicians" here I really mean my ugly phrase "proper mathematicians", i.e. people doing algebra/number theory/geometry/topology etc, people who have absolutely no idea what a type is and would even struggle to list the axioms of set theory. These people with their "canonical" constructions (a phrase which has no meaning) are the problem, and they're very hard to reach because currently these systems offer them nothing they need. I wrote a silly game</div><div><br></div><div><a href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/</a></div><div><br></div><div>to help my 1st years revise for my exam (and the game takes things much further than the contents of the course), and I'm writing a real number game too, to help my 1st years revise analysis for their January exam. It would not be hard to write analogous such games in one of the HoTT theories, I would imagine.</div><div><br></div><div>From what I have seen, it seems to me that Isabelle is a fabulous tool for classical analysis, Coq is great for finite group theory, the Kepler conjecture is proved in other HOL systems, and the HoTT systems are great for the theory of topological spaces up to homotopy. But number theory has been around for millennia and unfortunately uses analysis, group theory and topological spaces, and I want one system which can do all of them. I think that we can only find out the limitations of these systems by doing a whole bunch of "proper mathematics" in all of them. I think it's appalling that none of them can even *state* the Hodge conjecture, for example. For me, that is a very simple reason for a "proper mathematician" to immediately reject all of them in 2019. But I digress.</div><div><br></div><div>Kevin<br> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <br> <br> --<br> <br> Nicolas<br> <br> <br> <br> <br> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz" rel="noreferrer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz</a>.<br> </blockquote></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb2AoMWBeCCJ5B8%3DDfa8UgmO1vbWf7a%3DdvfRqTFTdu61qA%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH52Xb2AoMWBeCCJ5B8%3DDfa8UgmO1vbWf7a%3DdvfRqTFTdu61qA%40mail.gmail.com</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 7355 bytes --] SIXTH SYMPOSIUM ON COMPOSITIONAL STRUCTURES (SYCO 6) -- including a Category Theory PhD Recruitment Fair -- University of Leicester, UK 16-17 December, 2019 http://events.cs.bham.ac.uk/syco/6/ The Symposium on Compositional Structures (SYCO) is an interdisciplinary series of meetings aiming to support the growing community of researchers interested in the phenomenon of compositionality, from both applied and abstract perspectives, and in particular where category theory serves as a unifying common language. Previous SYCO events have been held at University of Birmingham, University of Strathclyde, University of Oxford, and Chapman University. We welcome submissions from researchers across computer science, mathematics, physics, philosophy, and beyond, with the aim of fostering friendly discussion, disseminating new ideas, and spreading knowledge between fields. Submission is encouraged for both mature research and work in progress, and by both established academics and junior researchers, including students. Submission is easy, with no format requirements or page restrictions. The meeting does not have proceedings, so work can be submitted even if it has been submitted or published elsewhere. Think creatively--- you could submit a recent paper, or notes on work in progress, or even a recent Masters or PhD thesis. While no list of topics could be exhaustive, SYCO welcomes submissions with a compositional focus related to any of the following areas, in particular from the perspective of category theory: - logical methods in computer science, including classical and quantum programming, type theory, concurrency, natural language processing and machine learning; - graphical calculi, including string diagrams, Petri nets and reaction networks; - languages and frameworks, including process algebras, proof nets, type theory and game semantics; - abstract algebra and pure category theory, including monoidal category theory, higher category theory, operads, polygraphs, and relationships to homotopy theory; - quantum algebra, including quantum computation and representation theory; - tools and techniques, including rewriting, formal proofs and proof assistants, and game theory; - industrial applications, including case studies and real-world problem descriptions. This new series aims to bring together the communities behind many previous successful events which have taken place over the last decade, including "Categories, Logic and Physics", "Categories, Logic and Physics (Scotland)", "Higher-Dimensional Rewriting and Applications", "String Diagrams in Computation, Logic and Physics", "Applied Category Theory", "Simons Workshop on Compositionality", and the "Peripatetic Seminar in Sheaves and Logic". SYCO is a regular fixture in the academic calendar, running regularly throughout the year, and becoming over time a recognized venue for presentation and discussion of results in an informal and friendly atmosphere. To help create this community, and to avoid the need to make difficult choices between strong submissions, in the event that more good-quality submissions are received than can be accommodated in the timetable, the programme committee may choose to *defer* some submissions to a future meeting, rather than reject them. This would be done based largely on submission order, giving an incentive for early submission, but would also take into account other requirements, such as ensuring a broad scientific programme. Deferred submissions can be re-submitted to any future SYCO meeting, where they would not need peer review, and where they would be prioritised for inclusion in the programme. This will allow us to ensure that speakers have enough time to present their ideas, without creating an unnecessarily competitive reviewing process. Meetings will be held sufficiently frequently to avoid a backlog of deferred papers. # INVITED SPEAKERS Gabriella Bohm, Wigner Research Centre for Physics Jennifer Hackett, University of Nottingham # PhD RECRUITMENT FAIR This event will include a poster session advertising PhD opportunities in category theory and related disciplines. If you are interested in advertising PhD opportunities at your institution, please email Simona Paoli at <sp424@leicester.ac.uk>. We expect significant participation from Masters students and final-year undergraduates who are considering further study in this area. # ACCEPTED PAPERS Dorette Pronk and Laura Scull - New Results on Bicategories of Fractions Applied to Orbifolds Amar Hadzihasanovic - Representable diagrammatic sets as a model of weak higher categories Drew Moshier and Steve Vickers - Cartesian bicategories and their Karoubi envelopes Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski and Fabio Zanasi - Contextual Equivalence for Signal Flow Graphs (Extended Abstract) Vincent Wang - Graphical Grammar + Graphical Completion of Monoidal Categories John Stell - Mathematical Morphology on Graphs: The role of relations on hypergraphs Quanlong Wang - An algebraic axiomatisation of ZX-calculus Morgan Rogers and Jens Hemelaer Monoid Properties as Topos-Theoretic Invariants Maaike Zwart and Dan Marsden - Composite Theories, and how to use them to prove no-go theorems for distributive laws Louis Parlant - Monoidal Monads and Preservation of Equations Callum Reader - Probability Monads for Enriched Categories Guillaume Boisseau - String diagrams for optics Dan Shiebler, Alexis Toumi and Mehrnoosh Sadrzadeh - Incremental Monoidal Grammars # IMPORTANT DATES Registration deadline: Monday 9th December 2019 Symposium dates: Monday 16th and Tuesday 17th December 2019 # Programme Committee Fatimah Ahmadi, University of Oxford Miriam Backens, University of Birmingham Nicolas Behr, Institut de Recherche en Informatique Fondamentale (IRIF), Universite Paris-Diderot - Paris 7 Carmen Maria Constantin, University of Oxford Chris Heunen, University of Edinburgh, Dominic Horsman, University of Grenoble Aleks Kissinger, University of Oxford Eliana Lorch, Thiel Fellowship Dan Marsden, University of Oxford (PC Chair) Samuel Mimram, Ecole Polytechnique Koko Muroya, RIMS, Kyoto University & University of Birmingham Simona Paoli, University of Leicester Mehrnoosh Sadrzadeh, University College London Alessio Santamaria, Queen Mary University of London Alexandra Silva, University College London Pawel Sobocinski, Tallinn University of Technology Jamie Vicary, University of Birmingham and University of Oxford Philip Zahn, University of St Gallen Tamara von Glehn # Steering Committee Ross Duncan, University of Strathclyde Chris Heunen, University of Edinburgh Dominic Horsman, University of Grenoble Alek Kissinger, University of Oxford Samuel Mimram, Ecole Polytechnique Simona Paoli, University of Leicester Mehrnoosh Sadrzadeh, University College London Pawel Sobocinski, Tallinn University of Technology Jamie Vicary, University of Birmingham and University of Oxford -- 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/5fb12ce2-f052-4d45-99f8-1bc0afc8fe67%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 9388 bytes --] <div dir="ltr"><div>SIXTH SYMPOSIUM ON COMPOSITIONAL STRUCTURES (SYCO 6)</div><div>-- including a Category Theory PhD Recruitment Fair --</div><div><br></div><div>University of Leicester, UK</div><div> 16-17 December, 2019</div><div><br></div><div> http://events.cs.bham.ac.uk/syco/6/</div><div><br></div><div>The Symposium on Compositional Structures (SYCO) is an</div><div>interdisciplinary series of meetings aiming to support the growing</div><div>community of researchers interested in the phenomenon of</div><div>compositionality, from both applied and abstract perspectives, and in</div><div>particular where category theory serves as a unifying common language.</div><div>Previous SYCO events have been held at University of Birmingham,</div><div>University of Strathclyde, University of Oxford, and Chapman University.</div><div><br></div><div>We welcome submissions from researchers across computer science,</div><div>mathematics, physics, philosophy, and beyond, with the aim of</div><div>fostering friendly discussion, disseminating new ideas, and spreading</div><div>knowledge between fields. Submission is encouraged for both mature</div><div>research and work in progress, and by both established academics and</div><div>junior researchers, including students.</div><div><br></div><div>Submission is easy, with no format requirements or page restrictions.</div><div>The meeting does not have proceedings, so work can be submitted even</div><div>if it has been submitted or published elsewhere. Think creatively---</div><div>you could submit a recent paper, or notes on work in progress, or even</div><div>a recent Masters or PhD thesis.</div><div><br></div><div>While no list of topics could be exhaustive, SYCO welcomes submissions</div><div>with a compositional focus related to any of the following areas, in</div><div>particular from the perspective of category theory:</div><div><br></div><div>- logical methods in computer science, including classical and</div><div>quantum programming, type theory, concurrency, natural language</div><div>processing and machine learning;</div><div><br></div><div>- graphical calculi, including string diagrams, Petri nets and</div><div>reaction networks;</div><div><br></div><div>- languages and frameworks, including process algebras, proof nets,</div><div>type theory and game semantics;</div><div><br></div><div>- abstract algebra and pure category theory, including monoidal</div><div>category theory, higher category theory, operads, polygraphs, and</div><div>relationships to homotopy theory;</div><div><br></div><div>- quantum algebra, including quantum computation and representation</div><div>theory;</div><div><br></div><div>- tools and techniques, including rewriting, formal proofs and proof</div><div>assistants, and game theory;</div><div><br></div><div>- industrial applications, including case studies and real-world</div><div>problem descriptions.</div><div><br></div><div>This new series aims to bring together the communities behind many</div><div>previous successful events which have taken place over the last</div><div>decade, including "Categories, Logic and Physics", "Categories, Logic</div><div>and Physics (Scotland)", "Higher-Dimensional Rewriting and</div><div>Applications", "String Diagrams in Computation, Logic and Physics",</div><div>"Applied Category Theory", "Simons Workshop on Compositionality", and</div><div>the "Peripatetic Seminar in Sheaves and Logic".</div><div><br></div><div>SYCO is a regular fixture in the academic calendar, running</div><div>regularly throughout the year, and becoming over time a recognized</div><div>venue for presentation and discussion of results in an informal and</div><div>friendly atmosphere. To help create this community, and to avoid the</div><div>need to make difficult choices between strong submissions, in the</div><div>event that more good-quality submissions are received than can be</div><div>accommodated in the timetable, the programme committee may choose to</div><div>*defer* some submissions to a future meeting, rather than reject them.</div><div>This would be done based largely on submission order, giving an</div><div>incentive for early submission, but would also take into account other</div><div>requirements, such as ensuring a broad scientific programme. Deferred</div><div>submissions can be re-submitted to any future SYCO meeting, where they</div><div>would not need peer review, and where they would be prioritised for</div><div>inclusion in the programme. This will allow us to ensure that speakers</div><div>have enough time to present their ideas, without creating an</div><div>unnecessarily competitive reviewing process. Meetings will be held</div><div>sufficiently frequently to avoid a backlog of deferred papers.</div><div><br></div><div># INVITED SPEAKERS</div><div><br></div><div>Gabriella Bohm, Wigner Research Centre for Physics</div><div>Jennifer Hackett, University of Nottingham</div><div><br></div><div># PhD RECRUITMENT FAIR</div><div><br></div><div>This event will include a poster session advertising PhD opportunities</div><div>in category theory and related disciplines. If you are interested in</div><div>advertising PhD opportunities at your institution, please email Simona</div><div>Paoli at <sp424@leicester.ac.uk>. We expect significant participation</div><div>from Masters students and final-year undergraduates who are</div><div>considering further study in this area.</div><div><br></div><div># ACCEPTED PAPERS</div><div><br></div><div>Dorette Pronk and Laura Scull - New Results on Bicategories of Fractions Applied to Orbifolds</div><div>Amar Hadzihasanovic - Representable diagrammatic sets as a model of weak higher categories</div><div>Drew Moshier and Steve Vickers - Cartesian bicategories and their Karoubi envelopes</div><div>Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski and Fabio Zanasi - Contextual Equivalence for Signal Flow Graphs (Extended Abstract)</div><div>Vincent Wang - Graphical Grammar + Graphical Completion of Monoidal Categories</div><div>John Stell - Mathematical Morphology on Graphs: The role of relations on hypergraphs</div><div>Quanlong Wang - An algebraic axiomatisation of ZX-calculus</div><div>Morgan Rogers and Jens Hemelaer<span style="white-space:pre"> </span>Monoid Properties as Topos-Theoretic Invariants</div><div>Maaike Zwart and Dan Marsden - Composite Theories, and how to use them to prove no-go theorems for distributive laws</div><div>Louis Parlant - Monoidal Monads and Preservation of Equations</div><div>Callum Reader - Probability Monads for Enriched Categories</div><div>Guillaume Boisseau - String diagrams for optics</div><div>Dan Shiebler, Alexis Toumi and Mehrnoosh Sadrzadeh - Incremental Monoidal Grammars</div><div><br></div><div># IMPORTANT DATES</div><div><br></div><div>Registration deadline: Monday 9th December 2019</div><div>Symposium dates: Monday 16th and Tuesday 17th December 2019</div><div><br></div><div># Programme Committee</div><div><br></div><div>Fatimah Ahmadi, University of Oxford</div><div>Miriam Backens, University of Birmingham</div><div>Nicolas Behr, Institut de Recherche en Informatique Fondamentale (IRIF), Universite Paris-Diderot - Paris 7</div><div>Carmen Maria Constantin, University of Oxford</div><div>Chris Heunen, University of Edinburgh,</div><div>Dominic Horsman, University of Grenoble</div><div>Aleks Kissinger, University of Oxford</div><div>Eliana Lorch, Thiel Fellowship</div><div>Dan Marsden, University of Oxford (PC Chair)</div><div>Samuel Mimram, Ecole Polytechnique</div><div>Koko Muroya, RIMS, Kyoto University & University of Birmingham</div><div>Simona Paoli, University of Leicester</div><div>Mehrnoosh Sadrzadeh, University College London</div><div>Alessio Santamaria, Queen Mary University of London</div><div>Alexandra Silva, University College London</div><div>Pawel Sobocinski, Tallinn University of Technology</div><div>Jamie Vicary, University of Birmingham and University of Oxford</div><div>Philip Zahn, University of St Gallen</div><div>Tamara von Glehn</div><div><br></div><div># Steering Committee</div><div><br></div><div>Ross Duncan, University of Strathclyde</div><div>Chris Heunen, University of Edinburgh</div><div>Dominic Horsman, University of Grenoble</div><div>Alek Kissinger, University of Oxford</div><div>Samuel Mimram, Ecole Polytechnique</div><div>Simona Paoli, University of Leicester</div><div>Mehrnoosh Sadrzadeh, University College London</div><div>Pawel Sobocinski, Tallinn University of Technology</div><div>Jamie Vicary, University of Birmingham and University of Oxford</div><div><br></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/5fb12ce2-f052-4d45-99f8-1bc0afc8fe67%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/5fb12ce2-f052-4d45-99f8-1bc0afc8fe67%40googlegroups.com</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 4485 bytes --] Hi! My guess would be that differentiability is irrelevant for knot theory. You could rather consider closed subsets homeomorphic to S^1. For instance you could restrict your attention to "paths" consisting of injective sequences of integral points P1, ... , Pi, ..., Pn=P0, where PiPi+1 is parallel to an axis and of length 1. There is probably a corresponding notion of "discrete" isotopy among such paths, so that if two such paths are continuously isotopic, they are also discretely isotopic . As a consequence knots now live in Z^3. So you can take the higher inductive type H with Z^3 as set of points, and the above (length one) intervals as generating equalities, and study "synthetic knots" in there. The first thing to check is probably that any path in H is homotopic to a path obtained from a sequence of generators. I am not sure at all that such a synthetic knot theory could be fruitful May-be more interesting is to fill the holes in the H above by adding generating 2-cells one for each elementary square and 3-cells one for each elementary cube. It is not so clear how to do it if you want these cells to be "invertible" More generally given a triangulated variety of dimension 3, you may try to specify as above a higher-inductive type, so that you could try to formulate (and prove...) a synthetic Poincaré conjecture. Sorry for divagating slightly too much! ah Le mer. 20 nov. 2019 à 20:13, Ali Caglayan <alizter@gmail.com> a écrit : > It seems to me that "differentially cohesive HoTT", whatever it ends up > being, is exactly the kind of viewpoint needed to study knot theory. The > following characterisation of knot theory (I think?) due to Allen Hatcher > might make this more apparent: > > Knot theory is the study of path-components of the space of smooth > submanifolds of S^3 diffeomorphic to S^1. > > So you need to be able to talk about a space being smooth, pick a smooth > structure for S^3 and S^1, what it means to be an immersion into a manifold > (submanifold) and diffeomorphisms. This is just stating what knot theory > ought to be, I have no idea if this viewpoint can actually tell you > anything until we have some workable theory of differential cohesion. > Currently we only have real-cohesive versions of HoTT. > > Some starter questions would be: > - Can you characterize the trivial knot. > - How do you define the "connected sum" of knots. > - How do you show every knot has an "inverse" with respect to the sum. > > > On Thursday, 19 July 2018 09:55:55 UTC+1, Ali Caglayan wrote: >> >> From what I have seen knot-theory has been very resistant to homotopy >> theoretic ideas (not classical ones). One 'clean' way of working with knot >> theory is to do so in the context of differential geometry. Cohesive HoTT >> supposedly can develop adequate differential geometry but at the moment it >> is very undeveloped. >> >> One of the difficulties with knot theory is that (classical) homotopy >> theory in HoTT isn't really done with real numbers and interval objects, >> which is needed if you want to define notions of ambient isotopy and such. >> >> I think the main difficulty here might be that HoTT is great at doing >> (synthetic) homotopy but not topology. The two can be easily confused. How >> do you take the complement of a space for example? >> >> I could be wrong however but this is the conclusion I got when I tried >> thinking about HoTT knots. >> > -- > 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/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.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/CAHPPr6zWU1VN7J_NXTJQ6ZuLc3TjrJ7yfJwMDqPuVu005%2BJqzA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5731 bytes --] <div dir="ltr"><div>Hi!</div><div><br></div><div> <div>My guess would be that differentiability is irrelevant for knot theory. <br></div><div>You could rather consider closed subsets homeomorphic to S^1. For instance you could restrict your attention to "paths" consisting of injective sequences of integral points <br></div><div>P1, ... , Pi, ..., Pn=P0, where PiPi+1 is parallel to an axis and of length 1. There is probably a corresponding notion of "discrete" isotopy among such paths, so that if two such paths are continuously isotopic, they are also discretely isotopic . As a consequence knots now live in Z^3.</div><div>So you can take the higher inductive type H with Z^3 as set of points, and the above (length one) intervals as generating equalities, and study "synthetic knots" in there. The first thing to check is probably that any path in H is homotopic to a path obtained from a sequence of generators.</div><div>I am not sure at all that such a synthetic knot theory could be fruitful May-be more interesting is to fill the holes in the H above by adding generating 2-cells one for each elementary square and 3-cells one for each elementary cube. It is not so clear how to do it if you want these cells to be "invertible" More generally given a triangulated variety of dimension 3, you may try to specify as above a higher-inductive type, so that you could try to formulate (and prove...) a synthetic Poincaré conjecture. <br></div><div><br></div><div>Sorry for divagating slightly too much!</div><div><br></div><div>ah<br></div><div><br></div><div><br></div> </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Le mer. 20 nov. 2019 à 20:13, Ali Caglayan <<a href="mailto:alizter@gmail.com" target="_blank">alizter@gmail.com</a>> a écrit :<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>It seems to me that "differentially cohesive HoTT", whatever it ends up being, is exactly the kind of viewpoint needed to study knot theory. The following characterisation of knot theory (I think?) due to Allen Hatcher might make this more apparent:</div><div><br></div><div>Knot theory is the study of path-components of the space of smooth submanifolds of S^3 diffeomorphic to S^1.</div><div><br></div><div>So you need to be able to talk about a space being smooth, pick a smooth structure for S^3 and S^1, what it means to be an immersion into a manifold (submanifold) and diffeomorphisms. This is just stating what knot theory ought to be, I have no idea if this viewpoint can actually tell you anything until we have some workable theory of differential cohesion. Currently we only have real-cohesive versions of HoTT.</div><div><br></div><div>Some starter questions would be:</div><div> - Can you characterize the trivial knot.<br></div><div> - How do you define the "connected sum" of knots.</div><div> - How do you show every knot has an "inverse" with respect to the sum.</div><div><br></div><div><br></div>On Thursday, 19 July 2018 09:55:55 UTC+1, Ali Caglayan wrote:<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>From what I have seen knot-theory has been very resistant to homotopy theoretic ideas (not classical ones). One 'clean' way of working with knot theory is to do so in the context of differential geometry. Cohesive HoTT supposedly can develop adequate differential geometry but at the moment it is very undeveloped.</div><div><br></div><div>One of the difficulties with knot theory is that (classical) homotopy theory in HoTT isn't really done with real numbers and interval objects, which is needed if you want to define notions of ambient isotopy and such.</div><div><br></div><div>I think the main difficulty here might be that HoTT is great at doing (synthetic) homotopy but not topology. The two can be easily confused. How do you take the complement of a space for example?</div><div><br></div><div>I could be wrong however but this is the conclusion I got when I tried thinking about HoTT knots.<br></div></div></blockquote></div> <p></p> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com?utm_medium=email&utm_source=footer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com</a>.<br> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAHPPr6zWU1VN7J_NXTJQ6ZuLc3TjrJ7yfJwMDqPuVu005%2BJqzA%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAHPPr6zWU1VN7J_NXTJQ6ZuLc3TjrJ7yfJwMDqPuVu005%2BJqzA%40mail.gmail.com</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 2312 bytes --] It seems to me that "differentially cohesive HoTT", whatever it ends up being, is exactly the kind of viewpoint needed to study knot theory. The following characterisation of knot theory (I think?) due to Allen Hatcher might make this more apparent: Knot theory is the study of path-components of the space of smooth submanifolds of S^3 diffeomorphic to S^1. So you need to be able to talk about a space being smooth, pick a smooth structure for S^3 and S^1, what it means to be an immersion into a manifold (submanifold) and diffeomorphisms. This is just stating what knot theory ought to be, I have no idea if this viewpoint can actually tell you anything until we have some workable theory of differential cohesion. Currently we only have real-cohesive versions of HoTT. Some starter questions would be: - Can you characterize the trivial knot. - How do you define the "connected sum" of knots. - How do you show every knot has an "inverse" with respect to the sum. On Thursday, 19 July 2018 09:55:55 UTC+1, Ali Caglayan wrote: > > From what I have seen knot-theory has been very resistant to homotopy > theoretic ideas (not classical ones). One 'clean' way of working with knot > theory is to do so in the context of differential geometry. Cohesive HoTT > supposedly can develop adequate differential geometry but at the moment it > is very undeveloped. > > One of the difficulties with knot theory is that (classical) homotopy > theory in HoTT isn't really done with real numbers and interval objects, > which is needed if you want to define notions of ambient isotopy and such. > > I think the main difficulty here might be that HoTT is great at doing > (synthetic) homotopy but not topology. The two can be easily confused. How > do you take the complement of a space for example? > > I could be wrong however but this is the conclusion I got when I tried > thinking about HoTT knots. > -- 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/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2986 bytes --] <div dir="ltr"><div>It seems to me that "differentially cohesive HoTT", whatever it ends up being, is exactly the kind of viewpoint needed to study knot theory. The following characterisation of knot theory (I think?) due to Allen Hatcher might make this more apparent:</div><div><br></div><div>Knot theory is the study of path-components of the space of smooth submanifolds of S^3 diffeomorphic to S^1.</div><div><br></div><div>So you need to be able to talk about a space being smooth, pick a smooth structure for S^3 and S^1, what it means to be an immersion into a manifold (submanifold) and diffeomorphisms. This is just stating what knot theory ought to be, I have no idea if this viewpoint can actually tell you anything until we have some workable theory of differential cohesion. Currently we only have real-cohesive versions of HoTT.</div><div><br></div><div>Some starter questions would be:</div><div> - Can you characterize the trivial knot.<br></div><div> - How do you define the "connected sum" of knots.</div><div> - How do you show every knot has an "inverse" with respect to the sum.</div><div><br></div><div><br></div>On Thursday, 19 July 2018 09:55:55 UTC+1, Ali Caglayan wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir="ltr"><div>From what I have seen knot-theory has been very resistant to homotopy theoretic ideas (not classical ones). One 'clean' way of working with knot theory is to do so in the context of differential geometry. Cohesive HoTT supposedly can develop adequate differential geometry but at the moment it is very undeveloped.</div><div><br></div><div>One of the difficulties with knot theory is that (classical) homotopy theory in HoTT isn't really done with real numbers and interval objects, which is needed if you want to define notions of ambient isotopy and such.</div><div><br></div><div>I think the main difficulty here might be that HoTT is great at doing (synthetic) homotopy but not topology. The two can be easily confused. How do you take the complement of a space for example?</div><div><br></div><div>I could be wrong however but this is the conclusion I got when I tried thinking about HoTT knots.<br></div></div></blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 3569 bytes --] ================================== ICALP-LICS 2020 Call for Workshops ================================== ICALP 2020 (http://econcs.pku.edu.cn/icalp2020/) and LICS 2020 (https://lics.siglog.org/lics20/) will take place in co-location from 8th till 12th of July 2020 in Beijing, China. The conferences will be preceded by two days of joint workshops, held on July 6th and 7th. We invite proposals of workshops affiliated with ICALP-LICS 2020 on all topics covered by ICALP and LICS, as well as other areas of theoretical computer science. Proposals should be submitted no later than *** November 30th, 2019 *** by sending an email to frederic.blanqui@inria.fr. Due to limited space of the venue we might not be able to accommodate all the proposed workshops. You should expect notification on the acceptance of your proposal by mid December 2019. A workshop proposal submission should consist of: - workshop's name and URL (if already available) - workshop's organizers together with their email addresses and web pages; - short description of the area covered by the workshop and the motivation behind it; - expected number of participants (if available, please include the data of previous years); - planned format of the event; - date preference (July 6th or 7th). As for the format, a standard option is a one-day workshop consisting of invited talks by leading experts and of shorter contributed talks, either directly invited by the organizers or selected among submissions. Deviations from this standard are also warmly welcome, including a shorter or a longer time span than a full day, or other elements of the schedule like open problem sessions, discussion panels, or working sessions. If you plan to have invited speakers, please specify their expected number and, if possible, tentative names. If you plan a call for papers or for contributed talks followed by a selection procedure, the submission date should be scheduled after ICALP 2020 and LICS 2020 notification, while the notification should take place considerably before the early registration deadline. In your submission please include details, in particular the time schedule, of the planned procedure of selecting papers and/or contributed talks. If you plan to have published proceedings of your workshop, please provide the name of the publisher. Please be advised that ICALP-LICS 2020 is not able to provide any financial support for publishing workshop proceedings. We expect the workshops to be financially independent. The expenses related to the participation of invited speakers, production of workshop materials, etc. should be covered from independent sources. On top of standard ICALP/LICS registration fee there will be a moderate registration fee for the workshops that will cover coffee breaks. This workshop fee will be waived for maximum two invited speakers for each workshop. Workshop selection committee: Frédéric Blanqui Naoki Kobayashi Yuqin Kong Michał Pilipczuk Zhilin Wu Lijun Zhang -- 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/d309b4ea-c12d-7d63-74b1-a2afe6df545f%40inria.fr. [-- Attachment #2: Type: text/html, Size: 5551 bytes --] <html> <head> <meta http-equiv="content-type" content="text/html; charset=UTF-8"> </head> <body bgcolor="#FFFFFF" text="#000000"> <br> <div class="moz-forward-container"> <div class="moz-forward-container"> <div class="moz-text-flowed" style="font-family: -moz-fixed; font-size: 12px;" lang="x-unicode">================================== <br> ICALP-LICS 2020 Call for Workshops <br> ================================== <br> <br> ICALP 2020 (<a class="moz-txt-link-freetext" href="http://econcs.pku.edu.cn/icalp2020/" moz-do-not-send="true">http://econcs.pku.edu.cn/icalp2020/</a>) and LICS 2020 (<a class="moz-txt-link-freetext" href="https://lics.siglog.org/lics20/" moz-do-not-send="true">https://lics.siglog.org/lics20/</a>) will take place in co-location from 8th till 12th of July 2020 in Beijing, China. The conferences will be preceded by two days of joint workshops, held on July 6th and 7th. We invite proposals of workshops affiliated with ICALP-LICS 2020 on all topics covered by ICALP and LICS, as well as other areas of theoretical computer science. <br> <br> Proposals should be submitted no later than <br> <br> *** November 30th, 2019 *** <br> <br> by sending an email to <a class="moz-txt-link-abbreviated" href="mailto:frederic.blanqui@inria.fr" moz-do-not-send="true">frederic.blanqui@inria.fr</a>. Due to limited space of the venue we might not be able to accommodate all the proposed workshops. You should expect notification on the acceptance of your proposal by mid December 2019. <br> <br> A workshop proposal submission should consist of: <br> <br> - workshop's name and URL (if already available) <br> <br> - workshop's organizers together with their email addresses and web pages; <br> <br> - short description of the area covered by the workshop and the motivation behind it; <br> <br> - expected number of participants (if available, please include the data of previous years); <br> <br> - planned format of the event; <br> <br> - date preference (July 6th or 7th). <br> <br> As for the format, a standard option is a one-day workshop consisting of invited talks by leading experts and of shorter contributed talks, either directly invited by the organizers or selected among submissions. Deviations from this standard are also warmly welcome, including a shorter or a longer time span than a full day, or other elements of the schedule like open problem sessions, discussion panels, or working sessions. <br> <br> If you plan to have invited speakers, please specify their expected number and, if possible, tentative names. If you plan a call for papers or for contributed talks followed by a selection procedure, the submission date should be scheduled after ICALP 2020 and LICS 2020 notification, while the notification should take place considerably before the early registration deadline. In your submission please include details, in particular the time schedule, of the planned procedure of selecting papers and/or contributed talks. If you plan to have published proceedings of your workshop, please provide the name of the publisher. Please be advised that ICALP-LICS 2020 is not able to provide any financial support for publishing workshop proceedings. <br> <br> We expect the workshops to be financially independent. The expenses related to the participation of invited speakers, production of workshop materials, etc. should be covered from independent sources. On top of standard ICALP/LICS registration fee there will be a moderate registration fee for the workshops that will cover coffee breaks. This workshop fee will be waived for maximum two invited speakers for each workshop. <br> <br> Workshop selection committee: <br> Frédéric Blanqui <br> Naoki Kobayashi <br> Yuqin Kong <br> Michał Pilipczuk <br> Zhilin Wu <br> Lijun Zhang <br> </div> </div> </div> </body> </html> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/d309b4ea-c12d-7d63-74b1-a2afe6df545f%40inria.fr?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/d309b4ea-c12d-7d63-74b1-a2afe6df545f%40inria.fr</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 2353 bytes --] Dear all, This is very sad news indeed. My memory of Erik is as a quiet but thoughtful and warm person, candid and principled, and vastly knowledgeable. Erik was my entry-point into the world of type theory, when, in 2016, he let me, then an impressionable masters student, into his cavernous setoid libraries, where I spent six happy months messing with E-categories---'"Erik"-categories'---and ECwAs, lost in the heady lure of checking coherences in a proof assistant. -Chaitanya. On Fri, Nov 15, 2019 at 11:15 PM Peter LeFanu Lumsdaine < p.l.lumsdaine@gmail.com> wrote: > Dear colleagues, > > Some very sad news — Erik Palmgren passed away unexpectedly this week at > his home in Stockholm, after a short period of bad health. > > Besides being insightful and influential in his own work, mostly on > constructive mathematics and related topics in logic, Erik was also a > generous and sensitive mentor to many students and younger colleagues, > first in Uppsala and then in Stockholm. He will be deeply missed. > > Personal website: http://staff.math.su.se/palmgren/ > > For any academic business regarding Erik, please contact either me < > p.l.lumsdaine@math.su.se> or Jonas Bergström <jonasb@math.su.se> (head of > the Stockholm University mathematics division). > > Sadly, > –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-k00GTNS4jm3vgvJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-k00GTNS4jm3vgvJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%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/CALwTfBf%3D80-ak%2Bgn%2BdDV3rsEoaSTMQPG9jH8_9EqQvYZpV%2B85Q%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3513 bytes --] <div dir="ltr"><p>Dear all,</p> <p>This is very sad news indeed.</p> <p>My memory of Erik is as a quiet but thoughtful and warm person, candid and principled, and vastly knowledgeable.<br> </p> <p>Erik was my entry-point into the world of type theory, when, in 2016, he let me, then an impressionable masters student, into his cavernous setoid libraries, where I spent six happy months messing with E-categories---'"Erik"-categories'---and ECwAs, lost in the heady lure of checking coherences in a proof assistant.</p> <p>-Chaitanya.</p></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Nov 15, 2019 at 11:15 PM Peter LeFanu Lumsdaine <<a href="mailto:p.l.lumsdaine@gmail.com">p.l.lumsdaine@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><div dir="ltr">Dear colleagues,<div><br></div><div><div>Some very sad news — Erik Palmgren passed away unexpectedly this week at his home in Stockholm, after a short period of bad health.</div><div><br></div><div>Besides being insightful and influential in his own work, mostly on constructive mathematics and related topics in logic, Erik was also a generous and sensitive mentor to many students and younger colleagues, first in Uppsala and then in Stockholm. He will be deeply missed.</div><div><br></div><div>Personal website: <a href="http://staff.math.su.se/palmgren/" target="_blank">http://staff.math.su.se/palmgren/</a><br></div><div><br></div><div>For any academic business regarding Erik, please contact either me <<a href="mailto:p.l.lumsdaine@math.su.se" target="_blank">p.l.lumsdaine@math.su.se</a>> or Jonas Bergström <<a href="mailto:jonasb@math.su.se" target="_blank">jonasb@math.su.se</a>> (head of the Stockholm University mathematics division).<br></div><div><br></div><div>Sadly,<br></div><div>–Peter.</div></div></div></div></div> <p></p> -- <br> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" target="_blank">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-k00GTNS4jm3vgvJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%40mail.gmail.com?utm_medium=email&utm_source=footer" target="_blank">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-k00GTNS4jm3vgvJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%40mail.gmail.com</a>.<br> </blockquote></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CALwTfBf%3D80-ak%2Bgn%2BdDV3rsEoaSTMQPG9jH8_9EqQvYZpV%2B85Q%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CALwTfBf%3D80-ak%2Bgn%2BdDV3rsEoaSTMQPG9jH8_9EqQvYZpV%2B85Q%40mail.gmail.com</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 2400 bytes --] Dear all, We are extending the submission deadline for the HoTT 2019 proceedings special issue of MSCS; the new deadline is *Friday 13 December*. Two notes for submitters: - If you already submitted for the original deadline but would like to use the extra time to revise your submission, let us know, and we will hold back from sending your submission out for refereeing for now. - There are problems with the MSCS LaTeX class file currently linked in the author instructions. Hopefully this should be fixed soon, but for now, don’t worry about putting submissions into the journal style — this can be done later after acceptance. Best wishes, –Peter and Dan. Original CfP: Submissions are now open for a special issue of Mathematical Structures in Computer Science on the proceedings of the HoTT 2019 conference, edited by Dan Licata and Peter LeFanu Lumsdaine. Papers on work presented at the HoTT19 conference are particularly encouraged, but the special issue is open to any work on homotopy type theory and related research areas. Specific topics include but are not limited to: homotopical and higher-categorical semantics of type theory; synthetic homotopy theory; applications of univalence and higher inductive types; cubical type theories and cubical models; formalization of mathematics and computer science in homotopy type theory / univalent foundations; and new type theories based on higher-dimensional ideas. To submit a paper, please follow the general MSCS submission procedure at https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science . When giving the submission details, select “Homotopy Type Theory 2019” for the field “Special Issue”. More information at: - https://www.cambridge.org/core/news/homotopy-type-theory - https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science - https://hott.github.io/HoTT-2019/ Best, Dan and 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-%3DyOcx5dLEuG0vC5eTQq7EXY88LYZrTQGEmMf2BSU6e5Q%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3436 bytes --] <div dir="ltr"><div dir="ltr"><div>Dear all,</div><div><br></div><div>We are extending the submission deadline for the HoTT 2019 proceedings special issue of MSCS; the new deadline is *Friday 13 December*.</div><div><br></div><div>Two notes for submitters:</div><div><br></div><div><div style="color:rgb(0,0,0)">- If you already submitted for the original deadline but would like to use the extra time to revise your submission, let us know, and we will hold back from sending your submission out for refereeing for now.</div><div style="color:rgb(0,0,0)"><br></div></div><div>- There are problems with the MSCS LaTeX class file currently linked in the author instructions. Hopefully this should be fixed soon, but for now, don’t worry about putting submissions into the journal style — this can be done later after acceptance.</div><div><br></div><div>Best wishes,</div><div>–Peter and Dan.</div><div><br></div><div>Original CfP:</div><div dir="ltr"><br></div><div dir="ltr">Submissions are now open for a special issue of Mathematical Structures in Computer Science on the proceedings of the HoTT 2019 conference, edited by Dan Licata and Peter LeFanu Lumsdaine.<br><br>Papers on work presented at the HoTT19 conference are particularly encouraged, but the special issue is open to any work on homotopy type theory and related research areas.<br><br>Specific topics include but are not limited to: homotopical and higher-categorical semantics of type theory; synthetic homotopy theory; applications of univalence and higher inductive types; cubical type theories and cubical models; formalization of mathematics and computer science in homotopy type theory / univalent foundations; and new type theories based on higher-dimensional ideas.<br><br>To submit a paper, please follow the general MSCS submission procedure at <a href="https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science" target="_blank">https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science</a> . When giving the submission details, select “Homotopy Type Theory 2019” for the field “Special Issue”.<div><br></div><div>More information at:</div><div>- <a href="https://www.cambridge.org/core/news/homotopy-type-theory" target="_blank">https://www.cambridge.org/core/news/homotopy-type-theory</a></div><div>- <a href="https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science" target="_blank">https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science</a><br>- <a href="https://hott.github.io/HoTT-2019/" target="_blank">https://hott.github.io/HoTT-2019/</a><br><br></div><div>Best,</div><div>Dan and Peter.</div></div></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-%3DyOcx5dLEuG0vC5eTQq7EXY88LYZrTQGEmMf2BSU6e5Q%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-%3DyOcx5dLEuG0vC5eTQq7EXY88LYZrTQGEmMf2BSU6e5Q%40mail.gmail.com</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 1121 bytes --] Dear colleagues, Some very sad news — Erik Palmgren passed away unexpectedly this week at his home in Stockholm, after a short period of bad health. Besides being insightful and influential in his own work, mostly on constructive mathematics and related topics in logic, Erik was also a generous and sensitive mentor to many students and younger colleagues, first in Uppsala and then in Stockholm. He will be deeply missed. Personal website: http://staff.math.su.se/palmgren/ For any academic business regarding Erik, please contact either me < p.l.lumsdaine@math.su.se> or Jonas Bergström <jonasb@math.su.se> (head of the Stockholm University mathematics division). Sadly, –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-k00GTNS4jm3vgvJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1799 bytes --] <div dir="ltr"><div dir="ltr"><div dir="ltr">Dear colleagues,<div><br></div><div><div>Some very sad news — Erik Palmgren passed away unexpectedly this week at his home in Stockholm, after a short period of bad health.</div><div><br></div><div>Besides being insightful and influential in his own work, mostly on constructive mathematics and related topics in logic, Erik was also a generous and sensitive mentor to many students and younger colleagues, first in Uppsala and then in Stockholm. He will be deeply missed.</div><div><br></div><div>Personal website: <a href="http://staff.math.su.se/palmgren/" target="_blank">http://staff.math.su.se/palmgren/</a><br></div><div><br></div><div>For any academic business regarding Erik, please contact either me <<a href="mailto:p.l.lumsdaine@math.su.se" target="_blank">p.l.lumsdaine@math.su.se</a>> or Jonas Bergström <<a href="mailto:jonasb@math.su.se" target="_blank">jonasb@math.su.se</a>> (head of the Stockholm University mathematics division).<br></div><div><br></div><div>Sadly,<br></div><div>–Peter.</div></div></div></div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-k00GTNS4jm3vgvJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-k00GTNS4jm3vgvJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%40mail.gmail.com</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 11416 bytes --] Hello HoTT list! I have recently been thinking about Whitehead products and how we can talk about them in homotopy type theory. I have always thought that their construction was slightly convoluted, and I failed to see why they were interesting operations to think about. Recently, Jacob Lurie gave a really nice talk about Lie algebras and homotopy theory: https://www.youtube.com/watch?v=LeaiPHAh0X0 I will give a quick and dirty summary of the start of his talk. If you don't care to hear it you can scroll past it to the section heading. The Whitehead product is a binary operation on homotopy groups of spheres. Explicitly, for a pointed space X this is a group homomorphism: Pi_{n + 1} (X) x Pi_{m + 1} (X) --> Pi_{n + m + 1} (X) Now at first glance this seems to be an ugly operation. The indexing, for example, doesn't quite line up, so it doesn't quite become what some people would consider to be a graded map. This is simply because this is the wrong way to look at it. What the Whitehead product really is is the following: Pi_n (loops X) x Pi_m (loops X) --> Pi_{n+m} (loops X) This is much better. But still the question arises, why do we care about such a map? To understand the picture, we take a few step backs and look at Lie theory. You don't need to know anything about Lie theory to understand this story however. Classically given a group G, we are often interested in the behavior of the commutator map: G x G --> G (g, h) |-> g h g^-1 h^-1 This map gives us a measure of how commutative our group operation is. Now often we have some extra structure on a group G, which lets us understand our commutator map better. Suppose G was also a smooth manifold in a compatible way with our group operation. We call such a group, a Lie group. Notably our group operation is now a smooth map, which means we can differentiate it as many times as we wish. It isn't too difficult to also show that our commutator map is also smooth. So using the tools at our disposal we can differentiate our commutator map (at the identity of G). Doing so we get the following bilinear map: TG x TG -> TG Which we will call our Lie bracket [-,-]. This bracket satisfies some extra identities which aren't so important for now: - Skew-symmetry [x, y] + [y, x] = 0 - Jacobi identity [x, [y, z]] + [y, [z, x]] + [z, [x, y]] = 0 Together an Abelian group with its Lie bracket operation satisfying the above identities is called a Lie algebra. As a quick example, consider the group SU(2) of unitary 2x2 matrices with determinant 1, or equivalently pairs of complex numbers (alpha, beta) such that |alpha|^2 + |beta|^2 = 1, or equivalently the group of unit quarternions. Now take my word for it, and note that the tangent space of SU(2) at the identity is essentially the vector space R^3. So the commutator operation we defined on SU(2) becomes a bilinear map R^3 x R^3 -> R^3. What is this map exactly? Well its just the cross product on R^3! Now it turns out in Lie theory, that no information was lost when differentiating this commutator map. By this I mean every Lie group has an associated Lie algebra and every Lie algebra has an associated Lie group. This correspondence let's you study these two worlds with the help of each other. We can develop the following heuristic: commutator maps in group-like objects can shed light on the structure of said object. How does this relate to homotopy theory? Well in homotopy theory, we have something that kind of looks like a group. The loop space of a pointed space X. If you are familiar with homotopy theory or homotopy type theory you will know that we have a concatenation map: loops X x loops X -> loops X Which takes a loop p and a loop q, and sends it to the loop pq. In classical homotopy theory loops are points in X parameterized by the interval. Concatenation is constructed by going twice as fast round p, then twice as fast round q, leaving you a loop pq. In homotopy type theory we can define the concatenation by path induction (see Ch2 of the HoTT book). Now we can also take inverses p^ of a path p in classical homotopy theory and HoTT. In classical homotopy theory you just go backwards along your paramterization. In HoTT you can define the inverse by path induction. With both you can show that inverse and identity laws kind of hold but with a catch: They only hold up to homotopy. When you look at homotopy classes of such loops when taking the fundamental group, this is fine because it ends up being associative "on the nose". In HoTT we define the fundamental group as the set-truncation of the loop space, which lets us show that any two "associativity proofs" are in fact the same. Observe that we can create a "commutator" map for loop spaces also: loops X x loops X --> loops X ( p , q ) |-> p q p^ q^ However as mentioned before, loop spaces aren't really groups, but groups up to homotopy (or H-groups). However when looking at the fundamental group of X, we see that our "commutator" becomes the actual commutator on the fundamental group. Now just as we did in Lie theory, we can exploit this "extra structure" that we have to study our "commutator" map. We do this by looking at the higher homotopy groups of our space, and see how it interacts with the commutator map. This is the story that Jacob Lurie told in his talk, which I was following up until he wrote the following: Pi_a (loops X) x Pi_b (loops X) --> Pi_{a + b} (loops X) and said that this was the Whitehead product. Now I didn't quite follow this step, and since I was watching the talk online, I couldn't put my hand up and ask a question. Since this wasn't really relevent to the pointed Jacob was trying to make, he didn't talk so much about it. Instead I devised my own explanation: What we really want to do is construct the following map: [Y, loops X] x [Z, loops X] --> [Y /\ Z , loops X] you can see if we plug in Y := S^a, Z := S^b we get [S^a, loops X] x [S^b, loops X] --> [S^a /\ S^b, loops X] Now a property of the smash product is that we have S^a /\ S^b being equivalent to S^(a+b) (which I will come back to since this isn't so obvious). And since higher homotopy groups are just the set of pointed maps from the spheres to a space, we can see that in classical homotopy theory and HoTT that we have a map: Pi_a (loops X) x Pi_b (loops X) --> Pi_{a+b} (loops X) Or in order words, we have as a special case, the Whitehead product. So the question becomes, how do we create this "generalized Whitehead product"? What we will see is that it is a pretty natural thing to consider. In fact it is just the composition of two maps: [Y, loops X] x [Z, loops X] -> [Y /\ Z, loops X /\ loops X] -> [Y /\ Z, loops X] Here by [-,-] I really mean the space of pointed maps, not the set as before. And all our arrows are also pointed. Mapping spaces are pointed spaces by taking the 'constant map at the basepoint' as the basepoint. Now the first map is just the bifunctoriality of the smash product. i.e. given two pointed maps Y -> loops X and Z -> loops X, we have a third pointed map Y /\ Z -> loops X /\ loops X. Furthermore, this construction of the pointed map is pointed itself hence sits as the first map in the above diagram. Now we are left to construct: [Y /\ Z, loops X /\ loops X] -> [Y /\ Z, loops X] Note that the functor [Y /\ Z, - ] can give this map if we give it a map loops X /\ loops X -> loops X. Now how do we construct a map loops X /\ loops X -> loops X? Well classically, the smash product is just a quotient, so we would use a function on the representatives of the equivalence classes and show that coming from the same class lands you in the same element. In HoTT we basically do something similar, the difference being that the smash product is a HIT. There are at least two equivalent definitions of the smash product in HoTT but we will ignore both of them and instead use an recursion principle you should be able to derive, no matter which definition you choose. This principle says: If you want to construct a map A /\ B -> C, then give me a map P : A x B -> C, such that we have the following: - pleft : forall a, P a pt = 1 - pright : forall b, P pt b = 1 - pleft pt = 1 - prigh pt = 1 Here 1 is the identity path or trivial loop. pt is just the base point of A or B. We are asking that our map essentially be pointed in each argument, and furthermore the proofs that they are pointed to be trivial. Now coming back to Whitehead, we see that to give a map: loops X /\ loops X -> loops X We need to give a map loops X x loops X -> loops X. So we just give the commutator map! It is an easy exercise to see that the commutator map satisfies the conditions we need for our recursion principle! So finally you can set-truncate this entire thing to get the whitehead product between given homotopy groups. This isn't the first time the Whitehead product has been defined in HoTT. Notably in his thesis, Guillaume Brunerie defined and used the Whitehead product, together with the James construction, to show that Pi_4(S^3) has a non-trivial generator of order n. (And is in fact generated by the bracket!) Guillaume uses joins of spheres and the 3x3 lemma which I think is far too complicated to describe what is in fact a very simple operation. The 3x3 lemma is a very non-trivial thing to prove. I mentioned earlier that S^n /\ S^m ~= S^(n+m) which isn't so trivial to show, but I wouldn't like to leave anybody hanging so I will give a quick proof here: When I write '=' I mean equivalence (which is a terrible abuse of notation). Start with the following three lemmas: Lemma 1. S^0 /\ X = X Lemma 2. S^1 /\ X = Susp X Lemma 3. X /\ (Y /\ Z) = (X /\ Y) /\ Z We want to show S^n /\ S^m = S^n+m, start by induction on n. For the base case we need to show that S^0 /\ S^m, apply lemma 1. Now our induction hypothesis is that S^n /\ S^m = S^n+m, and we wish to show S^n+1 /\ S^m = S^n+m+1. Since we define the spheres to be an iterated suspension, observe that: S^n+1 = Susp S^n = S^1 /\ S^n by lemma 2. Now using lemma 3, observe that S^n+1 /\ S^m = (S^1 /\ S^n) /\ S^m = S^1 /\ (S^n /\ S^ m), hence by lemma 2 and our induction hypothesis S^n+1 /\ S^m = Susp (S^n+m) = S^n+m+1, and we are done. I didn't really get a feel for the Whitehead product until Jacob mentioned that it was a commutator map in his talk. I thought that this would be a simpler and more enlightening construction than the ones I have come across. Whitehead products are important in homotopy theory because in some appropriate sense, every homotopy operation comes from Whitehead products and another simple operation. And as Guillaume showed, they can be used to construct non-trivial elements of higher homotopy groups. Hopefully this has been an interesting read. Please feel free to reply and ask questions. Happy thinking! Ali Caglayan -- 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/CAB17i%3DiL5O4-aQ-7YsPHOzo3MbnGHNgxXuYMW7ZPcxCWtQGAqg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 13064 bytes --] <div dir="ltr"><div class="gmail_quote"><div dir="ltr">Hello HoTT list!<br><br>I have recently been thinking about Whitehead products and how we can talk about<br>them in homotopy type theory. I have always thought that their construction was<br>slightly convoluted, and I failed to see why they were interesting operations to<br>think about.<br><br>Recently, Jacob Lurie gave a really nice talk about Lie algebras and homotopy<br>theory:<br><br><a href="https://www.youtube.com/watch?v=LeaiPHAh0X0" target="_blank">https://www.youtube.com/watch?v=LeaiPHAh0X0</a><br><br>I will give a quick and dirty summary of the start of his talk. If you don't care to</div><div dir="ltr">hear it you can scroll past it to the section heading.<br></div><div dir="ltr"><br></div><div dir="ltr">The Whitehead product is a binary operation on homotopy groups of spheres.<br>Explicitly, for a pointed space X this is a group homomorphism:<br><br> Pi_{n + 1} (X) x Pi_{m + 1} (X) --> Pi_{n + m + 1} (X)<br><br>Now at first glance this seems to be an ugly operation. The indexing, for<br>example, doesn't quite line up, so it doesn't quite become what some people<br>would consider to be a graded map.<br><br>This is simply because this is the wrong way to look at it. What the Whitehead<br>product really is is the following:<br><br> Pi_n (loops X) x Pi_m (loops X) --> Pi_{n+m} (loops X)<br><br>This is much better.<br>But still the question arises, why do we care about such a map?<br><br>To understand the picture, we take a few step backs and look at Lie theory.<br>You don't need to know anything about Lie theory to understand this story<br>however.<br><br>Classically given a group G, we are often interested in the behavior of the<br>commutator map:<br><br> G x G --> G<br> (g, h) |-> g h g^-1 h^-1<br><br>This map gives us a measure of how commutative our group operation is.<br><br>Now often we have some extra structure on a group G, which lets us understand<br>our commutator map better.<br><br>Suppose G was also a smooth manifold in a compatible way with our group<br>operation. We call such a group, a Lie group. Notably our group operation is now<br>a smooth map, which means we can differentiate it as many times as we wish. It<br>isn't too difficult to also show that our commutator map is also smooth.<br><br>So using the tools at our disposal we can differentiate our commutator map<br>(at the identity of G). Doing so we get the following bilinear map:<br><br> TG x TG -> TG<br><br>Which we will call our Lie bracket [-,-]. This bracket satisfies some extra<br>identities which aren't so important for now:<br><br> - Skew-symmetry [x, y] + [y, x] = 0<br> - Jacobi identity [x, [y, z]] + [y, [z, x]] + [z, [x, y]] = 0 <br><br>Together an Abelian group with its Lie bracket operation satisfying the above<br>identities is called a Lie algebra.<br><br>As a quick example, consider the group SU(2) of unitary 2x2 matrices with<br>determinant 1, or equivalently pairs of complex numbers (alpha, beta) such that<br>|alpha|^2 + |beta|^2 = 1, or equivalently the group of unit quarternions.<br><br>Now take my word for it, and note that the tangent space of SU(2) at the<br>identity is essentially the vector space R^3. So the commutator operation we<br>defined on SU(2) becomes a bilinear map R^3 x R^3 -> R^3.<br><br>What is this map exactly? Well its just the cross product on R^3!<br><br>Now it turns out in Lie theory, that no information was lost when<br>differentiating this commutator map. By this I mean every Lie group has an<br>associated Lie algebra and every Lie algebra has an associated Lie group. This<br>correspondence let's you study these two worlds with the help of each other.<br><br>We can develop the following heuristic: commutator maps in group-like objects<br>can shed light on the structure of said object.<br><br><br><font size="4">How does this relate to homotopy theory?</font><br><br>Well in homotopy theory, we have something that kind of looks like a group. The<br>loop space of a pointed space X. If you are familiar with homotopy theory or<br>homotopy type theory you will know that we have a concatenation map:<br><br> loops X x loops X -> loops X<br><br>Which takes a loop p and a loop q, and sends it to the loop pq. In classical<br>homotopy theory loops are points in X parameterized by the interval.<br>Concatenation is constructed by going twice as fast round p, then twice as fast<br>round q, leaving you a loop pq. In homotopy type theory we can define the<br>concatenation by path induction (see Ch2 of the HoTT book).<br><br>Now we can also take inverses p^ of a path p in classical homotopy theory and<br>HoTT. In classical homotopy theory you just go backwards along your<br>paramterization. In HoTT you can define the inverse by path induction. With both<br>you can show that inverse and identity laws kind of hold but with a catch:<br> <br> They only hold up to homotopy.<br><br>When you look at homotopy classes of such loops when taking the fundamental<br>group, this is fine because it ends up being associative "on the nose". In HoTT<br>we define the fundamental group as the set-truncation of the loop space, which<br>lets us show that any two "associativity proofs" are in fact the same.<br><br>Observe that we can create a "commutator" map for loop spaces also:<br><br> loops X x loops X --> loops X<br> ( p , q ) |-> p q p^ q^<br> <br>However as mentioned before, loop spaces aren't really groups, but groups up to<br>homotopy (or H-groups). However when looking at the fundamental group of X, we<br>see that our "commutator" becomes the actual commutator on the fundamental group.<br><br>Now just as we did in Lie theory, we can exploit this "extra structure" that we<br>have to study our "commutator" map. We do this by looking at the higher homotopy<br>groups of our space, and see how it interacts with the commutator map.<br><br>This is the story that Jacob Lurie told in his talk, which I was following up<br>until he wrote the following:<br><br> Pi_a (loops X) x Pi_b (loops X) --> Pi_{a + b} (loops X)<br><br>and said that this was the Whitehead product. Now I didn't quite follow this<br>step, and since I was watching the talk online, I couldn't put my hand up and<br>ask a question. Since this wasn't really relevent to the pointed Jacob was<br>trying to make, he didn't talk so much about it.<br><br>Instead I devised my own explanation:<br><br>What we really want to do is construct the following map:<br><br> [Y, loops X] x [Z, loops X] --> [Y /\ Z , loops X]<br><br>you can see if we plug in Y := S^a, Z := S^b we get<br><br> [S^a, loops X] x [S^b, loops X] --> [S^a /\ S^b, loops X]<br><br>Now a property of the smash product is that we have S^a /\ S^b being equivalent<br>to S^(a+b) (which I will come back to since this isn't so obvious). And since<br>higher homotopy groups are just the set of pointed maps from the spheres to a<br>space, we can see that in classical homotopy theory and HoTT that we have a map:<br><br> Pi_a (loops X) x Pi_b (loops X) --> Pi_{a+b} (loops X)<br><br>Or in order words, we have as a special case, the Whitehead product. So the<br>question becomes, how do we create this "generalized Whitehead product"?<br><br>What we will see is that it is a pretty natural thing to consider. In fact it is<br>just the composition of two maps:<br><br>[Y, loops X] x [Z, loops X] -> [Y /\ Z, loops X /\ loops X] -> [Y /\ Z, loops X]<br><br>Here by [-,-] I really mean the space of pointed maps, not the set as before.<br>And all our arrows are also pointed. Mapping spaces are pointed spaces by taking<br>the 'constant map at the basepoint' as the basepoint.<br><br>Now the first map is just the bifunctoriality of the smash product. i.e. given<br>two pointed maps Y -> loops X and Z -> loops X, we have a third pointed map<br>Y /\ Z -> loops X /\ loops X. Furthermore, this construction of the pointed map<br>is pointed itself hence sits as the first map in the above diagram.<br><br>Now we are left to construct:<br><br> [Y /\ Z, loops X /\ loops X] -> [Y /\ Z, loops X]<br><br>Note that the functor [Y /\ Z, - ] can give this map if we give it a map<br> <br> loops X /\ loops X -> loops X.<br><br>Now how do we construct a map loops X /\ loops X -> loops X? Well classically,<br>the smash product is just a quotient, so we would use a function on the<br>representatives of the equivalence classes and show that coming from the same<br>class lands you in the same element.<br><br>In HoTT we basically do something similar, the difference being that the smash<br>product is a HIT. There are at least two equivalent definitions of the smash<br>product in HoTT but we will ignore both of them and instead use an recursion<br>principle you should be able to derive, no matter which definition you choose.<br><br>This principle says:<br><br>If you want to construct a map A /\ B -> C, then give me a map P : A x B -> C,<br>such that we have the following:<br> - pleft : forall a, P a pt = 1<br> - pright : forall b, P pt b = 1<br> - pleft pt = 1<br> - prigh pt = 1<br><br>Here 1 is the identity path or trivial loop. pt is just the base point of A or<br>B. We are asking that our map essentially be pointed in each argument, and<br>furthermore the proofs that they are pointed to be trivial.<br><br>Now coming back to Whitehead, we see that to give a map:<br><br> loops X /\ loops X -> loops X<br><br>We need to give a map<br><br> loops X x loops X -> loops X.<br><br>So we just give the commutator map!<br><br>It is an easy exercise to see that the commutator map satisfies the conditions<br>we need for our recursion principle!<br><br>So finally you can set-truncate this entire thing to get the whitehead product<br>between given homotopy groups.<br><br>This isn't the first time the Whitehead product has been defined in HoTT.<br>Notably in his thesis, Guillaume Brunerie defined and used the Whitehead<br>product, together with the James construction, to show that Pi_4(S^3) has a<br>non-trivial generator of order n. (And is in fact generated by the bracket!)<br><br>Guillaume uses joins of spheres and the 3x3 lemma which I think is far too<br>complicated to describe what is in fact a very simple operation. The 3x3 lemma<br>is a very non-trivial thing to prove.<br><br>I mentioned earlier that S^n /\ S^m ~= S^(n+m) which isn't so trivial to show,<br>but I wouldn't like to leave anybody hanging so I will give a quick proof here:<br><br>When I write '=' I mean equivalence (which is a terrible abuse of notation).<br><br>Start with the following three lemmas:<br><br>Lemma 1. S^0 /\ X = X<br>Lemma 2. S^1 /\ X = Susp X<br>Lemma 3. X /\ (Y /\ Z) = (X /\ Y) /\ Z<br><br>We want to show S^n /\ S^m = S^n+m, start by induction on n. For the base case<br>we need to show that S^0 /\ S^m, apply lemma 1. Now our induction hypothesis is<br>that S^n /\ S^m = S^n+m, and we wish to show S^n+1 /\ S^m = S^n+m+1. Since we<br>define the spheres to be an iterated suspension, observe that:<br>S^n+1 = Susp S^n = S^1 /\ S^n by lemma 2. Now using lemma 3, observe that<br>S^n+1 /\ S^m = (S^1 /\ S^n) /\ S^m = S^1 /\ (S^n /\ S^ m), hence by lemma 2<br>and our induction hypothesis S^n+1 /\ S^m = Susp (S^n+m) = S^n+m+1, and we are<br>done.<br><br>I didn't really get a feel for the Whitehead product until Jacob mentioned that<br>it was a commutator map in his talk. I thought that this would be a simpler and<br>more enlightening construction than the ones I have come across.<br><br>Whitehead products are important in homotopy theory because in some appropriate<br>sense, every homotopy operation comes from Whitehead products and another<br>simple operation. And as Guillaume showed, they can be used to construct<br>non-trivial elements of higher homotopy groups.<br><br>Hopefully this has been an interesting read. Please feel free to reply and ask<br>questions. <br><br>Happy thinking!<br><br>Ali Caglayan<br></div> </div></div> <p></p> -- <br /> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br /> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br /> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DiL5O4-aQ-7YsPHOzo3MbnGHNgxXuYMW7ZPcxCWtQGAqg%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DiL5O4-aQ-7YsPHOzo3MbnGHNgxXuYMW7ZPcxCWtQGAqg%40mail.gmail.com</a>.<br />

After several requests, we extend the deadline to 24 November 2019, and we welcome new submissions, which missed the previous abstract deadline. Open call for papers Post-proceedings of the 25th International Conference on Types for Proofs and Programs TYPES 2019 TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2019 was held 11-14 June in Oslo, Norway. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings (http://www.dagstuhl.de/en/publications/lipics). Submission to this post-proceedings volume is open to everyone, also to those who did not participate in the conference. We welcome high-quality descriptions of original work, as well as position papers, overview papers, and system descriptions. Submissions should be written in English, not overlapping with published or simultaneously submitted work to a journal or a conference with archival proceedings. The scope of the post-proceedings is the same as the scope of the conference: the theory and practice of type theory. In particular, we welcome submissions on the following topics: * Foundations of type theory and constructive mathematics; * Homotopy type theory and univalent mathematics; * Applications of type theory; * Dependently typed programming; * Industrial uses of type theory technology; * Meta-theoretic studies of type systems; * Proof assistants and proof technology; * Automation in computer-assisted reasoning; * Links between type theory and functional programming; * Formalizing mathematics using type theory. IMPORTANT DATES * Paper submission: 24 November 2019 * Author notification: 25 March 2020 DETAILS * Papers have to be formatted with LIPIcs style (currently lipics-v2019.cls) and adhere to the style requirements of LIPIcs: http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/ * The upper limit for the length of submissions is 20 pages * Papers have to be submitted in pdf through EasyChair: https://easychair.org/conferences/?conf=types2019postproc * Authors have the option to attach to their submission a zip or tgz file containing code (formalized proofs or programs), but reviewers are not obliged to take the attachments into account and they will not be published. * In case of questions, e.g. on the page limit, contact one of the editors. EDITORS Marc Bezem, Marc.Bezem@uib.no, University of Bergen, Norway Assia Mahboubi, assia.mahboubi@inria.fr, Inria -- Vrije Universiteit Amsterdam -- 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/1b5ff232-a710-36c0-b891-733c84902a32%40inria.fr.