Please distribute to undergraduate and master's students and appropriate counsellors and supervisors. Note that we have a large group of faculty, postdocs and graduate students with interests involving homotopy type theory. The February 1st deadline is very close, so apply soon, but also note that applications will continue to be reviewed past the deadline as space permits. Graduate Student Positions Department of Mathematics University of Western Ontario London, Ontario, Canada The Department of Mathematics at the University of Western Ontario solicits applications for its MSc and PhD programs. We have up to 20 fully funded positions available, and applicants from any country are welcome. Our faculty members supervise research in a variety of areas: http://www.math.uwo.ca/graduate/supervisors.html The Department of Mathematics is part of the School of Mathematical Sciences: http://uwo.ca/smss/ More information about our program, including the application procedure, is available at http://www.math.uwo.ca/graduate/ Students normally start in September, in which case applications should be complete (including letters of reference and supplementary material) by February 1. Applications received after this deadline will be reviewed as space permits. Early applications are welcome, and we encourage applicants to apply for external scholarships they are eligible for. Please contact math-grad-program@uwo.ca with any questions you may have. -- 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/CAEXhy3OWmW9OGOXw2THnrh-n1%3D5FXAUJ14oq_f7jdCoqssLPHQ%40mail.gmail.com.

Dear all, The Homotopy Type Theory Electronic Seminar Talks (HoTTEST) are returning in Winter 2020. The speakers are: January 23: Simon Henry February 6: Niels van der Weide February 20: Karol Szumiło March 19: Jon Sterling April 2: Denis-Charles Cisinski April 16: Matthew Weaver The seminar is back to its usual time of alternating Thursdays at 11:30 Eastern. For updates and instructions how to attend, please see https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html The seminar is open to everyone, but some prior familiarity with HoTT will be assumed. Best wishes, Chris Kapulkin for the organizers -- 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/CAEXhy3PLLqMvaFZnOFFLFk2QF681KuDMC%3DMLd32kHg%2BwAqgruA%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 1442 bytes --] Dear friends, This summer the 8th European Congress of Mathematics (https://www.8ecm.si) is taking place in Slovenia between July 5-11, 2020. There is a possibility to have a two-day mini-symposium on homotopy type theory, univalent foundations, higher category theory, formalization, and related topics. The ECM is a large meeting, so such a mini-symposium will likely be attended by people from outside the community. This, I think, will be a very good outreach opportunity for our field. The congress requires at least 20 presentations in a two-day mini-symposium, where I should add that participants can only register for the entire congress. Please see the website for the fees. If you are interested in speaking at the mini-symposium, could you please provide me by FRIDAY JANUARY 24TH with - your name, - your affiliation, - a tentative title or the topic of something you might want to talk about at this symposium. Abstracts are not required at this point. I hope to hear from you. Best wishes, Egbert Rijke -- 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/CAGqv1OBBC-6N3Ho4mK8Rb7YPMAh%2B%3DAUSSDPBO4M7mMz0LoaJpQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4122 bytes --] <div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><p style="margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">Dear friends,</font></p> <p style="margin:0px;font-stretch:normal;line-height:normal;min-height:14px"><font face="arial, sans-serif"><br></font></p> <p style="margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">This summer the 8th European Congress of Mathematics (<a href="https://www.8ecm.si/"><span style="color:rgb(220,161,13)">https://www.8ecm.si</span></a>) is taking place in Slovenia between July 5-11, 2020. There is a possibility to have a two-day mini-symposium on homotopy type theory, univalent foundations, higher category theory, formalization, and related topics. The ECM is a large meeting, so such a mini-symposium will likely be attended by people from outside the community. This, I think, will be a very good outreach opportunity for our field.</font></p><p style="margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif"><br></font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">The congress requires at least 20 presentations in a two-day mini-symposium, where I should add that participants can only register for the entire congress. Please see the website for the fees.</font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif"><br></font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">If you are interested in speaking at the mini-symposium, could you please provide me by FRIDAY JANUARY 24TH with </font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">- your name,</font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">- your affiliation,</font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">- a tentative title or the topic of something you might want to talk about at this symposium.</font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">Abstracts are not required at this point.</font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif"><br></font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">I hope to hear from you.</font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif"><br></font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">Best wishes,</font></p><p style="color:rgb(0,0,0);margin:0px;font-stretch:normal;line-height:normal"><font face="arial, sans-serif">Egbert Rijke</font></p> <p style="margin:0px;font-stretch:normal;line-height:normal;min-height:14px"><font face="arial, sans-serif"><br></font></p><p style="margin:0px;font-stretch:normal;line-height:normal;min-height:14px"><br></p> <p style="margin:0px;font-stretch:normal;font-size:12px;line-height:normal;font-family:"Helvetica Neue";min-height:14px"><br></p> </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/CAGqv1OBBC-6N3Ho4mK8Rb7YPMAh%2B%3DAUSSDPBO4M7mMz0LoaJpQ%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1OBBC-6N3Ho4mK8Rb7YPMAh%2B%3DAUSSDPBO4M7mMz0LoaJpQ%40mail.gmail.com</a>.<br />

======== CALL FOR PAPERS SEVENTH SYMPOSIUM ON COMPOSITIONAL STRUCTURES (SYCO 7) Tallinn University of Technology, Estonia 30-31 March 2020 http://events.cs.bham.ac.uk/syco/7/ ======== 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, Chapman University, and University of Leicester. 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. 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. IMPORTANT DATES ======== All deadlines are 23:59 Anywhere on Earth. Submission deadline: Monday 10 February 2020 Author notification: Monday 17 February 2020 Symposium dates: Monday 30 and Tuesday 31 March 2020 SUBMISSION INSTRUCTIONS ======== Submission are by EasyChair, via the SYCO 7 submission page: https://easychair.org/conferences/?conf=syco7 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. 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. Deferred submissions can be re-submitted to any future SYCO meeting, where they will not need peer review, and where they will be prioritised for inclusion in the programme. Meetings will be held sufficiently frequently to avoid a backlog of deferred papers. If you have a submission which was deferred from a previous SYCO meeting, it will not automatically be considered for SYCO 7; you still need to submit it again through EasyChair. When submitting, append the words "DEFERRED FROM SYCO X" to the title of your paper, replacing "X" with the appropriate meeting number. There is no need to attach any documents. PROGRAMME COMMITTEE ======== Christoph Dorn, University of Oxford Ross Duncan, University of Strathclyde Brendan Fong, MIT Amar Hadzihasanovic, IRIF, Université de Paris (PC chair) Chris Heunen, University of Edinburgh Alex Kavvos, Aarhus University Marie Kerjean, INRIA Bretagne Atlantique, Équipe Gallinette Martha Lewis, ILLC, University of Amsterdam Samuel Mimram, École Polytechnique Koko Muroya, RIMS, Kyoto University Jovana Obradović, Charles University in Prague Simona Paoli, University of Leicester Mehrnoosh Sadrzadeh, University College London Pawel Sobocinski, Tallinn University of Technology Christina Vasilakopoulou, University of Patras Jamie Vicary, University of Birmingham and University of Oxford Maaike Zwart, University of Oxford -- Amar Hadzihasanovic IRIF, Université de Paris http://www.irif.fr/~ahadziha/ -- 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/CAJb9em10pvtuk%2BnmjSQcX3G-TiPYSLXhuDCs6%3DWHm8A7zkHY9A%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 3553 bytes --] Thanks to everyone who replied! Just for the reference since Christian's email went only to me: there is a remark in the paper that states it is possible to make the theory extensional, so it appears 2LTT is exactly the type theory I was looking for. Best, Kristina On 1/7/2020 5:23 PM, Christian Sattler wrote: > See axiom (A5) in Section 2.4: > > (A5) We can ask that the outer level validates the equality > reflection rule, i.e. forms a model of extensional type theory. > This is the case in all the example models we are interested in. > > > Equality reflection is supported in presheaf models, which justify > conservativity over HoTT. The main problem with equality reflection is > syntactical, in that we don't have good proof assistant support for it... > > On Tue, 7 Jan 2020 at 23:11, Kristina Sojakova > <sojakova.kristina@gmail.com <mailto:sojakova.kristina@gmail.com>> wrote: > > Hello Rafael, > > Thank you for the reference. I browsed the paper; it seems to me that > the theory does not appear to support identity reflection. I am > looking > for a truly extensional form of equality (in addition to the usual > one), > where equal terms are syntactically identified. > > Kristina > > On 1/7/2020 5:03 PM, Rafaël Bocquet wrote: > > Hello, > > > > I think that the paper "Two-Level Type Theory and Applications" > > (https://arxiv.org/abs/1705.03307), whose last version has been > > submitted on arXiv last month, answers these questions. One of the > > intended models of 2LTT is the presheaf category Ĉ over any > model C of > > HoTT, and this presheaf model is conservative over C, essentially > > because the Yoneda embedding is fully faithful. This means that > we can > > always work in 2LTT instead of HoTT. > > > > Rafaël > > > > On 1/7/20 8:59 PM, Kristina Sojakova wrote: > >> Dear all, > >> > >> I have been increasingly running into situations where I wished > I had > >> an extensional equality type with a reflection rule in HoTT, in > >> addition to the intensional one to which univalence pertains. I > know > >> that type systems with two equalities have been studied in the > HoTT > >> community (e.g., VV's HTS), but last time I discussed this with > >> people it seemed the situation was not yet well-understood. So my > >> question is, what exactly goes wrong if we endow HoTT with an > >> extensional type? > >> > >> Thank you, > >> > >> Kristina > >> > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/60639a49-a1c6-0cfd-0bdf-65ad45b14e24%40gmail.com. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/f840404d-7427-0156-2f9a-50bfa865ea0d%40gmail.com. [-- Attachment #2: Type: text/html, Size: 5999 bytes --] <html> <head> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> </head> <body> <p>Thanks to everyone who replied! <br> </p> <p>Just for the reference since Christian's email went only to me: there is a remark in the paper that states it is possible to make the theory extensional, so it appears 2LTT is exactly the type theory I was looking for.</p> <p>Best,</p> <p>Kristina<br> </p> <div class="moz-cite-prefix">On 1/7/2020 5:23 PM, Christian Sattler wrote:<br> </div> <blockquote type="cite" cite="mid:CALCpNBoWKXbQgdJ2Pqq_G7J_0D48OVGUeQoBnOfDHzC__GWkHA@mail.gmail.com"> <meta http-equiv="content-type" content="text/html; charset=UTF-8"> <div dir="ltr">See axiom (A5) in Section 2.4: <div><br> <blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">(A5) We can ask that the outer level validates the equality reflection rule, i.e. forms a model of extensional type theory. This is the case in all the example models we are interested in.</blockquote> <div><br> </div> <div>Equality reflection is supported in presheaf models, which justify conservativity over HoTT. The main problem with equality reflection is syntactical, in that we don't have good proof assistant support for it...</div> </div> </div> <br> <div class="gmail_quote"> <div dir="ltr" class="gmail_attr">On Tue, 7 Jan 2020 at 23:11, Kristina Sojakova <<a href="mailto:sojakova.kristina@gmail.com" moz-do-not-send="true">sojakova.kristina@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">Hello Rafael,<br> <br> Thank you for the reference. I browsed the paper; it seems to me that <br> the theory does not appear to support identity reflection. I am looking <br> for a truly extensional form of equality (in addition to the usual one), <br> where equal terms are syntactically identified.<br> <br> Kristina<br> <br> On 1/7/2020 5:03 PM, Rafaël Bocquet wrote:<br> > Hello,<br> ><br> > I think that the paper "Two-Level Type Theory and Applications" <br> > (<a href="https://arxiv.org/abs/1705.03307" rel="noreferrer" target="_blank" moz-do-not-send="true">https://arxiv.org/abs/1705.03307</a>), whose last version has been <br> > submitted on arXiv last month, answers these questions. One of the <br> > intended models of 2LTT is the presheaf category Ĉ over any model C of <br> > HoTT, and this presheaf model is conservative over C, essentially <br> > because the Yoneda embedding is fully faithful. This means that we can <br> > always work in 2LTT instead of HoTT.<br> ><br> > Rafaël<br> ><br> > On 1/7/20 8:59 PM, Kristina Sojakova wrote:<br> >> Dear all,<br> >><br> >> I have been increasingly running into situations where I wished I had <br> >> an extensional equality type with a reflection rule in HoTT, in <br> >> addition to the intensional one to which univalence pertains. I know <br> >> that type systems with two equalities have been studied in the HoTT <br> >> community (e.g., VV's HTS), but last time I discussed this with <br> >> people it seemed the situation was not yet well-understood. So my <br> >> question is, what exactly goes wrong if we endow HoTT with an <br> >> extensional type?<br> >><br> >> Thank you,<br> >><br> >> Kristina<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" moz-do-not-send="true">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/60639a49-a1c6-0cfd-0bdf-65ad45b14e24%40gmail.com" rel="noreferrer" target="_blank" moz-do-not-send="true">https://groups.google.com/d/msgid/HomotopyTypeTheory/60639a49-a1c6-0cfd-0bdf-65ad45b14e24%40gmail.com</a>.<br> </blockquote> </div> </blockquote> </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/f840404d-7427-0156-2f9a-50bfa865ea0d%40gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/f840404d-7427-0156-2f9a-50bfa865ea0d%40gmail.com</a>.<br />

The intended presheaf model supports equality reflection. Martin Hofmann's conservativity theorem also implies that most type theories with UIP can conservatively be extended with equality reflection. On 1/7/20 11:11 PM, Kristina Sojakova wrote: > Hello Rafael, > > Thank you for the reference. I browsed the paper; it seems to me that > the theory does not appear to support identity reflection. I am > looking for a truly extensional form of equality (in addition to the > usual one), where equal terms are syntactically identified. > > Kristina > > On 1/7/2020 5:03 PM, Rafaël Bocquet wrote: >> Hello, >> >> I think that the paper "Two-Level Type Theory and Applications" >> (https://arxiv.org/abs/1705.03307), whose last version has been >> submitted on arXiv last month, answers these questions. One of the >> intended models of 2LTT is the presheaf category Ĉ over any model C >> of HoTT, and this presheaf model is conservative over C, essentially >> because the Yoneda embedding is fully faithful. This means that we >> can always work in 2LTT instead of HoTT. >> >> Rafaël >> >> On 1/7/20 8:59 PM, Kristina Sojakova wrote: >>> Dear all, >>> >>> I have been increasingly running into situations where I wished I >>> had an extensional equality type with a reflection rule in HoTT, in >>> addition to the intensional one to which univalence pertains. I know >>> that type systems with two equalities have been studied in the HoTT >>> community (e.g., VV's HTS), but last time I discussed this with >>> people it seemed the situation was not yet well-understood. So my >>> question is, what exactly goes wrong if we endow HoTT with an >>> extensional type? >>> >>> Thank you, >>> >>> Kristina >>> > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/563bb6a5-7603-c59a-5943-6f925e56b2b4%40ens.fr.

Hello Rafael, Thank you for the reference. I browsed the paper; it seems to me that the theory does not appear to support identity reflection. I am looking for a truly extensional form of equality (in addition to the usual one), where equal terms are syntactically identified. Kristina On 1/7/2020 5:03 PM, Rafaël Bocquet wrote: > Hello, > > I think that the paper "Two-Level Type Theory and Applications" > (https://arxiv.org/abs/1705.03307), whose last version has been > submitted on arXiv last month, answers these questions. One of the > intended models of 2LTT is the presheaf category Ĉ over any model C of > HoTT, and this presheaf model is conservative over C, essentially > because the Yoneda embedding is fully faithful. This means that we can > always work in 2LTT instead of HoTT. > > Rafaël > > On 1/7/20 8:59 PM, Kristina Sojakova wrote: >> Dear all, >> >> I have been increasingly running into situations where I wished I had >> an extensional equality type with a reflection rule in HoTT, in >> addition to the intensional one to which univalence pertains. I know >> that type systems with two equalities have been studied in the HoTT >> community (e.g., VV's HTS), but last time I discussed this with >> people it seemed the situation was not yet well-understood. So my >> question is, what exactly goes wrong if we endow HoTT with an >> extensional type? >> >> Thank you, >> >> Kristina >> -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/60639a49-a1c6-0cfd-0bdf-65ad45b14e24%40gmail.com.

Hello, I think that the paper "Two-Level Type Theory and Applications" (https://arxiv.org/abs/1705.03307), whose last version has been submitted on arXiv last month, answers these questions. One of the intended models of 2LTT is the presheaf category Ĉ over any model C of HoTT, and this presheaf model is conservative over C, essentially because the Yoneda embedding is fully faithful. This means that we can always work in 2LTT instead of HoTT. Rafaël On 1/7/20 8:59 PM, Kristina Sojakova wrote: > Dear all, > > I have been increasingly running into situations where I wished I had > an extensional equality type with a reflection rule in HoTT, in > addition to the intensional one to which univalence pertains. I know > that type systems with two equalities have been studied in the HoTT > community (e.g., VV's HTS), but last time I discussed this with people > it seemed the situation was not yet well-understood. So my question > is, what exactly goes wrong if we endow HoTT with an extensional type? > > Thank you, > > Kristina > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/7d1235e5-76ac-2a7d-9317-21d30f6973ad%40ens.fr.

Dear all, I have been increasingly running into situations where I wished I had an extensional equality type with a reflection rule in HoTT, in addition to the intensional one to which univalence pertains. I know that type systems with two equalities have been studied in the HoTT community (e.g., VV's HTS), but last time I discussed this with people it seemed the situation was not yet well-understood. So my question is, what exactly goes wrong if we endow HoTT with an extensional type? Thank you, Kristina -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8de08372-b17d-c153-73ad-4cd8b6c49758%40gmail.com.

We have a new paper on the arxiv. Comments, suggestions and questions are very welcome. Synthetic topology in Homotopy Type Theory for probabilistic programming Martin E. Bidlingmaier, Florian Faissole, Bas Spitters The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial σ-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies we define valuations and lower integrals on sets, and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed. -- 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/CAOoPQuR4ttw71bPEA%2BxtXZ__Q5kKFGRqgJVgTA%3D2PmLc5%3Dd5Lw%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 2776 bytes --] > On Dec 22, 2019, at 1:05 AM, Justin Scarfy <pujustinyang@gmail.com <mailto:pujustinyang@gmail.com>> wrote: > > > > On Saturday, December 21, 2019 at 7:06:06 AM UTC-8, Justin Scarfy wrote: > I am interested in this [these] positions- I am a mathematician in Vancouver, Canada, but I never graduated from the undergrad degree as UBC wants me to follow their rules and do two more none-math courses, all i do is math/ programming [for 20+ hours a day] for the past 10 years > > On Tuesday, December 17, 2019 at 4:00:59 AM UTC-8, Thorsten Altenkirch wrote: > We are looking for students (in the moment only international > I am Canadian > - UK/ EU will be advertised later. > > Prospective students interested in Homotopy Type Theory and related subjects are especially ancouraged to apply. > > > Please share! > > Thorsten > > > http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt <http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt> > https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918 <https://www.nottingham.ac.uk/jobs/currentvacancies/%E2%80%A6/SCI1918> > https://www.nottingham.ac.uk/research/groups/fp-lab/ <https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY> > > 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 <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com <https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%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/5CB8B1AE-98BA-4B4C-8592-C7850892FFBB%40gmail.com. [-- Attachment #2: Type: text/html, Size: 7164 bytes --] <html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Dec 22, 2019, at 1:05 AM, Justin Scarfy <<a href="mailto:pujustinyang@gmail.com" class="">pujustinyang@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><br class=""><br class="">On Saturday, December 21, 2019 at 7:06:06 AM UTC-8, Justin Scarfy wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir="ltr" class="">I am interested in this [these] positions- I am a mathematician in Vancouver, Canada, but I never graduated from the undergrad degree as UBC wants me to follow their rules and do two more none-math courses, all i do is math/ programming [for 20+ hours a day] for the past 10 years<br class=""><br class="">On Tuesday, December 17, 2019 at 4:00:59 AM UTC-8, Thorsten Altenkirch wrote:<blockquote class="gmail_quote" style="margin:0;margin-left:0.8ex;border-left:1px #ccc solid;padding-left:1ex"> <div lang="EN-GB" link="#0563C1" vlink="#954F72" class=""> <div class=""><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class="">We are looking for students (in the moment only international</span></p></div></div></blockquote></div></blockquote></div></div></blockquote><div class=""><br class=""></div>I am Canadian<br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir="ltr" class=""><blockquote class="gmail_quote" style="margin:0;margin-left:0.8ex;border-left:1px #ccc solid;padding-left:1ex"><div lang="EN-GB" link="#0563C1" vlink="#954F72" class=""><div class=""><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""><span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""> - UK/ EU will be advertised later. </span></p><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class="">Prospective students interested in Homotopy Type Theory and related subjects are especially ancouraged to apply.</span></p><div style="margin-right: 0cm; margin-bottom: 4.5pt; margin-left: 0cm;" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""> </span><br class="webkit-block-placeholder"></div><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class="">Please share!</span></p><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class="">Thorsten</span></p><div style="margin-right: 0cm; margin-bottom: 4.5pt; margin-left: 0cm;" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""> </span><br class="webkit-block-placeholder"></div><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm;text-align:start;word-spacing:0px" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""><a href="http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt" rel="nofollow" target="_blank" class="">http://www.cs.nott.ac.uk/~<wbr class="">pszgmh/phd-advert.txt</a></span></p><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"inherit",serif;color:#1c1e21" class=""><a href="https://www.nottingham.ac.uk/jobs/currentvacancies/%E2%80%A6/SCI1918" rel="nofollow" target="_blank" class="">https://www.nottingham.ac.uk/<wbr class="">jobs/currentvacancies/…/<wbr class="">SCI1918</a></span><span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""></span></p><p style="margin-right:0cm;margin-bottom:0cm;margin-left:0cm;margin-bottom:.0001pt;text-align:start;word-spacing:0px" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""><a href="https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY" rel="nofollow" target="_blank" class=""><span style="font-family:"inherit",serif;color:#385898" class="">https://www.nottingham.ac.uk/<wbr class="">research/groups/fp-lab/</span></a></span></p><div class=""><span style="font-size:11.0pt" class=""> </span><br class="webkit-block-placeholder"></div> </div> <pre class="">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></div> </blockquote></div></blockquote></div><div class=""><br class="webkit-block-placeholder"></div> -- <br class=""> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br class=""> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" class="">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br class=""> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com?utm_medium=email&utm_source=footer" class="">https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com</a>.<br class=""> </div></blockquote></div><br class=""></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/5CB8B1AE-98BA-4B4C-8592-C7850892FFBB%40gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/5CB8B1AE-98BA-4B4C-8592-C7850892FFBB%40gmail.com</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 2776 bytes --] > On Dec 22, 2019, at 1:05 AM, Justin Scarfy <pujustinyang@gmail.com <mailto:pujustinyang@gmail.com>> wrote: > > > > On Saturday, December 21, 2019 at 7:06:06 AM UTC-8, Justin Scarfy wrote: > I am interested in this [these] positions- I am a mathematician in Vancouver, Canada, but I never graduated from the undergrad degree as UBC wants me to follow their rules and do two more none-math courses, all i do is math/ programming [for 20+ hours a day] for the past 10 years > > On Tuesday, December 17, 2019 at 4:00:59 AM UTC-8, Thorsten Altenkirch wrote: > We are looking for students (in the moment only international > I am Canadian > - UK/ EU will be advertised later. > > Prospective students interested in Homotopy Type Theory and related subjects are especially ancouraged to apply. > > > Please share! > > Thorsten > > > http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt <http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt> > https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918 <https://www.nottingham.ac.uk/jobs/currentvacancies/%E2%80%A6/SCI1918> > https://www.nottingham.ac.uk/research/groups/fp-lab/ <https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY> > > 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 <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com <https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%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/863DBD14-383B-4B36-9E1D-296341D79126%40gmail.com. [-- Attachment #2: Type: text/html, Size: 7348 bytes --] <html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Dec 22, 2019, at 1:05 AM, Justin Scarfy <<a href="mailto:pujustinyang@gmail.com" class="">pujustinyang@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><br class=""><br class="">On Saturday, December 21, 2019 at 7:06:06 AM UTC-8, Justin Scarfy wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir="ltr" class="">I am interested in this [these] positions- I am a mathematician in Vancouver, Canada, but I never graduated from the undergrad degree as UBC wants me to follow their rules and do two more none-math courses, all i do is math/ programming [for 20+ hours a day] for the past 10 years<br class=""><br class="">On Tuesday, December 17, 2019 at 4:00:59 AM UTC-8, Thorsten Altenkirch wrote:<blockquote class="gmail_quote" style="margin:0;margin-left:0.8ex;border-left:1px #ccc solid;padding-left:1ex"> <div lang="EN-GB" link="#0563C1" vlink="#954F72" class=""> <div class=""><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class="">We are looking for students (in the moment only international</span></p></div></div></blockquote></div></blockquote></div></div></blockquote><div class=""><br class=""></div>I am Canadian<br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir="ltr" class=""><blockquote class="gmail_quote" style="margin:0;margin-left:0.8ex;border-left:1px #ccc solid;padding-left:1ex"><div lang="EN-GB" link="#0563C1" vlink="#954F72" class=""><div class=""><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""><span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""> - UK/ EU will be advertised later. </span></p><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class="">Prospective students interested in Homotopy Type Theory and related subjects are especially ancouraged to apply.</span></p><div style="margin-right: 0cm; margin-bottom: 4.5pt; margin-left: 0cm;" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""> </span><br class="webkit-block-placeholder"></div><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class="">Please share!</span></p><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class="">Thorsten</span></p><div style="margin-right: 0cm; margin-bottom: 4.5pt; margin-left: 0cm;" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""> </span><br class="webkit-block-placeholder"></div><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm;text-align:start;word-spacing:0px" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""><a href="http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt" rel="nofollow" target="_blank" class="">http://www.cs.nott.ac.uk/~<wbr class="">pszgmh/phd-advert.txt</a></span></p><p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm" class=""> <span style="font-size:10.5pt;font-family:"inherit",serif;color:#1c1e21" class=""><a href="https://www.nottingham.ac.uk/jobs/currentvacancies/%E2%80%A6/SCI1918" rel="nofollow" target="_blank" class="">https://www.nottingham.ac.uk/<wbr class="">jobs/currentvacancies/…/<wbr class="">SCI1918</a></span><span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""></span></p><p style="margin-right:0cm;margin-bottom:0cm;margin-left:0cm;margin-bottom:.0001pt;text-align:start;word-spacing:0px" class=""> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21" class=""><a href="https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY" rel="nofollow" target="_blank" class=""><span style="font-family:"inherit",serif;color:#385898" class="">https://www.nottingham.ac.uk/<wbr class="">research/groups/fp-lab/</span></a></span></p><div class=""><span style="font-size:11.0pt" class=""> </span><br class="webkit-block-placeholder"></div> </div> <pre class="">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></div> </blockquote></div></blockquote></div><div class=""><br class="webkit-block-placeholder"></div> -- <br class=""> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br class=""> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com" class="">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br class=""> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com?utm_medium=email&utm_source=footer" class="">https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com</a>.<br class=""> </div></blockquote></div><br class=""></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/863DBD14-383B-4B36-9E1D-296341D79126%40gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/863DBD14-383B-4B36-9E1D-296341D79126%40gmail.com</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 1992 bytes --] On Saturday, December 21, 2019 at 7:06:06 AM UTC-8, Justin Scarfy wrote: > > I am interested in this [these] positions- I am a mathematician in > Vancouver, Canada, but I never graduated from the undergrad degree as UBC > wants me to follow their rules and do two more none-math courses, all i do > is math/ programming [for 20+ hours a day] for the past 10 years > > On Tuesday, December 17, 2019 at 4:00:59 AM UTC-8, Thorsten Altenkirch > wrote: >> >> We are looking for students (in the moment only international - UK/ EU >> will be advertised later. >> >> Prospective students interested in Homotopy Type Theory and related >> subjects are especially ancouraged to apply. >> >> >> >> Please share! >> >> Thorsten >> >> >> >> http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt >> >> https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918 >> >> https://www.nottingham.ac.uk/research/groups/fp-lab/ >> <https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY> >> >> >> >> 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/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 5996 bytes --] <div dir="ltr"><br><br>On Saturday, December 21, 2019 at 7:06:06 AM UTC-8, Justin Scarfy wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir="ltr">I am interested in this [these] positions- I am a mathematician in Vancouver, Canada, but I never graduated from the undergrad degree as UBC wants me to follow their rules and do two more none-math courses, all i do is math/ programming [for 20+ hours a day] for the past 10 years<br><br>On Tuesday, December 17, 2019 at 4:00:59 AM UTC-8, Thorsten Altenkirch wrote:<blockquote class="gmail_quote" style="margin:0;margin-left:0.8ex;border-left:1px #ccc solid;padding-left:1ex"> <div lang="EN-GB" link="#0563C1" vlink="#954F72"> <div> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21">We are looking for students (in the moment only international - UK/ EU will be advertised later. </span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21">Prospective students interested in Homotopy Type Theory and related subjects are especially ancouraged to apply.</span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"> </span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21">Please share!</span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21">Thorsten</span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"> </span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm;text-align:start;word-spacing:0px"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"><a href="http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt" rel="nofollow" target="_blank" onmousedown="this.href='http://www.google.com/url?q\x3dhttp%3A%2F%2Fwww.cs.nott.ac.uk%2F~pszgmh%2Fphd-advert.txt\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGzvwA-rhoTqNtYRfIdKt6rTwF4YQ';return true;" onclick="this.href='http://www.google.com/url?q\x3dhttp%3A%2F%2Fwww.cs.nott.ac.uk%2F~pszgmh%2Fphd-advert.txt\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGzvwA-rhoTqNtYRfIdKt6rTwF4YQ';return true;">http://www.cs.nott.ac.uk/~<wbr>pszgmh/phd-advert.txt</a></span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"inherit",serif;color:#1c1e21"><a href="https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918" rel="nofollow" target="_blank" onmousedown="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fwww.nottingham.ac.uk%2Fjobs%2Fcurrentvacancies%2F%E2%80%A6%2FSCI1918\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGe2TUd-L9JFN2YtYj9YnMcZChTQA';return true;" onclick="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fwww.nottingham.ac.uk%2Fjobs%2Fcurrentvacancies%2F%E2%80%A6%2FSCI1918\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGe2TUd-L9JFN2YtYj9YnMcZChTQA';return true;">https://www.nottingham.ac.uk/<wbr>jobs/currentvacancies/…/<wbr>SCI1918</a></span><span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"></span></p> <p style="margin-right:0cm;margin-bottom:0cm;margin-left:0cm;margin-bottom:.0001pt;text-align:start;word-spacing:0px"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"><a href="https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY" rel="nofollow" target="_blank" onmousedown="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fwww.nottingham.ac.uk%2Fresearch%2Fgroups%2Ffp-lab%2F%3Ffbclid%3DIwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGmO47ShOKlukNPawQqnaes_QMHvQ';return true;" onclick="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fwww.nottingham.ac.uk%2Fresearch%2Fgroups%2Ffp-lab%2F%3Ffbclid%3DIwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGmO47ShOKlukNPawQqnaes_QMHvQ';return true;"><span style="font-family:"inherit",serif;color:#385898">https://www.nottingham.ac.uk/<wbr>research/groups/fp-lab/</span></a></span></p> <p class="MsoNormal"><span style="font-size:11.0pt"> </span></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></div> </blockquote></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/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/edf8b644-dff8-4d0f-af57-f6e51fe68940%40googlegroups.com</a>.<br />

[-- Attachment #1.1: Type: text/plain, Size: 1838 bytes --] I am interested in this [these] positions- I am a mathematician in Vancouver, Canada, but I never graduated from the undergrad degree as UBC wants me to follow their rules and do two more none-math courses, all i do is math/ programming for the past 10 years On Tuesday, December 17, 2019 at 4:00:59 AM UTC-8, Thorsten Altenkirch wrote: > > We are looking for students (in the moment only international - UK/ EU > will be advertised later. > > Prospective students interested in Homotopy Type Theory and related > subjects are especially ancouraged to apply. > > > > Please share! > > Thorsten > > > > http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt > > https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918 > > https://www.nottingham.ac.uk/research/groups/fp-lab/ > <https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY> > > > > 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/01690ffb-8b83-4ab9-99c9-f315cfe330e1%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 5749 bytes --] <div dir="ltr">I am interested in this [these] positions- I am a mathematician in Vancouver, Canada, but I never graduated from the undergrad degree as UBC wants me to follow their rules and do two more none-math courses, all i do is math/ programming for the past 10 years<br><br>On Tuesday, December 17, 2019 at 4:00:59 AM UTC-8, Thorsten Altenkirch wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"> <div lang="EN-GB" link="#0563C1" vlink="#954F72"> <div> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21">We are looking for students (in the moment only international - UK/ EU will be advertised later. </span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21">Prospective students interested in Homotopy Type Theory and related subjects are especially ancouraged to apply.</span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"> </span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21">Please share!</span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21">Thorsten</span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"> </span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm;text-align:start;word-spacing:0px"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"><a href="http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt" target="_blank" rel="nofollow" onmousedown="this.href='http://www.google.com/url?q\x3dhttp%3A%2F%2Fwww.cs.nott.ac.uk%2F~pszgmh%2Fphd-advert.txt\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGzvwA-rhoTqNtYRfIdKt6rTwF4YQ';return true;" onclick="this.href='http://www.google.com/url?q\x3dhttp%3A%2F%2Fwww.cs.nott.ac.uk%2F~pszgmh%2Fphd-advert.txt\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGzvwA-rhoTqNtYRfIdKt6rTwF4YQ';return true;">http://www.cs.nott.ac.uk/~<wbr>pszgmh/phd-advert.txt</a></span></p> <p style="margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"inherit",serif;color:#1c1e21"><a href="https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918" target="_blank" rel="nofollow" onmousedown="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fwww.nottingham.ac.uk%2Fjobs%2Fcurrentvacancies%2F%E2%80%A6%2FSCI1918\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGe2TUd-L9JFN2YtYj9YnMcZChTQA';return true;" onclick="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fwww.nottingham.ac.uk%2Fjobs%2Fcurrentvacancies%2F%E2%80%A6%2FSCI1918\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGe2TUd-L9JFN2YtYj9YnMcZChTQA';return true;">https://www.nottingham.ac.uk/<wbr>jobs/currentvacancies/…/<wbr>SCI1918</a></span><span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"></span></p> <p style="margin-right:0cm;margin-bottom:0cm;margin-left:0cm;margin-bottom:.0001pt;text-align:start;word-spacing:0px"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1c1e21"><a href="https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY" target="_blank" rel="nofollow" onmousedown="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fwww.nottingham.ac.uk%2Fresearch%2Fgroups%2Ffp-lab%2F%3Ffbclid%3DIwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGmO47ShOKlukNPawQqnaes_QMHvQ';return true;" onclick="this.href='https://www.google.com/url?q\x3dhttps%3A%2F%2Fwww.nottingham.ac.uk%2Fresearch%2Fgroups%2Ffp-lab%2F%3Ffbclid%3DIwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNGmO47ShOKlukNPawQqnaes_QMHvQ';return true;"><span style="font-family:"inherit",serif;color:#385898">https://www.nottingham.ac.uk/<wbr>research/groups/fp-lab/</span></a></span></p> <p class="MsoNormal"><span style="font-size:11.0pt"> </span></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></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/01690ffb-8b83-4ab9-99c9-f315cfe330e1%40googlegroups.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/01690ffb-8b83-4ab9-99c9-f315cfe330e1%40googlegroups.com</a>.<br />

[-- Attachment #1: Type: text/plain, Size: 1415 bytes --] We are looking for students (in the moment only international - UK/ EU will be advertised later. Prospective students interested in Homotopy Type Theory and related subjects are especially ancouraged to apply. Please share! Thorsten http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918 https://www.nottingham.ac.uk/research/groups/fp-lab/<https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY> 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/CAC7C301-BC77-4BF8-90E1-A2FAB6FF7115%40nottingham.ac.uk. [-- Attachment #2: Type: text/html, Size: 5688 bytes --] <html 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:inherit; 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:12.0pt; font-family:"Calibri",sans-serif; mso-fareast-language:EN-US;} a:link, span.MsoHyperlink {mso-style-priority:99; color:#0563C1; text-decoration:underline;} a:visited, span.MsoHyperlinkFollowed {mso-style-priority:99; color:#954F72; text-decoration:underline;} span.EmailStyle17 {mso-style-type:personal-compose; font-family:"Calibri",sans-serif; color:windowtext;} .MsoChpDefault {mso-style-type:export-only; font-family:"Calibri",sans-serif; mso-fareast-language:EN-US;} @page WordSection1 {size:612.0pt 792.0pt; margin:72.0pt 72.0pt 72.0pt 72.0pt;} div.WordSection1 {page:WordSection1;} --></style> </head> <body lang="EN-GB" link="#0563C1" vlink="#954F72"> <div class="WordSection1"> <p style="mso-margin-top-alt:0cm;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21">We are looking for students (in the moment only international - UK/ EU will be advertised later. <o:p></o:p></span></p> <p style="mso-margin-top-alt:0cm;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21">Prospective students interested in Homotopy Type Theory and related subjects are especially ancouraged to apply.<o:p></o:p></span></p> <p style="mso-margin-top-alt:0cm;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21"><o:p> </o:p></span></p> <p style="mso-margin-top-alt:0cm;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21">Please share!<o:p></o:p></span></p> <p style="mso-margin-top-alt:0cm;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21">Thorsten<o:p></o:p></span></p> <p style="mso-margin-top-alt:0cm;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21"><o:p> </o:p></span></p> <p style="mso-margin-top-alt:4.5pt;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm;caret-color: rgb(28, 30, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;word-spacing:0px"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21">http://www.cs.nott.ac.uk/~pszgmh/phd-advert.txt<o:p></o:p></span></p> <p style="mso-margin-top-alt:4.5pt;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm"> <span style="font-size:10.5pt;font-family:"inherit",serif;color:#1C1E21"><a href="https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918">https://www.nottingham.ac.uk/jobs/currentvacancies/…/SCI1918</a></span><span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21"><o:p></o:p></span></p> <p style="mso-margin-top-alt:4.5pt;margin-right:0cm;margin-bottom:0cm;margin-left:0cm;margin-bottom:.0001pt;caret-color: rgb(28, 30, 33);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-size-adjust: auto;-webkit-text-stroke-width: 0px;word-spacing:0px"> <span style="font-size:10.5pt;font-family:"Arial",sans-serif;color:#1C1E21"><a href="https://www.nottingham.ac.uk/research/groups/fp-lab/?fbclid=IwAR22DBUr6V-gu3Su8Yzm6XmYXe4fT9mKXF4HeyneQdPYt7k-TgqCTh7JCEY" target="_blank"><span style="font-family:"inherit",serif;color:#385898">https://www.nottingham.ac.uk/research/groups/fp-lab/</span></a><o:p></o:p></span></p> <p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></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/CAC7C301-BC77-4BF8-90E1-A2FAB6FF7115%40nottingham.ac.uk?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAC7C301-BC77-4BF8-90E1-A2FAB6FF7115%40nottingham.ac.uk</a>.<br />

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