[-- Attachment #1: Type: text/plain, Size: 1252 bytes --] Dear all, We are pleased to announce the fourth Midwest Homotopy Type Theory Seminar which will take place at the Ohio State University on the weekend of April 25-26, 2020. INVITED SPEAKERS: - Evan Cavallo (Carnegie Mellon) - Andrew Swan (Carnegie Mellon) - Matthew Weaver (Princeton) REGISTRATION: There is no registration fee, but registration will help the organizers. Please register using this form: https://forms.gle/zBKZeG3caLGq8JDq7 SUBMITTED TALKS: Please submit talks using the registration form. FUNDING: Some funding is available to help young researchers attend the seminar. Please indicate any interest in the registration form. FURTHER DETAILS: Further details, including information about lodging, can be found at https://paigenorth.github.io/midwesthott/ Best, Paige Randall North 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/CALsq1T%3DNFbYhun_4iQmxqhF%2B%3Dt_dyiExixThodgHXKHZrupK%2BQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2182 bytes --]

[Submissions from the HoTT/UF community would be very welcome, in particular with Finster, Garner, Licata, Shulman on the PC this year.] CALL FOR PAPERS 3rd Annual International Conference on Applied Category Theory (ACT2020) July 6 – 10, 2020, MIT, USA http://act2020.mit.edu * * * Applied category theory is a topic of interest for a growing community of researchers interested in studying many different kinds of systems using category-theoretic tools. These systems are found across computer science, mathematics, and physics, as well as in social science, linguistics, cognition, and neuroscience. The background and experience of our members is as varied as the systems being studied. The goal of the Applied Category Theory conference is to bring the majority of researchers in the field together and provide a platform for exposing progress in the area. We seek submissions of both original research papers and extended abstracts of work that's been submitted, accepted, or published elsewhere. Original research papers we accept will be invited for publication in a proceedings volume. Some contributions will be invited to become keynote addresses, and best paper award(s) may also be given. The conference will include a business showcase, and it will be preceded by a tutorial day. This event follows ACT 2018 in Leiden, and ACT 2019 in Oxford. ** IMPORTANT DATES (all in 2020)** Submission of contributed papers: April 26 Acceptance/Rejection notification: May 17 Early bird registration deadline: May 20 Final registration deadline: June 26 Tutorial day: July 5 Main conference: July 6 – 10 ** SUBMISSIONS ** Two types of submissions are accepted, both of which will be reviewed using the same standards: - Proceedings Track. Original contributions of high-quality work consisting of a 5–12 page extended abstract that provides evidence of results of genuine interest, and with enough detail to allow the program committee to assess the merits of the work. Submission of a work-in-progress is encouraged, but it must be more substantial than a research proposal. - Non-Proceedings Track. Descriptions of high-quality work submitted or published elsewhere will also be considered, provided the work is recent and relevant to the conference. The work may be of any length, but the program committee members may only look at the first 3 pages of the submission, so you should ensure that these pages contain sufficient evidence of the quality and rigor of your work. Submissions should be prepared using LaTeX, and must be submitted in PDF format. The submission link is available on the ACT2020 web page. ** PROGRAM COMMITTEE ** Mathieu Anel, Carnegie Mellon University John Baez, Centre for Quantum Technologies Richard Blute, University of Ottawa Tai-Danae Bradley, City University of New York Andrea Censi, ETH Zurich Bob Coecke, University of Oxford Valeria de Paiva, Samsung Research America and University of Birmingham Ross Duncan, University of Strathclyde Eric Finster, University of Birmingham Brendan Fong, Massachusetts Institute of Technology Tobias Fritz, Perimeter Institute for Theoretical Physics Richard Garner, Macquarie University Fabrizio Romano Genovese, Statebox Amar Hadzihasanovic, IRIF, Université de Paris Helle Hvid Hansen, Delft University of Technology Jules Hedges, Max Planck Institute for Mathematics in the Sciences Kathryn Hess Bellwald, Ecole Polytechnique Fédérale de Lausanne Chris Heunen, The University of Edinburgh Joachim Kock, Universitat Autònoma de Barcelona Tom Leinster, The University of Edinburgh Martha Lewis, University of Amsterdam Daniel R. Licata, Wesleyan University David Jaz Myers, Johns Hopkins University Paolo Perrone, Massachusetts Institute of Technology Vaughan Pratt, Stanford University Peter Selinger, Dalhousie University Michael Shulman, University of San Diego David I. Spivak, Massachusetts Institute of Technology (co-chair) Walter Tholen, York University Todd Trimble, Western Connecticut State University Jamie Vicary, University of Birmingham (co-chair) Maaike Zwart, University of Oxford ** STEERING COMMITTEE ** John Baez (University of California Riverside) Bob Coecke (University of Oxford) David Spivak (MIT) Christina Vasilakopoulou (University of Patras) -- 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/CANr23v02PNx9MaQDVQ7E%3D3nU7nKR6oYV%2BKr7i55e4i97yVM%3D4Q%40mail.gmail.com.

[-- Attachment #1.1: Type: text/plain, Size: 2301 bytes --] [This is a reminder that the deadline for pre-registration is ** March 15, 2020 **, note that we are pleased to have to new lectures by Valery Isaev and Paige North] ==================================================================== Spring School on Theoretical Computer Science (EPIT) – Homotopy Type Theory Ile d’Oléron, CAES CNRS La vieille Perrotine, France. 25th-29th May 2020 https://epit2020cnrs.inria.fr ==================================================================== The EPIT is a French thematic school proposing, on an yearly basis, an intensive 5-day long training, specializing on a particular topic in theoretical computer science. It is primarily addressed to PhD students, Post-doctoral researchers and junior academics. The 2020 edition of the EPIT will be centered around Homotopy Type Theory, a research topic at the junction of Computer Science and Mathematics. Our hope is hence to provide an introduction that is accessible to researchers in both areas. Pre-registration is now open, please visit https://epit2020cnrs.inria.fr/registration/ to know more. For any question, please contact epit2020@sciencesconf.org NB: As the number of places is limited, we have fixed a deadline for pre-registration to ** March 15, 2020 **. -------------------------------------------------------------------- Lecturers Andrej Bauer (Ljubljana University): Introduction to Homotopy Type Theory Guillaume Brunerie (Stockholm University): Synthetic Homotopy Theory Valery Isaev (JetBrain, Saint Petersburg): The Arend proof assistant Anders Mörtberg (Stockholm University): Cubical Type Theory Paige North (Ohio State University): Directed Homotopy Type Theory Andy Pitts (Cambridge University): Models of (Univalent) Type Theory Bas Spitters (Aarhus University): The Coq-HoTT library -- 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/0e10d866-00f3-4311-90a9-f704ef26e10b%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 8893 bytes --]

Yes, I think probably you want indexed categories, incarnated as fibrations. You can then remove the invertibility too: if C is the 1-object category corresponding to the monoid of natural numbers, then an opfibration over C is a category equipped with an endofunctor, an endomorphism over the generating morphism of C is an algebra for that endofunctor, and its n-fold composition with itself is the corresponding algebra for F^n. On Fri, Feb 28, 2020 at 10:44 AM Noah Snyder <nsnyder@gmail.com> wrote: > > Mike pointed out that I didn't explain how my example is a special case of dependent path composition. A type family over S^1 is a higher groupoid together with an (invertible) endofunctor F. A path over loop is an algebra for that endofunctor (where the map is an iso). If you dependent path compose it with itself n times you get a path over loop^n, i.e. an algebra for F^n. Best, > > Noah > > On Fri, Feb 28, 2020 at 10:33 AM Noah Snyder <nsnyder@gmail.com> wrote: >> >> Section 2.3 of the book introduces "dependent paths" (which are paths in a fibration "lying over" a path in the base) and "dependent path composition" which composes such dependent paths when that makes sense. I'm working on a paper that's not about HoTT but where "dependent path composition" plays an important role. The problem I'm running into is that I don't know what dependent path composition is called in "standard" mathematics. Does anyone know if this has another name in higher category theory? (Naturally, we'll include a remark mentioning the HoTT way of thinking about this (since it's how I think about it!), but I think that won't be illuminating to most of our target audience.) >> >> The simplest example of what I have in mind here is if C is a category and F is an endofunctor and c is an F-algebra (i.e. we have endowed c with a chosen map f: F(c) --> c) then c is also an F^n-algebra by taking the "nth power of f" which actually means f \circ F(f) \circ F^2(f) \circ ... \circ F^{n-1}(f). In particular, I think this example illustrates that you can talk about "dependent k-morphisms" and their compositions without requiring anything in sight to be a (higher) groupoid. >> >> My best guess is that the right setting might be "indexed (higher) categories"? >> >> Best, >> >> Noah > > -- > 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/CAO0tDg5mstbw3Ujjfu%2BkMfgW7_7y7raxbWV_yh-2phB2ynwb8g%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/CAOvivQzAoLQkXUNDkauM5so1rNu9-LsyWRHM4xO16d4O8Wt-0A%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 2651 bytes --] Dear all, This is a reminder for the memorial conference for Erik Palmgren, on Thu/Fri 7–8 May (plus excursion Sat 9), at Stockholm University: http://logic.math.su.se/palmgren-memorial/ (Full original CfP forwarded below.) In particular, if you would like to speak, or apply for travel funding (for early-career participants), please let us know by *next Friday, March 6* at the latest (original deadline was last Friday). Best wishes, –Peter. ---------- Forwarded message --------- From: Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com> Date: Thu, Jan 23, 2020 at 2:40 PM Subject: CfP: Memorial Conference for Erik Palmgren, 7–8 May, Stockholm Dear all, A memorial conference for Erik Palmgren will take place on Thu/Fri 7–8 May 2020 (plus excursion on Sat 9), at Stockholm University: http://logic.math.su.se/palmgren-memorial/ Topics may include all Erik’s academic interests: type theory and its models, categorical logic and foundations, constructive mathematics and proof theory, nonstandard analysis, and the philosophy of constructive mathematics. Invited speakers (confirmed): • Douglas Bridges • Jacopo Emmenegger • Christian Espíndola • Håkon Gylterud • Hajime Ishihara • Millie Maietti • Ieke Moerdijk • Peter Schuster There is some space for contributed talks. If you would like to speak, please send a title and abstract to <palmgren-memorial@math.su.se> by Friday February 28 [NB now extended to Fri March 6.]. Contributions are especially encouraged from those who knew and worked with Erik. Registration is free; please email <palmgren-memorial@math.su.se> by Friday 3 April if you plan to attend. Some travel funding is available for early-career participants. To apply, please let us know in your registration email by Friday February 28. [NB now extended to Fri March 6.] The conference is organized by Erik’s students and colleagues at Stockholm University: • Guillaume Brunerie • Menno de Boer • Henrik Forssell • Peter LeFanu Lumsdaine • Johan Lindberg • Per Martin-Löf • Anna Montaruli • Anders Mörtberg Please feel free to redistribute this announcement. Best wishes, –Peter. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-n49zVQjYUMawqHPRUTDTMNc6PWJ1c2m9rh8a5%3DrOnOqA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3326 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2211 bytes --] Mike pointed out that I didn't explain how my example is a special case of dependent path composition. A type family over S^1 is a higher groupoid together with an (invertible) endofunctor F. A path over loop is an algebra for that endofunctor (where the map is an iso). If you dependent path compose it with itself n times you get a path over loop^n, i.e. an algebra for F^n. Best, Noah On Fri, Feb 28, 2020 at 10:33 AM Noah Snyder <nsnyder@gmail.com> wrote: > Section 2.3 of the book introduces "dependent paths" (which are paths in a > fibration "lying over" a path in the base) and "dependent path composition" > which composes such dependent paths when that makes sense. I'm working on > a paper that's not about HoTT but where "dependent path composition" plays > an important role. The problem I'm running into is that I don't know what > dependent path composition is called in "standard" mathematics. Does > anyone know if this has another name in higher category theory? > (Naturally, we'll include a remark mentioning the HoTT way of thinking > about this (since it's how I think about it!), but I think that won't be > illuminating to most of our target audience.) > > The simplest example of what I have in mind here is if C is a category and > F is an endofunctor and c is an F-algebra (i.e. we have endowed c with a > chosen map f: F(c) --> c) then c is also an F^n-algebra by taking the "nth > power of f" which actually means f \circ F(f) \circ F^2(f) \circ ... \circ > F^{n-1}(f). In particular, I think this example illustrates that you can > talk about "dependent k-morphisms" and their compositions without requiring > anything in sight to be a (higher) groupoid. > > My best guess is that the right setting might be "indexed (higher) > categories"? > > Best, > > Noah > -- 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/CAO0tDg5mstbw3Ujjfu%2BkMfgW7_7y7raxbWV_yh-2phB2ynwb8g%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3040 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1698 bytes --] Section 2.3 of the book introduces "dependent paths" (which are paths in a fibration "lying over" a path in the base) and "dependent path composition" which composes such dependent paths when that makes sense. I'm working on a paper that's not about HoTT but where "dependent path composition" plays an important role. The problem I'm running into is that I don't know what dependent path composition is called in "standard" mathematics. Does anyone know if this has another name in higher category theory? (Naturally, we'll include a remark mentioning the HoTT way of thinking about this (since it's how I think about it!), but I think that won't be illuminating to most of our target audience.) The simplest example of what I have in mind here is if C is a category and F is an endofunctor and c is an F-algebra (i.e. we have endowed c with a chosen map f: F(c) --> c) then c is also an F^n-algebra by taking the "nth power of f" which actually means f \circ F(f) \circ F^2(f) \circ ... \circ F^{n-1}(f). In particular, I think this example illustrates that you can talk about "dependent k-morphisms" and their compositions without requiring anything in sight to be a (higher) groupoid. My best guess is that the right setting might be "indexed (higher) categories"? Best, Noah -- 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/CAO0tDg7uSiQrU8%2B0tnwJQHB_AWvRKAxmAePF88GOvd_ra%3DrpwA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2226 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2606 bytes --] [Apologies for multiple postings.] Autumn school "Proof and Computation" Fischbachau, Germany, 20th to 26th September 2020 http://www.mathematik.uni-muenchen.de/~schwicht/pc20.php The fifth international autumn school "Proof and Computation" will be held from 20th to 26th September 2020 in Fischbachau near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy. SCOPE -------------------- - Predicative Foundations - Constructive Mathematics and Type Theory - Computation in Higher Types - Extraction of Programs from Proofs COURSES -------------------- - Steve Awodey: Categorical logic - Marc Bezem: Coherent logic - Hajime Ishihara: Reverse mathematics in constructive set theory - Stefan Neuwirth: The philosophy of dynamic algebra - Frederik Nordvall Forsberg: Universes of data types in constructive type theory - Monika Seisenberger: Extraction of programs from proofs - Chuangjie Xu: Various approaches to compute moduli of continuity WORKING GROUPS -------------------- There will be an opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of constructing correct programs from proofs. APPLICATIONS -------------------- Graduate or PhD students and young postdoctoral researches are invited to apply. Applications (e.g. a self-introduction including research interests and motivation) should be sent to Chuangjie Xu <xu@math.lmu.de>. Students are required to provide also a letter of recommendation, preferably from the thesis adviser. Deadline for applications: **30 May 2020**. Applicants will be notified by 20th June 2020. FINANCIAL SUPPORT -------------------- Successful applicants will be offered **full-board accommodation** for the days of the autumn school. There are NO funds, however, to reimburse travel or further expenses, which successful applicants will have to cover otherwise. The workshop is supported by the Udo Keller Stiftung (Hamburg), the CID (Computing with Infinite Data) programme of the European Commission and a JSPS core-to-core project. Klaus Mainzer Peter Schuster Helmut Schwichtenberg -- 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/d459f9a3-0791-4b32-9e17-7fcba5aa0ccb%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 18419 bytes --]

Logical Frameworks and Meta-Languages: Theory and Practice LFMTP 2020 Paris, France 29 June 2020 Affiliated with FSCD 2020 and IJCAR 2020 https://lfmtp.org/workshops/2020/ Abstract submission deadline: 5 April 2020 Paper submission deadline: 11 April 2020 SPECIAL SESSION IN HONOUR OF Frank Pfenning To celebrate the 60th birthday of Frank Pfenning and his great many contributions to the topics of LFMTP, one session will be devoted to talks by collaborators and friends of Frank. ABOUT LFMTP Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2020 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages, process calculi and related formally specified systems. * Formalisation of model-theoretic and proof-theoretic semantics of logics. * Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Design and implementation of systems and tools related to meta- languages and logical frameworks IMPORTANT DATES All deadlines are established as the end of day (23:59) AoE. * Abstract submission deadline: 5 April 2020 * Submission deadline: 11 April 2020 * Notification to authors: 13 May 2020 * Final version due: 22 May 2020 * Workshop: 29 June 2020 SUBMISSION INFORMATION In addition to regular papers, we accept the submission of "work in progress" reports, in a broad sense. Those do not need to report fully polished research results, but should be of interest for the community at large. Submitted papers should be in PDF, formatted using the EPTCS LaTeX style. The length is restricted to 15 pages for regular papers and 8 pages for "Work in Progress" papers. Submission is via EasyChair: https://easychair.org/my/conference?conf=lfmtp2020 All submissions will be peer-reviewed and the authors of those accepted will be invited to present their papers at the workshop. POST-PROCEEDINGS After the workshop we will publish post-proceedings in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series. Accepted regular papers will be published in the post-proceedings. Authors of selected work-in-progress papers will be invited to submit the full versions of their papers for publication in the post- proceedings, subject to another round of review. PROGRAM COMMITTEE David Baelde, LSV, ENS Paris-Saclay & Inria Paris Frédéric Blanqui, INRIA Alberto Ciaffaglione, University of Udine Dennis Müller, Friedrich-Alexander-University Erlangen-Nürnberg Michael Norrish, Data61 Carlos Olarte, Universidade Federal do Rio Grande do Norde Claudio Sacerdoti Coen, University of Bologna (PC Co-Chair) Ulrich Schöpp, fortiss GmbH Alwen Tiu, Australian National University (PC Co-Chair) Tjark Weber, Uppsala University -- Prof. Claudio Sacerdoti Coen Department of Computer Science and Engineering University of Bologna -- 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/f1d9cafe27cd0e663d686f32a88da55939c700bf.camel%40unibo.it.

======== CALL FOR PARTICIPATION 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. The next SYCO, to be held at Tallinn University of Technology, will host 2 invited talks and 14 contributed talks. Topics range from logical methods in computer science, to higher category theory, through applications of categories in probability and linguistics. INVITED TALKS ======== * Bartek Klin (University of Warsaw) Monadic monadic second order logic * Christine Tasson (IRIF, Université de Paris) The linear-non-linear substitution 2-monad CONTRIBUTED TALKS ======== * Sivert Aasnæss - Contextuality for circuits * Vikraman Choudhury - Tracking intensional resources using weighted sets and comonads * Elena di Lavore - A proposal for subgame perfection in compositional game theory * Tobias Fritz, Eigil Fjeldgren Rischel - The zero-one laws of Kolmogorov and Hewitt-Savage in categorical probability * Lukas Heidemann - Frames in pretriangulated dg-categories * Nick Hu - External traced monoidal categories * Maxime Lucas - Rewriting strategies as contracting homotopies * Violeta Martins de Freitas - Life in arrows: an introduction to applied category theory * Dylan McDermott, Alan Mycroft - On the relation between call-by-value and call-by-name * Michael Moortgat, Mehrnoosh Sadrzadeh, Gijs Wijnholds - A Frobenius algebraic analysis for parasitic gaps * Olivier Peltre - Homological algebra for message-passing algorithms * Alex Rice - Coinductive invertibility in higher categories * Julian Salamanca Téllez - Distributive laws over the powerset * Niels van der Weide - Constructing finitary 1-truncated higher inductive types as groupoid quotients REGISTRATION ======== Registration is open until Monday 23 March. Details are available on the conference website: http://events.cs.bham.ac.uk/syco/7/ PROGRAMME COMMITTEE ======== Miriam Backens, University of Birmingham 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 Kohei Kishida, University of Illinois at Urbana-Champaign Martha Lewis, ILLC, University of Amsterdam Samuel Mimram, École Polytechnique Koko Muroya, RIMS, Kyoto University Jovana Obradović, Institute of Mathematics CAS Viktoriya Ozornova, Ruhr-Universität Bochum 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 -- 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/CAJb9em1AaCP3PFxtjvu3wWNh49axXzRBdVs8JJRvWGsVhx2VWw%40mail.gmail.com.

Actually let me modify that: (G3) holds in any type-theoretic model topos. And since coproducts are disjoint, (G2) is implied by (G1) and (G3); while since the initial object is strict, (G1) merely asserts that it is fibrant. So if the initial object is fibrant, then all of (G1-G3) hold. The initial object isn't always fibrant, but I wouldn't be surprised if every Grothendieck (∞,1)-topos could be presented by a model category of this sort in which the initial object is fibrant, at least in a classical metatheory, for the same reason that every Grothendieck 1-topos is overt classically: we can simply remove from the site all objects that are covered by the empty family. But I haven't checked the details in the ∞-case. And I still don't know any way to make the NNO fibrant. On Fri, Feb 21, 2020 at 2:13 PM Michael Shulman <shulman@sandiego.edu> wrote: > > I believe the best that's known is that (assuming an inaccessible > cardinal) any Grothendieck (∞,1)-topos can be presented by a model > category -- namely, a left exact localization of an injective model > structure on simplicial presheaves -- satisfying all of Joyal's axioms > except those involving coproducts (G1-G3) and fibrancy of the NNO > (A2). Most of the properties are easy to show from the definitions; > G6 and G7 follow from the fact that it presents a Grothendieck > (∞,1)-topos; L2 follows from an adjoint pushout-product calculation; > and I showed L6 myself most recently in > https://arxiv.org/abs/1904.07004. > > The extra axioms (G1-G3) and (A2) hold in many examples -- e.g. the > injective model structure itself, which presents a presheaf > (∞,1)-topos, and probably also other examples such as sheaves on > locally connected sites. But in other cases even the initial object > may not be fibrant. Personally, my current opinion (subject to > change) is that (G1-G3) and (A2) are unreasonably strong, and > unnecessary for most purposes. > > > On Fri, Feb 21, 2020 at 5:23 AM Bas Spitters <b.a.w.spitters@gmail.com> wrote: > > > > In 2014, Andra Joyal proposed a definition of an elementary higher topos. > > > > "This lecture contains a proposed definition that is not an > > (∞,1)-category but a presentation of one by a model category-like > > structure; this is closer to the type theory, but further from the > > intended examples. In particular, there are unresolved coherence > > questions even as to whether every Grothendieck (∞,1)-topos can be > > presented by a model in Joyal’s sense (in particular, how strict can a > > universe be made, and can the natural numbers object be made > > fibrant)." > > https://ncatlab.org/nlab/show/elementary+%28infinity%2C1%29-topos > > > > Has there been any progress on these coherence questions? > > > > -- > > 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/CAOoPQuQc317E8qUEOWJ2JQD_iXAFyE%3DWcttruqd5A8tRpHqttg%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/CAOvivQwXyK0QMj-F0%2BCcEV1VjQoFTDh9P7P9630chx1V9Hpapg%40mail.gmail.com.

I believe the best that's known is that (assuming an inaccessible cardinal) any Grothendieck (∞,1)-topos can be presented by a model category -- namely, a left exact localization of an injective model structure on simplicial presheaves -- satisfying all of Joyal's axioms except those involving coproducts (G1-G3) and fibrancy of the NNO (A2). Most of the properties are easy to show from the definitions; G6 and G7 follow from the fact that it presents a Grothendieck (∞,1)-topos; L2 follows from an adjoint pushout-product calculation; and I showed L6 myself most recently in https://arxiv.org/abs/1904.07004. The extra axioms (G1-G3) and (A2) hold in many examples -- e.g. the injective model structure itself, which presents a presheaf (∞,1)-topos, and probably also other examples such as sheaves on locally connected sites. But in other cases even the initial object may not be fibrant. Personally, my current opinion (subject to change) is that (G1-G3) and (A2) are unreasonably strong, and unnecessary for most purposes. On Fri, Feb 21, 2020 at 5:23 AM Bas Spitters <b.a.w.spitters@gmail.com> wrote: > > In 2014, Andra Joyal proposed a definition of an elementary higher topos. > > "This lecture contains a proposed definition that is not an > (∞,1)-category but a presentation of one by a model category-like > structure; this is closer to the type theory, but further from the > intended examples. In particular, there are unresolved coherence > questions even as to whether every Grothendieck (∞,1)-topos can be > presented by a model in Joyal’s sense (in particular, how strict can a > universe be made, and can the natural numbers object be made > fibrant)." > https://ncatlab.org/nlab/show/elementary+%28infinity%2C1%29-topos > > Has there been any progress on these coherence questions? > > -- > 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/CAOoPQuQc317E8qUEOWJ2JQD_iXAFyE%3DWcttruqd5A8tRpHqttg%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/CAOvivQya7JthjksQC-XQ%2Bjuc3N_-O3JJibDjRM8F1hyML4CMAQ%40mail.gmail.com.

In 2014, Andra Joyal proposed a definition of an elementary higher topos. "This lecture contains a proposed definition that is not an (∞,1)-category but a presentation of one by a model category-like structure; this is closer to the type theory, but further from the intended examples. In particular, there are unresolved coherence questions even as to whether every Grothendieck (∞,1)-topos can be presented by a model in Joyal’s sense (in particular, how strict can a universe be made, and can the natural numbers object be made fibrant)." https://ncatlab.org/nlab/show/elementary+%28infinity%2C1%29-topos Has there been any progress on these coherence questions? -- 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/CAOoPQuQc317E8qUEOWJ2JQD_iXAFyE%3DWcttruqd5A8tRpHqttg%40mail.gmail.com.

FSCD 2020 will feature more satellite workshops than expected and as a result, the dates of HoTT/UF'20 had to be adjusted. Please see below for an updated announcement. We apologize for any inconvenience this may have caused. Best wishes, Chris Kapulkin for the organizers --- Workshop on Homotopy Type Theory and Univalent Foundations July 5-6, 2020, Paris, France (not Ontario) https://hott-uf.github.io/2020 Co-located with FSCD 2020 https://fscd2020.org/ Abstract submission deadline: March 25, 2020 Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Invited talks * Carlo Angiuli (Carnegie Mellon University) * Liron Cohen (Ben-Gurion University) * Pierre-Louis Curien (Université de Paris) # Submissions * Abstract submission deadline: March 25, 2020 * Author notification: mid-April 2020 Submissions should consist of a title and an abstract, in pdf format, of no more than 4 pages, submitted via https://easychair.org/conferences/?conf=hottuf2020 Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. # Program committee * Benedikt Ahrens (University of Birmingham) * Paolo Capriotti (Technische Universität Darmstadt) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Birmingham) * Peter LeFanu Lumsdaine (Stockholm University) * Anders Mörtberg (Stockholm University) * Paige Randall North (Ohio State University) * Nicolas Tabareau (Inria Nantes) # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario) -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3Nsvq_qW-EVhC5YAW-cr0%2B0d-32J%3DC0JO%3DaLMDpdcz%3DtA%40mail.gmail.com.

[-- Attachment #1.1: Type: text/plain, Size: 2364 bytes --] We are pleased to announce the School on Univalent Mathematics 2020, to be held at the Palazzone di Cortona (https://www.sns.it/en/palazzone-cortona), Cortona, Italy, July 27-31, 2020 (https://unimath.github.io/cortona2020/) Overview ======== Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky's program of Univalent Foundations, a new approach to foundations of mathematics based on ideas from homotopy theory, such as the Univalence Principle. The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is based on the computer proof assistant Coq. In this school and workshop, we aim to introduce newcomers to the ideas of Univalent Foundations and mathematics therein, and to the formalization of mathematics in a computer proof assistant based on Univalent Foundations. Format ======= Participants will receive an introduction to Univalent Foundations and to mathematics in those foundations, by leading experts in the field. In the accompanying problem sessions, they will formalize pieces of univalent mathematics in the UniMath library. More information on the format is given on the website https://unimath.github.io/cortona2020 . Application and funding ======================= For information on how to participate, please visit https://unimath.github.io/cortona2020/. Mentors ====== Benedikt Ahrens (University of Birmingham) Joseph Helfer (Stanford University) Tom de Jong (University of Birmingham) Marco Maggesi (University of Florence) Ralph Matthes (CNRS, University Toulouse) Paige Randall North (The Ohio State University) Niccolò Veltri (Tallinn University of Technolog) Niels van der Weide (University of Nijmegen) Best regards, The organizers Benedikt Ahrens and Marco Maggesi -- 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/ddefa71a-42c0-4abf-8b73-8f2a980f948d%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 3401 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1028 bytes --] Dear friends and colleagues, The next Peripatetic Seminar on Sheaves and Logic (PSSL 106) will be held on the weekend of April 4th--5th at the School of Mathematics, University of Leeds (UK). There is no conference fee. However for practical reasons, we kindly ask all participants to register by March 20th. The registration form and further information is available on the website: http://www1.maths.leeds.ac.uk/~pmtsh/pssl106.html If you have any questions, please email pssl106@leeds.ac.uk to contact the organisers. With best regards, Nicola Gambino Sina Hazratpour Gabriele Lobbia Karol Szumiło -- 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/ffbc4432-0008-4360-bf8b-f5c5f05e8946%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1751 bytes --]

We have a summer full of HoTT events ahead of us! I just want to remind people that we have a wiki where we can collect such (and other) information. https://ncatlab.org/homotopytypetheory/show/Events -- 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/CAOoPQuSeYFZ5nCX%2BCSTbGCcrFj0wMX0GRnYEQDc_iiroMWiYqQ%40mail.gmail.com.

The International Congress on Mathematical Software 2020 (ICMS 2020) will be held in Braunschweig, Germany on July 13-16, 2020: http://www.iaa.tu-bs.de/AppliedAlgebra/ICMS2020/ICMS2020.html There will be a session on "Univalent Mathematics: Theory and Implementation" at this event: https://univalent-math.github.io/ Title and short abstract submission deadline: February 23, 2020. # Aim and scope of session Homotopy Type Theory/Univalent Foundations (HoTT/UF) is a new type-theoretic foundation for mathematics based on novel connections between dependent type theory and homotopy theory. Recently there has been much interest in the constructive meaning of the univalence axiom, which has led to multiple new cubical proof assistants natively supporting univalence and higher inductive types. These proof assistants allow for the convenient formalization of abstract mathematics, especially synthetic homotopy theory, and also provide several features previously missing from many type-theoretic proof assistants, such as function extensionality and quotients. The goal of this session is to gather experts on HoTT/UF and its implementation to present recent results and discuss future directions, including but not limited to: o Implementation of proof assistants for univalent mathematics o Cubical type theories and their metatheory o Formalization of univalent mathematics # Submissions Most talks at the session will be invited, but there is room for a few contributed talks. If you would like to speak at the session please send us an email with title and a short plain text abstract by February 23, 2020. If accepted, you will have the option to submit an extended abstract (4-8 pages) by March 16, 2020. The accepted extended abstracts will then be published in the Springer Lecture Notes in Computer Science (LNCS) series. # Deadlines * Title and short abstract deadline (strict): February 23, 2020. * Notification: February 24, 2020. * Extended abstract deadline (optional): March 16, 2020. * Notification: April 27, 2020. * Final version of accepted extended abstracts: May 9, 2020. # Session organizers * Carlo Angiuli (Carnegie Mellon University) - cangiuli@cs.cmu.edu * Anders Mörtberg (Stockholm University) - anders.mortberg@math.su.se -- 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/CAMWCpp%3DT%2Bixw60EvtrHuAqLweARJzdc9HjAQBrw0%2Bx-5kPeSaw%40mail.gmail.com.

======== FINAL 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. INVITED SPEAKERS ======== Bartek Klin, University of Warsaw Christine Tasson, IRIF, Université de Paris 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 ======== Miriam Backens, University of Birmingham 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 Kohei Kishida, University of Illinois at Urbana-Champaign Martha Lewis, ILLC, University of Amsterdam Samuel Mimram, École Polytechnique Koko Muroya, RIMS, Kyoto University Jovana Obradović, Institute of Mathematics CAS Viktoriya Ozornova, Ruhr-Universität Bochum 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/CAJb9em3kq9eF78ZaCy%3DJcD%3DzLMLaiwmi_TZ-L9Z5CqgOEXwOog%40mail.gmail.com.

[-- Attachment #1.1: Type: text/plain, Size: 1979 bytes --] ==================================================================== Spring School on Theoretical Computer Science (EPIT) – Homotopy Type Theory Ile d’Oléron, CAES CNRS La vieille Perrotine, France. 25th-29th May 2020 https://epit2020cnrs.inria.fr ==================================================================== The EPIT is a French thematic school proposing, on an yearly basis, an intensive 5-day long training, specializing on a particular topic in theoretical computer science. It is primarily addressed to PhD students, Post-doctoral researchers and junior academics. The 2020 edition of the EPIT will be centered around Homotopy Type Theory, a research topic at the junction of Computer Science and Mathematics. Our hope is hence to provide an introduction that is accessible to researchers in both areas. Pre-registration is now open, please visit https://epit2020cnrs.inria.fr/registration/ to know more. For any question, please contact epit2020@sciencesconf.org NB: As the number of places is limited, we have fixed a deadline for pre-registration to ** March 15, 2020 **. -------------------------------------------------------------------- Lecturers Andrej Bauer (Ljubljana University): Introduction to Homotopy Type Theory Bas Spitters (Aarhus University): The Coq-HoTT library Andy Pitts (Cambridge University): Models of (Univalent) Type Theory Anders Mörtberg (Stockholm University): Cubical Type Theory Guillaume Brunerie (Stockholm University): Synthetic Homotopy Theory -- 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/221d36fb-a065-404f-9664-e474734713a6%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 7274 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 887 bytes --] Dear all, The ILLC is looking for an excellent PhD candidate who is interested in conducting research in an area within the ILLC that fits naturally in the Faculty of Science. The add can be found here: http://www.illc.uva.nl/NewsandEvents/News/Positions/newsitem/11506/PhD-candidate-Logic-Language-and-Computation Candidates who are interested in category theory and (homotopy) type theory should feel free to contact me before applying. Deadline: 17 February 2020. Best wishes, Benno -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8de729a0-d7ee-459a-8e49-ee845e1711cb%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1809 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3131 bytes --] Hello all, The results which I've talked about in Herrsching in December are now on the arXiv: https://arxiv.org/abs/2001.07655 In this work, Jakob von Raumer and I address the following problem: Consider paths in a given graph. If we want to prove a certain property for all paths, the obvious approach is to try induction on [the length of] a path. If we want to prove a certain property for all *closed* paths (first vertex = last vertex), this does not work since closed paths are not inductively generated (if we remove an edge from a closed path, it is not closed any more). We have studied this situation because certain coherence properties in HoTT can be formulated in terms of cycles. Our primary example is the following. Let's say we have a type A and a family (<) : A -> A -> Type (a "binary proof-relevant relation"). For a 1-type B, a function from the set-truncated quotient A/< to B is given by: (1) f : A -> B (2) h : Pi(x,y:A). x<y -> f(x) = f(y) (3) c : the property that h maps every closed zig-zag in A to reflexivity in B. (A closed zig-zag is a closed path in the graph generated by the symmetric closure of <). In those examples that we were interested in, we found that property (3) is very difficult to check (or we simply didn't manage to at all) because of the problem explained in the first paragraph, although we know that (3) can't be false. Not yet quite an instance, but close to being one, is the situation Mike described with "the [...] universe certainly is fully coherent" in https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/ Our paper builds on the observation that, at least in all those cases we were interested in, the relation < has additional and so far unused properties: First, it is locally confluent (in the constructive sense: every span can be completed to the obvious shape); Second, it is (co-) well-founded. (These assumptions are natural if the relation is encoding some reduction.) We construct a new relation on the type of closed zig-zags with the property that this new relation is again (co-) well-founded. The consequence is, in a nutshell, that every closed zig-zag can be expressed as a combination of shapes given by local confluence. The application is this: If we want to prove a property such as (3), for all closed zig-zags, it is enough to check the property for the zig-zag generated by a span with local confluence. And that is possible (and fairly easy), simply because we know how the "confluence zig-zags" will look like. An application-of-the-application is the statement that the fundamental groups of the free higher group over a set are trivial, and related results. As always, any comments are welcome! Nicolai -- 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/CA%2BAZBBokxk5mHf%2BuQ0OeEbLEm0Xuk1WKiFK77mxnBbcp_FBX4A%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3762 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 526 bytes --] I'd like to advertise this: https://homotopytypetheory.org/2020/01/26/the-cantor-schroder-bernstein-theorem-for-%e2%88%9e-groupoids/ -- 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/80a2bd2d-791c-4546-8199-32fe7bd0d38c%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 844 bytes --]

[-- Attachment #1: Type: text/plain, Size: 6438 bytes --] The following announcement may be of interest to some readers of this list. regards, Noam ---------- Forwarded message --------- From: Sadrzadeh, Mehrnoosh <m.sadrzadeh@ucl.ac.uk> Date: Fri, 24 Jan 2020 at 08:07 Subject: [TYPES/announce] Call for Nominations: E. W. Beth Outstanding Dissertation Prize 2020 To: mol@cs.earlham.edu <mol@cs.earlham.edu>, folli@folli.info < folli@folli.info>, ProofTheory@lists.bath.ac.uk < ProofTheory@lists.bath.ac.uk>, categories@mta.ca <categories@mta.ca>, types-announce@lists.seas.upenn.edu <types-announce@lists.seas.upenn.edu>, elsnet-list@list.hum.uu.nl <elsnet-list@vz07-list.im.hum.uu.nl>, nordlingnet@uib.no <nordlingnet@uib.no>, ln@groupes.renater.fr < ln@groupes.renater.fr> [ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Nominations: E. W. Beth Outstanding Dissertation Prize 2020 Since 2002, the Association for Logic, Language, and Information (FoLLI) has been awarding the annual E.W. Beth Dissertation Prize to outstanding Ph.D. dissertations in Logic, Language, and Information ( http://www.folli.info/?page_id=74), with financial support of the E.W. Beth Foundation ( https://www.knaw.nl/en/awards/funds/evert-willem-beth-stichting/evert-willem-beth-foundation). Nominations are now invited for the best dissertation in these areas resulting in a Ph.D. degree awarded in 2019. The deadline for nominations is the 15th of April 2020. Qualifications: - A dissertation is eligible for the Beth Dissertation Prize 2020, if the Ph.D. degree has been awarded in Logic, Language, or Information between January 1st and December 31st, 2019. - There are no restrictions on the nationality, ethnicity, age, gender or employment status of the author of the nominated dissertation, nor on the university, academic department or scientific institution formally conferring the Ph.D. degree, nor on the language in which the dissertation has originally been written. - In accordance with the aim of the Beth Foundation to continue and extend the work of the Dutch logician Evert Willem Beth, nominations are invited of excellent dissertations on current topics in philosophical and mathematical logic, computer science logic, philosophy of science, philosophy of language, history of logic, history of the philosophy of science and scientific philosophy in general, as well as the current theoretical and foundational developments in information and computation, language and cognition. Dissertations with results more broadly impacting various research areas in their interdisciplinary investigations are especially solicited. - If a nominated dissertation has originally been written in a language other than English, its dossier should still contain the required 10 page English abstract, see below. If the committee decides that a nominated dissertation in a language other than English requires translation to English for proper evaluation, the committee can transfer its nomination to the competition in 2021. The English translation must in such cases be submitted before the deadline of the call for nominations in 2021. The committee may recommend the Beth Foundation to consider supporting such nominated dissertations for English translation, upon request by the author of the dissertation. The prize consists of: - a certificate - a donation of 3000 euros, provided by the E.W. Beth Foundation - an invitation to submit the dissertation, possibly after revision, for publication in FoLLI Publications on Logic, Language and Information (Springer). Only digital submissions are accepted, without exception. Hard copy submissions are not allowed. The following documents are to be submitted in the nomination dossier: - The original dissertation in pdf format (ps/doc/rtf etc. not acceptable). - A ten-page English abstract of the dissertation, presenting the main results of each chapter. - A letter of nomination from the dissertation supervisor, which concisely describes the scope and significance of the dissertation, stating when the degree was officially awarded and the members of the Ph.D. committee. Nominations should contain the address, phone and email details of the nominator. - Two additional letters of support, including at least one from a referee not affiliated with the academic institution that awarded the Ph.D. degree, nor otherwise related to the nominee (e.g. former teachers, supervisors, co-authors, publishers or relatives) or the dissertation. - Self-nominations are not possible. All pdf documents must be submitted electronically, as one zip file, via EasyChair by following the link https://easychair.org/conferences/?conf=bdp2020. In case of any problems with the submission one should contact the chair of the committee Mehrnoosh Sadrzadeh (m.sadrzadeh@ucl.ac.uk). The prize will be awarded by the chair of the FoLLI board at a ceremony during the 32nd ESSLLI summer school in University of Utrecht, August 3-14, 2020. Beth dissertation prize committee 2020: Maria Aloni (University of Amsterdam) Alexander Clark(Kings College London) Cleo Condoravdi (Stanford University) Robin Cooper (University of Gothenburg) Guy Emerson (University of Cambridge) Katrin Erk (University of Texas at Austin) Arash Eshghi (Hariot-Watt University) Sujata Ghosh (ISI, Chennai) Davide Grossi (University of Groningen and University of Amsterdam) Chris Haase (University College London) Aurelie Herbelot (University of Trento) Louise McNally (Universitat Pompeu Fabra Barcelona) Reinhard Muskens (University of Amsterdam) Laura Rimmell (Deep Mind) Mehrnoosh Sadrzadeh (University College London, chair) Mark Steedman (University of Edinburgh) Matthew Stone (Rutgers) Jouko Väänänen (University of Helsinki) Noam Zeilberger (Ecole Polytechnique) -- 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/CAPYuNkBA9w75i4YCYkr%3DO440jY2kU8UxkfENT1RXyBNteFqBaA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 18043 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1911 bytes --] Dear all, A memorial conference for Erik Palmgren will take place on Thu/Fri 7–8 May 2020 (plus excursion on Sat 9), at Stockholm University: http://logic.math.su.se/palmgren-memorial/ Topics may include all Erik’s academic interests: type theory and its models, categorical logic and foundations, constructive mathematics and proof theory, nonstandard analysis, and the philosophy of constructive mathematics. Invited speakers (confirmed): • Douglas Bridges • Jacopo Emmenegger • Christian Espíndola • Håkon Gylterud • Hajime Ishihara • Millie Maietti • Ieke Moerdijk • Peter Schuster There is some space for contributed talks. If you would like to speak, please send a title and abstract to <palmgren-memorial@math.su.se> by Friday February 28. Contributions are especially encouraged from those who knew and worked with Erik. Registration is free; please email <palmgren-memorial@math.su.se> by Friday 3 April if you plan to attend. Some travel funding is available for early-career participants. To apply, please let us know in your registration email by Friday February 28. The conference is organized by Erik’s students and colleagues at Stockholm University: • Guillaume Brunerie • Menno de Boer • Henrik Forssell • Peter LeFanu Lumsdaine • Johan Lindberg • Per Martin-Löf • Anna Montaruli • Anders Mörtberg Please feel free to redistribute this announcement. Best wishes, –Peter. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-nM%2BP2N6TZHqD%3DLNFao59OZVzAoJ%3DpCoPM24xt85y%3DEjg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2785 bytes --]