[-- Attachment #1.1: Type: text/plain, Size: 6533 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. # IMPORTANT DATES All deadlines are 23:59 Anywhere on Earth Submission Deadline: Monday 4th November 2019 Author Notification: Monday 18th November 2019 Registration deadline: Monday 9th December 2019 Symposium dates: Monday 16th and Tuesday 17th December 2019 # Programme Committee Fatimah Ahmadi, University of Oxford Miriam Backens, University of Birmingham Nicols Behr, Institut de Recherche en Informatique Fondamentale (IRIF), Université 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/f23d9edc-bab5-42e0-97ef-05cca0b908dc%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 8270 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 455 bytes --] There is any connection between Floer homotopy theory and Hott -- 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/6450b566-3328-494f-8f57-c6e8af385d89%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 890 bytes --]

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

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

Dear All, I would like to invite applications for a fully-funded PhD position in the School of Computer Science at the University of Birmingham, UK. The PhD student will work me on topics related to categorical semantics of programming languages and computer theorem proving. Students broadly interested in these fields of research are strongly encouraged to apply. Topics of particular interest are: * Syntax and semantics of type theory * Formalisation of mathematics in univalent foundations * Directed type theory * Algebraic specification of programming languages Applicants should hold, or be about to obtain, a Masters or Bachelor degree in Computer Science or Mathematics. The PhD position is fully funded, covering tuition fees and a tax-free scholarship. Healthcare is provided for free. Please, do not hesitate to contact me by email for further details: b.ahrens@cs.bham.ac.uk In addition, feel free to browse my webpage for more information on my research interests: https://benediktahrens.net The theory group at Birmingham's School of Computer Science is very active, organising regular seminars and informal meetings. Many relevant international events frequently take place in Birmingham such as YaMCATS category theory seminar, Midlands Graduate School, and Workshops on Univalent Mathematics. For more information see http://www.cs.bham.ac.uk/research/groupings/theory/. Information on how to apply is given on http://www.cs.bham.ac.uk/admissions/postgraduate-research/. However, interested candidates are strongly encouraged to contact me in the first instance. Benedikt Ahrens -- 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/d5dff735-4e3a-1f3d-6ca4-93dc052ea786%40gmail.com.

In the 1-category case, Kripke-Joyal is a specific formulation of the internal language of a 1-topos (or more general 1-category), involving a forcing relation relating objects of the topos to formulas in its internal logic. The existing work on internal languages for higher categories, including all of the links provided by Ali, is not actually Kripke-Joyal style but is a categorification of a different approach to internal languages that directly constructs objects corresponding to each formula, the connection being that the forcing relation is a representable functor and the interpretation objects are what represent it. I understood the question to be whether, in contrast to all of this existing work, there is also a Kripke-Joyal-style approach to internal languages of higher categories. I expect that probably there is, but I don't think such a thing has been written down yet, although I hear that Awodey and Gambino have been thinking about it. But my instinct is that a Kripke-Joyal approach wouldn't make the coherence questions any easier, since it's basically just a translation through the Yoneda lemma; any coherence technique that can be used for one version should also work for the other. On Tue, Oct 8, 2019 at 9:36 AM Ali Caglayan <alizter@gmail.com> wrote: > > Hi Alexander, > > I think what you are asking is "what is the internal language of an oo-topos". This is doesn't really make much sense as stated since we don't have a definition for "internal language" in an oo-topos. But we expect that once we can define such a notion, then it ought to be HoTT. This will require further work, but recently there have been some big strides towards this direction with Mike Shulman's work. > > The Kripke-Joyal semantics of a topos of sheaves is essentially a dictionary between the "internal language" of this 1-topos and what it means externally. I have quotation marks here because I am not being very precise and phrases like "internal language" do have precise meanings which I don't care to look up right now. > > You are correct that these have been used in practice. Just look at Ingo Blechschmidt's work. He discusses on pg. 199 briefly the thing that you consider. > > The thing to note with Mike's work is theorem 11.1, which shows that every oo-topos can be presented by a "type-theoretic model topos". Now you can think of Kripke-Joyal semantics as a "machine" that can translate between internal and external statements. Here is a page on the nlab that shows what this will probably end up looking like. > > To get an idea what such a machine might do, have a look at Charles Rezk's "translation" of a HoTT proof of Blakers-Massey into higher topos theory. The key point here is that this proof was not known in higher topos theory before. It is a very natural argument in HoTT however. I would say this is pretty fruitful. > > The reason I keep saying "probably" is because nobody has actually formally written down these semantics that I know of. Kripke-Joyal semantics are fairly technical already, just look at Ingo's thesis. And you are correct that with HoTT there are lot's of subtleties involved. > > So to answer you final question: yes it is being investigated and yes it seems to be fruitful. > > I will add however that apart from Ingo's work, I don't know of many people using Kripke-Joyal semantics to actually do algebraic geometry. It's true that Ingo discovered some new arguments (generic freeness) but these have yet to catch on with "regular" algebraic geometers. This is because even though it is a 200 page thesis, it only covers foundational aspects of the subject, i.e. the basics of scheme theory. There is much more work to be done before it gets mainstream. > > We will probably see algebraic topologists using the internal language of (oo-)toposes well before algebraic geometers do. Since we already have examples of these almost being done. > > These are just my thoughts on your question and is no means the word of an expert. > > Best, > Ali Caglayan > > > On Tue, Oct 8, 2019 at 4:07 PM Alexander Gietelink Oldenziel <a.f.d.a.gietelinkoldenziel@gmail.com> wrote: >> >> Dear all, >> >> It is my understanding that the interpretation of HoTT inside higher topoi is an ongoing field of research. Much of this business involves subtle strictness properties and things like contextual and syntactic categories. >> In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These semantics are easy to use in practice. Naively, it seems one could lift the Kripke-Joyal semantics by not asking for truth but simply an inhabitant of a type. >> >> Has this been investigated at all? Is it ultimately fruitless? >> >> -- >> 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/1b613bab-505c-4880-9778-4e3206872294%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/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpypzzDa0J8pPT1eYnZV1qUaQ%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/CAOvivQzEpWEtHZvNKPJxBnYPBxh2XhKB4jobVT0BZmn%3DvP42QQ%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 4563 bytes --] Hi Alexander, I think what you are asking is "what is the internal language of an oo-topos". This is doesn't really make much sense as stated since we don't have a definition for "internal language" in an oo-topos. But we expect that once we can define such a notion, then it ought to be HoTT. This will require further work, but recently there have been some big strides towards this direction with Mike Shulman's work <https://arxiv.org/abs/1904.07004>. The Kripke-Joyal semantics of a topos of sheaves is essentially a dictionary between the "internal language" of this 1-topos and what it means externally. I have quotation marks here because I am not being very precise and phrases like "internal language" do have precise meanings which I don't care to look up right now. You are correct that these have been used in practice. Just look at Ingo Blechschmidt's work <https://rawgit.com/iblech/internal-methods/master/notes.pdf>. He discusses on pg. 199 briefly the thing that you consider. The thing to note with Mike's work is theorem 11.1, which shows that every oo-topos can be presented by a "type-theoretic model topos". Now you can think of Kripke-Joyal semantics as a "machine" that can translate between internal and external statements. Here is a page on the nlab <https://ncatlab.org/nlab/show/HoTT+methods+for+homotopy+theorists> that shows what this will probably end up looking like. To get an idea what such a machine might do, have a look at Charles Rezk's "translation" <https://faculty.math.illinois.edu/~rezk/freudenthal-and-blakers-massey.pdf> of a HoTT proof of Blakers-Massey into higher topos theory. The key point here is that this proof was not known in higher topos theory before. It is a very natural argument in HoTT however. I would say this is pretty fruitful. The reason I keep saying "probably" is because nobody has actually formally written down these semantics that I know of. Kripke-Joyal semantics are fairly technical already, just look at Ingo's thesis. And you are correct that with HoTT there are lot's of subtleties involved. So to answer you final question: yes it is being investigated and yes it seems to be fruitful. I will add however that apart from Ingo's work, I don't know of many people using Kripke-Joyal semantics to actually do algebraic geometry. It's true that Ingo discovered some new arguments (generic freeness) but these have yet to catch on with "regular" algebraic geometers. This is because even though it is a 200 page thesis, it only covers foundational aspects of the subject, i.e. the basics of scheme theory. There is much more work to be done before it gets mainstream. We will probably see algebraic topologists using the internal language of (oo-)toposes well before algebraic geometers do. Since we already have examples of these almost being done. These are just my thoughts on your question and is no means the word of an expert. Best, Ali Caglayan On Tue, Oct 8, 2019 at 4:07 PM Alexander Gietelink Oldenziel < a.f.d.a.gietelinkoldenziel@gmail.com> wrote: > Dear all, > > It is my understanding that the interpretation of HoTT inside higher topoi > is an ongoing field of research. Much of this business involves subtle > strictness properties and things like contextual and syntactic categories. > In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These > semantics are easy to use in practice. Naively, it seems one could lift > the Kripke-Joyal semantics by not asking for truth but simply an inhabitant > of a type. > > Has this been investigated at all? Is it ultimately fruitless? > > -- > 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/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%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/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpypzzDa0J8pPT1eYnZV1qUaQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5864 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 926 bytes --] Dear all, It is my understanding that the interpretation of HoTT inside higher topoi is an ongoing field of research. Much of this business involves subtle strictness properties and things like contextual and syntactic categories. In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These semantics are easy to use in practice. Naively, it seems one could lift the Kripke-Joyal semantics by not asking for truth but simply an inhabitant of a type. Has this been investigated at all? Is it ultimately fruitless? -- 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/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1281 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1453 bytes --] I expect many readers of this list would be qualified or know qualified researchers. Thanks! —Amr Job Title: Assistant Professor in Computer Science (Quantum Information) Apply at: https://indiana.peopleadmin.com/postings/8506 <https://indiana.peopleadmin.com/postings/8506> Contact: Amr Sabry (sabry@indiana.edu <mailto:sabry@indiana.edu>) The School of Informatics, Computing, and Engineering (SICE) at Indiana University (IU) Bloomington invites applications for a tenure-track assistant professor position in quantum information to begin in Fall 2020. Duties will include research, teaching, and service. Candidates with research interests in formal models of computation, algorithms, and information theory, preferably with connection to quantum computation, quantum simulation, or quantum information science, are encouraged to apply. This position is part of an initiative for significant growth in these areas through the IU Center for Quantum Information Science and Engineering, bringing together researchers from multiple disciplines. -- 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/0A1B33C2-E05F-428B-A4B0-ACE5F2DB7C6D%40gmail.com. [-- Attachment #2: Type: text/html, Size: 3416 bytes --]

[-- Attachment #1: Type: text/plain, Size: 958 bytes --] Friends, The Department of Philosophy at Carnegie Mellon University is looking to hire a mathematical logician at the assistant professor level. Note that HoTT is included among the possible areas of specialization. Interfolio: https://apply.interfolio.com/69329 <https://apply.interfolio.com/69329> MathJobs: https://www.mathjobs.org/jobs/jobs/14697 <https://www.mathjobs.org/jobs/jobs/14697> PhilJobs: https://philjobs.org/job/show/13806 <https://philjobs.org/job/show/13806> Please share this information with anyone who may be interested. Best wishes, Steve -- 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/038DEE27-9A75-459B-938A-ED14B51CF6BB%40cmu.edu. [-- Attachment #2: Type: text/html, Size: 2533 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3490 bytes --] *The Department of Computer Science at Aarhus University, Denmark, offers a considerable number of PhD and PostDoc positions in the areas of Logic, Semantics and Programming Languages. Our research spans a wide spectrum of topics concerning models and logics for programming languages and type theories, language-based security, blockchains, theoretical foundations and practical tools for program analysis, formal verification and model checking.* *Aarhus University admits PhD students on the basis of a bachelor's degree (for 5 year PhDs) or a master's degree (for 3 year PhDs). If admitted, all tuition is covered, and a generous stipend is provided <https://phd.scitech.au.dk/for-applicants/phd-study-structure-and-income/>. Postdoc positions can be for 1 or 2 years, and with the possibility of renewal (depending on the individual projects and sources of funding). Interested applicants at all levels are encouraged to contact the respective faculty for details, enclosing a CV and a short description of interests.Logic and Semantics group: http://cs.au.dk/research/logic-and-semantics/ <http://cs.au.dk/research/logic-and-semantics/>Aslan Askarov <http://askarov.net/> (language-based security, web security, type systems, program analysis)Lars Birkedal <https://cs.au.dk/~birke/> (higher-order concurrent separation logic <http://iris-project.org>, type theory <http://cs.au.dk/~birke/ghott/index.html>, program verification)Bas Spitters <http://users-cs.au.dk/spitters/> (computer aided proofs in cryptography, homotopy type theory, formal verification of blockchains <http://cs.au.dk/research/centers/concordium/>)Jaco van de Pol <https://www.cs.au.dk/~jaco/> (parallel & symbolic model checking, synthesis, graph games)Programming Languages group: https://cs.au.dk/research/programming-languages/ <https://cs.au.dk/research/programming-languages/>Magnus Madsen <http://cs.au.dk/~magnusm/> (programming language design, functional and logic programming, type systems)Anders Møller <https://cs.au.dk/~amoeller/> (static & dynamic program analysis, program analysis and automated testing for web and mobile software)Andreas Pavlogiannis <https://tildeweb.au.dk/au648021/> (algorithmic & computational foundations of model checking, quantitative verification, static & dynamic analysis, concurrency)Aarhus University is realizing an ambitious multi-phase digitalization initiative <https://newsroom.au.dk/en/news/show/artikel/aarhus-universitet-lancerer-ambitioes-digital-satsning/> which will help prepare researchers, students and the labour force for the digital transition of the future. The initiative aims at significant expansion <http://cs.au.dk/news-events/news/show-news/artikel/exciting-expansion-plans-for-computer-science-at-aarhus-university/> of the Department of Computer Science for faculty and students.Next deadline: November 1st, 2019Information about the PhD program: http://phd.scitech.au.dk/for-applicants/application-guide/ <http://phd.scitech.au.dk/for-applicants/application-guide/>* -- 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/CAOoPQuTYceMKNrymyWeyg%2B6aV99HaEPZ9dJiGrraVv0PPcnq-w%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 14466 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1714 bytes --] Dear all, We are pleased to announce the third Midwest Homotopy Type Theory Seminar, to take place on October 19-20, 2019 at the University of Michigan (Ann Arbor). The meeting will feature talks by: Kuen-Bang Hou (Favonia) University of Minnesota Nullable Compositions Chris Kapulkin University of Western Ontario Homotopy Canonicity of Homotopy Type Theory Paige North Ohio State University Two-sided Weak Factorization Systems with pre-talks given by: Deshin Finlay (University of Michigan) Scott Newton (Ohio State University) Robert Rose (Indiana University) with topical question/discussion ("ask-me-anything") sessions led by: Andreas Blass University of Michigan on topos theory Dan Christensen University of Western Ontario on homotopy theory Amr Sabry Indiana University on programming languages Please visit http://math.lsa.umich.edu/~simoncho/mwhottseminar.html for further details including the schedule and travel information. In particular, please note that the preferred rate we have negotiated with the nearby hotel is valid until September 27. There is no registration fee, but we request that those planning to attend fill out the very short registration form on the website for our planning purposes (e.g. getting enough coffee for everyone). Best, Simon Cho 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/3e63cc6d-6c8c-45a7-9927-cb22c9a9d60d%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2255 bytes --]

Hello all, I thought I'd let the readers of this list know that since a few years ago the NSF postdocs can be held in Canada. This is an excellent opportunity for American citizens/permanent residents that are about to finish their Ph.D. and happen to know a university in Canada with an active homotopy type theory group (wink, wink). For details, see https://www.nsf.gov/funding/pgm_summ.jsp?pims_id=5301&org=NSF The application deadline is October 16, 2019. Best, Chris -- 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/CAEXhy3N0rBi6cnmxrLFD3qv_j13dBCfH3VCKdzgQ_cT0481u%2Bw%40mail.gmail.com.

All variations of CCHM that I know suffer from the same issue as ABCFHL for the reasons explained by Dan and Evan. Just as in the cartesian setting fst(coe(ua(e))) reduces to fst(e) composed with some "morally-the-identity-compositions" that don't disappear automatically. For example, in Cubical Agda fst(coe(ua(e))) reduces to fst(e) composed with a coe in a constant family that we have to take care of manually (we write transport for coe): https://github.com/agda/cubical/blob/master/Cubical/Foundations/Univalence.agda#L149 In my experience this is rarely a problem in practice though. It's a bit annoying to insert these corrections manually in proofs, but it happens quite rarely and when doing concrete computations with closed types they disappear automatically. One difference I've noticed when doing synthetic homotopy theory in cubical type theory compared to HoTT is that we use equalities and univalence a lot more. The fact that we sometimes need to insert these correction terms is largely compensated by all of the useful primitives of cubical type theory that we have for working with equalities that are not available for equivalences (path abstraction/application, composition...). -- Anders On Wed, Sep 18, 2019 at 10:36 PM Evan Cavallo <evancavallo@gmail.com> wrote: > > The definition of univalence for BCH cubical sets in https://arxiv.org/abs/1710.10941 does satisfy the property that fst(coe(ua(e))) = fst(e) : A -> B exactly. They note (Remark 7) that the definition can also be adjusted so that transporting backwards along the equivalence gives the inverse function one can extract from e. > > Roughly, the problem Dan describes in ABCFHL---that the B in Glue [alpha -> T] B can also depend on the direction of coercion x---can be avoided in the BCH analogue of Glue by simply demanding that B is degenerate in x. The restricted operation is still sufficient to prove univalence. We can't make sense of this in a structural cubical set model because the property of being degenerate in a given variable isn't stable under diagonal substitution. > > Evan > > 2019年9月18日(水) 15:23 Michael Shulman <shulman@sandiego.edu>: >> >> Thanks, that's very interesting! >> >> The reason I ask is that I was wondering to what extent the type "A=B" >> can be regarded as "a coherent definition of equivalence" alongside >> half-adjoint equivalences, maps with contractible fibers, etc. Of >> course in some sense it is (even in Book HoTT), since it's equivalent >> to Equiv(A,B); but the question is how practical it is -- for >> instance, is it reasonable when doing synthetic homotopy theory to >> state all equivalences as equalities? >> >> In practice, the way we often construct equivalences is to make them >> out of a quasi-inverse pair, and all the standard definitions of >> equivalence have the nice property that they remember the two >> functions in the quasi-inverse pair judgmentally. My experience with >> the HoTT/Coq library is that this property is very useful, which is >> one reason we state equivalences as equivalences rather than making >> use of univalence to state them as equalities (another reason is that >> it avoids "univalence-redexes" all over the theory). Half-adjoint >> equivalences have the additional nice property that they remember one >> of the homotopies judgmentally, and if you're willing to prove the >> coherence 2-path by hand then they can be made to remember both of the >> homotopies; this seems to be much less useful than I thought it would >> be when we made the choice to use half-adjoint equivalences in the >> HoTT/Coq library, but it has proven useful at least once. >> >> So I was wondering to what extent equality of types in cubical type >> theory has properties like this. It sounds from what you say like the >> answer is "not much". This makes the lack of regularity seem like a >> rather more serious problem than I had previously thought. >> >> On Wed, Sep 18, 2019 at 9:15 AM Licata, Dan <dlicata@wesleyan.edu> wrote: >> > >> > In ABCFHL, even the function fst(coe(ua(e))) : A -> B is only path-equal to fst(e) : A -> B. If I recall correctly, the issue is that composition in the Glue type that you use to implement ua doesn’t judgementally give you f; instead there is some morally-the-identity-composition (that would cancel with regularity) that gets stuck in. This is because the general algorithm for composition in the glue type has to coerce in the “base” of the glue type (B in Glue [alpha -> T] B), which in the case of ua(e) = Glue [x = 0 -> (A,e), x=1 -> (B,id)] B is degenerate in x, but in general might not be. >> > >> > I don’t recall any cubical type theories solving this, but I don’t remember the details of all of the other variations that have been explored well enough to say for sure. >> > >> > > On Sep 18, 2019, at 11:42 AM, Michael Shulman <shulman@sandiego.edu> wrote: >> > > >> > > Let Equiv(A,B) denote the type of half-adjoint equivalences, so that >> > > an e:Equiv(A,B) consists of five data: a function A -> B, a function B >> > > -> A, two homotopies, and a coherence 2-path. Using univalence, we >> > > can make e into an identification ua(e) : A=B, and then back into an >> > > equivalence coe(ua(e)) : Equiv(A,B), which is typally equal to e. >> > > >> > > Now we might wonder whether coe(ua(e)) might be in fact *judgmentally* >> > > equal to e; or at least whether this might be true of some, if not >> > > all, of its five components. In Book HoTT this is clearly not the >> > > case, since univalence is posited as an axiom about which we know >> > > nothing else. But what about cubical type theories? Can any of the >> > > components of an equivalence e be recovered, up to judgmental >> > > equality, from coe(ua(e))? (My guess would be that at least the >> > > function A -> B, and probably also the function B -> A, can be >> > > recovered, but perhaps not more.) >> > > >> > > -- >> > > 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/CAOvivQzzSXNHs%2BzbPQTyHEuU53aHXJ0sPe4pr%2Byf0ahLGvUpVA%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/1DF8E802-2959-4BEF-A85A-3C6E5E7B9595%40wesleyan.edu. >> >> -- >> 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/CAOvivQz_wY2CVp9Y5caEehVotR7w7D%3DoP6jpoUxm463pNdNHuA%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/CAFcn59ZLBcQMwJUMnnDKq3ewf582x4z4aqce4xR16xzcQeRxgA%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/CAMWCppk7Dz6EEsf0R7pQhS9z2Y11jTMAhxo674G4%2BqEUqssM9A%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 6392 bytes --] The definition of univalence for BCH cubical sets in https://arxiv.org/abs/1710.10941 does satisfy the property that fst(coe(ua(e))) = fst(e) : A -> B exactly. They note (Remark 7) that the definition can also be adjusted so that transporting backwards along the equivalence gives the inverse function one can extract from e. Roughly, the problem Dan describes in ABCFHL---that the B in Glue [alpha -> T] B can also depend on the direction of coercion x---can be avoided in the BCH analogue of Glue by simply demanding that B is degenerate in x. The restricted operation is still sufficient to prove univalence. We can't make sense of this in a structural cubical set model because the property of being degenerate in a given variable isn't stable under diagonal substitution. Evan 2019年9月18日(水) 15:23 Michael Shulman <shulman@sandiego.edu>: > Thanks, that's very interesting! > > The reason I ask is that I was wondering to what extent the type "A=B" > can be regarded as "a coherent definition of equivalence" alongside > half-adjoint equivalences, maps with contractible fibers, etc. Of > course in some sense it is (even in Book HoTT), since it's equivalent > to Equiv(A,B); but the question is how practical it is -- for > instance, is it reasonable when doing synthetic homotopy theory to > state all equivalences as equalities? > > In practice, the way we often construct equivalences is to make them > out of a quasi-inverse pair, and all the standard definitions of > equivalence have the nice property that they remember the two > functions in the quasi-inverse pair judgmentally. My experience with > the HoTT/Coq library is that this property is very useful, which is > one reason we state equivalences as equivalences rather than making > use of univalence to state them as equalities (another reason is that > it avoids "univalence-redexes" all over the theory). Half-adjoint > equivalences have the additional nice property that they remember one > of the homotopies judgmentally, and if you're willing to prove the > coherence 2-path by hand then they can be made to remember both of the > homotopies; this seems to be much less useful than I thought it would > be when we made the choice to use half-adjoint equivalences in the > HoTT/Coq library, but it has proven useful at least once. > > So I was wondering to what extent equality of types in cubical type > theory has properties like this. It sounds from what you say like the > answer is "not much". This makes the lack of regularity seem like a > rather more serious problem than I had previously thought. > > On Wed, Sep 18, 2019 at 9:15 AM Licata, Dan <dlicata@wesleyan.edu> wrote: > > > > In ABCFHL, even the function fst(coe(ua(e))) : A -> B is only path-equal > to fst(e) : A -> B. If I recall correctly, the issue is that composition > in the Glue type that you use to implement ua doesn’t judgementally give > you f; instead there is some morally-the-identity-composition (that would > cancel with regularity) that gets stuck in. This is because the general > algorithm for composition in the glue type has to coerce in the “base” of > the glue type (B in Glue [alpha -> T] B), which in the case of ua(e) = Glue > [x = 0 -> (A,e), x=1 -> (B,id)] B is degenerate in x, but in general might > not be. > > > > I don’t recall any cubical type theories solving this, but I don’t > remember the details of all of the other variations that have been explored > well enough to say for sure. > > > > > On Sep 18, 2019, at 11:42 AM, Michael Shulman <shulman@sandiego.edu> > wrote: > > > > > > Let Equiv(A,B) denote the type of half-adjoint equivalences, so that > > > an e:Equiv(A,B) consists of five data: a function A -> B, a function B > > > -> A, two homotopies, and a coherence 2-path. Using univalence, we > > > can make e into an identification ua(e) : A=B, and then back into an > > > equivalence coe(ua(e)) : Equiv(A,B), which is typally equal to e. > > > > > > Now we might wonder whether coe(ua(e)) might be in fact *judgmentally* > > > equal to e; or at least whether this might be true of some, if not > > > all, of its five components. In Book HoTT this is clearly not the > > > case, since univalence is posited as an axiom about which we know > > > nothing else. But what about cubical type theories? Can any of the > > > components of an equivalence e be recovered, up to judgmental > > > equality, from coe(ua(e))? (My guess would be that at least the > > > function A -> B, and probably also the function B -> A, can be > > > recovered, but perhaps not more.) > > > > > > -- > > > 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/CAOvivQzzSXNHs%2BzbPQTyHEuU53aHXJ0sPe4pr%2Byf0ahLGvUpVA%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/1DF8E802-2959-4BEF-A85A-3C6E5E7B9595%40wesleyan.edu > . > > -- > 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/CAOvivQz_wY2CVp9Y5caEehVotR7w7D%3DoP6jpoUxm463pNdNHuA%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/CAFcn59ZLBcQMwJUMnnDKq3ewf582x4z4aqce4xR16xzcQeRxgA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 8303 bytes --]

Thanks, that's very interesting! The reason I ask is that I was wondering to what extent the type "A=B" can be regarded as "a coherent definition of equivalence" alongside half-adjoint equivalences, maps with contractible fibers, etc. Of course in some sense it is (even in Book HoTT), since it's equivalent to Equiv(A,B); but the question is how practical it is -- for instance, is it reasonable when doing synthetic homotopy theory to state all equivalences as equalities? In practice, the way we often construct equivalences is to make them out of a quasi-inverse pair, and all the standard definitions of equivalence have the nice property that they remember the two functions in the quasi-inverse pair judgmentally. My experience with the HoTT/Coq library is that this property is very useful, which is one reason we state equivalences as equivalences rather than making use of univalence to state them as equalities (another reason is that it avoids "univalence-redexes" all over the theory). Half-adjoint equivalences have the additional nice property that they remember one of the homotopies judgmentally, and if you're willing to prove the coherence 2-path by hand then they can be made to remember both of the homotopies; this seems to be much less useful than I thought it would be when we made the choice to use half-adjoint equivalences in the HoTT/Coq library, but it has proven useful at least once. So I was wondering to what extent equality of types in cubical type theory has properties like this. It sounds from what you say like the answer is "not much". This makes the lack of regularity seem like a rather more serious problem than I had previously thought. On Wed, Sep 18, 2019 at 9:15 AM Licata, Dan <dlicata@wesleyan.edu> wrote: > > In ABCFHL, even the function fst(coe(ua(e))) : A -> B is only path-equal to fst(e) : A -> B. If I recall correctly, the issue is that composition in the Glue type that you use to implement ua doesn’t judgementally give you f; instead there is some morally-the-identity-composition (that would cancel with regularity) that gets stuck in. This is because the general algorithm for composition in the glue type has to coerce in the “base” of the glue type (B in Glue [alpha -> T] B), which in the case of ua(e) = Glue [x = 0 -> (A,e), x=1 -> (B,id)] B is degenerate in x, but in general might not be. > > I don’t recall any cubical type theories solving this, but I don’t remember the details of all of the other variations that have been explored well enough to say for sure. > > > On Sep 18, 2019, at 11:42 AM, Michael Shulman <shulman@sandiego.edu> wrote: > > > > Let Equiv(A,B) denote the type of half-adjoint equivalences, so that > > an e:Equiv(A,B) consists of five data: a function A -> B, a function B > > -> A, two homotopies, and a coherence 2-path. Using univalence, we > > can make e into an identification ua(e) : A=B, and then back into an > > equivalence coe(ua(e)) : Equiv(A,B), which is typally equal to e. > > > > Now we might wonder whether coe(ua(e)) might be in fact *judgmentally* > > equal to e; or at least whether this might be true of some, if not > > all, of its five components. In Book HoTT this is clearly not the > > case, since univalence is posited as an axiom about which we know > > nothing else. But what about cubical type theories? Can any of the > > components of an equivalence e be recovered, up to judgmental > > equality, from coe(ua(e))? (My guess would be that at least the > > function A -> B, and probably also the function B -> A, can be > > recovered, but perhaps not more.) > > > > -- > > 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/CAOvivQzzSXNHs%2BzbPQTyHEuU53aHXJ0sPe4pr%2Byf0ahLGvUpVA%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/1DF8E802-2959-4BEF-A85A-3C6E5E7B9595%40wesleyan.edu. -- 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/CAOvivQz_wY2CVp9Y5caEehVotR7w7D%3DoP6jpoUxm463pNdNHuA%40mail.gmail.com.

What I find more interesting is that it's even *possible* to parametrize a definition of S^n with one n-loop by an internal n. It would be intriguing to try to find a schema or semantics for HITs that allow paths of arbitrary internally-specified dimensions, and see whether there are other examples that are more useful. The only other vaguely similar example that I know of is mentioned at the end of https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/ (and implemented in the HoTT/Coq library), a definition of localization that works in the absence of funext. On Wed, Sep 18, 2019 at 9:27 AM Licata, Dan <dlicata@wesleyan.edu> wrote: > > Thanks Anders. To be clear, I don’t think we have any schemas or semantics of HITs that accept this definition of S^n (with an n-loop for an internally-specified n) in any non-cubical settings either; at the time, I was thinking of it more as exploring what you can do with the definition. Proving the two definitions equivalent should be the same (modulo which definitional equalities you get) as implementing the one-n-loop rules in terms of suspensions, so that would be one way to justify these rules. > > Also, the proof of pi_n(S^n) = Z that Guillaume mentioned, which predated Freudenthal, is a lot more work than the one that you get from Freudenthal, so I’m not sure we have any motivating examples for why the one-n-loop definition is better than the suspension definition for arbitrary n. > > -Dan > > > On Sep 18, 2019, at 8:00 AM, Anders Mörtberg <andersmortberg@gmail.com> wrote: > > > > Let me elaborate a bit on my answer. One might naively try to copy Dan and Guillaume's definition and write the following in Cubical Agda: > > > > > > Omega : (A : Type₀) → A → Type₀ > > Omega A a = (a ≡ a) > > > > itOmega : ℕ → (A : Type₀) → A → Type₀ > > itOmega zero A a = Omega A a > > itOmega (suc n) A a = itOmega n (Omega A a) refl > > > > data Sn (n : ℕ) : Type₀ where > > base : Sn n > > surf : itOmega n (Sn n) base > > > > > > However Agda will complain as surf is not constructing an element of Sn. This might seem a bit funny as Cubical Agda is perfectly happy with > > > > > > data S³ : Type₀ where > > base : S³ > > surf : Path (Path (base ≡ base) refl refl) refl refl > > > > > > But what is happening under the hood is that surf is a constructor taking i, j, and k in the interval and returning an element of S^3 with boundary "base" whenever i, j and k are 0 or 1. In cubicaltt we can write this HIT in the following way: > > > > > > data S3 = base > > | surf <i j k> [ (i=0) -> base > > , (i=1) -> base > > , (j=0) -> base > > , (j=1) -> base > > , (k=0) -> base > > , (k=1) -> base ] > > > > > > The problem is then clearer: in order to write the surf constructor of Sn we would have to quantify over n interval variables and specify the boundary of the n-cell. This is what that is not supported by any of the cubical schemas for HITs. > > > > -- > > Anders > > > > On Wednesday, September 18, 2019 at 11:00:22 AM UTC+2, Guillaume Brunerie wrote: > > Hi, > > > > We give a definition of S^n with one point and one n-loop by > > introduction/elimination/reduction rules in our paper with Dan Licata > > (https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can be > > implemented in Agda (so Kristina’s question can be formulated and can > > presumably be formalized in Agda) but I don’t think we actually proved > > it. > > > > Best, > > Guillaume > > > > Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg <andersm...@gmail.com>: > > > > > > Hi Kristina, > > > > > > We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda: > > > https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda > > > > > > However, I don't think we can even write down the general version of > > > S^n as a type with a point and an n-loop with the schema implemented > > > in Cubical Agda. As far as I know no other schema for HITs support > > > this kind of types either. > > > > > > -- > > > Anders > > > > > > On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova > > > <sojakova...@gmail.com> wrote: > > > > > > > > Hello everybody, > > > > > > > > Is it worked out somewhere that the two definitions of Sn as a > > > > suspension on one hand and a HIT with a point and an n-loop on the other > > > > hand are equivalent? This is also an exercise in the book. I know > > > > Favonia has some Agda code on spheres but I couldn't find this result in > > > > there. > > > > > > > > Thanks, > > > > > > > > Kristina > > > > > > > > > > > > -- > > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/db712ad2-396f-4328-bb73-898dcb956834%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/DBF368F2-295C-4175-93F2-1EA01D49B95D%40wesleyan.edu. -- 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/CAOvivQy%2BUGKt3q8P8ed9N6E%2BjOUcjgQ49pxp0rBuDM%3DSoV-QbQ%40mail.gmail.com.

Thanks Anders. To be clear, I don’t think we have any schemas or semantics of HITs that accept this definition of S^n (with an n-loop for an internally-specified n) in any non-cubical settings either; at the time, I was thinking of it more as exploring what you can do with the definition. Proving the two definitions equivalent should be the same (modulo which definitional equalities you get) as implementing the one-n-loop rules in terms of suspensions, so that would be one way to justify these rules. Also, the proof of pi_n(S^n) = Z that Guillaume mentioned, which predated Freudenthal, is a lot more work than the one that you get from Freudenthal, so I’m not sure we have any motivating examples for why the one-n-loop definition is better than the suspension definition for arbitrary n. -Dan > On Sep 18, 2019, at 8:00 AM, Anders Mörtberg <andersmortberg@gmail.com> wrote: > > Let me elaborate a bit on my answer. One might naively try to copy Dan and Guillaume's definition and write the following in Cubical Agda: > > > Omega : (A : Type₀) → A → Type₀ > Omega A a = (a ≡ a) > > itOmega : ℕ → (A : Type₀) → A → Type₀ > itOmega zero A a = Omega A a > itOmega (suc n) A a = itOmega n (Omega A a) refl > > data Sn (n : ℕ) : Type₀ where > base : Sn n > surf : itOmega n (Sn n) base > > > However Agda will complain as surf is not constructing an element of Sn. This might seem a bit funny as Cubical Agda is perfectly happy with > > > data S³ : Type₀ where > base : S³ > surf : Path (Path (base ≡ base) refl refl) refl refl > > > But what is happening under the hood is that surf is a constructor taking i, j, and k in the interval and returning an element of S^3 with boundary "base" whenever i, j and k are 0 or 1. In cubicaltt we can write this HIT in the following way: > > > data S3 = base > | surf <i j k> [ (i=0) -> base > , (i=1) -> base > , (j=0) -> base > , (j=1) -> base > , (k=0) -> base > , (k=1) -> base ] > > > The problem is then clearer: in order to write the surf constructor of Sn we would have to quantify over n interval variables and specify the boundary of the n-cell. This is what that is not supported by any of the cubical schemas for HITs. > > -- > Anders > > On Wednesday, September 18, 2019 at 11:00:22 AM UTC+2, Guillaume Brunerie wrote: > Hi, > > We give a definition of S^n with one point and one n-loop by > introduction/elimination/reduction rules in our paper with Dan Licata > (https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can be > implemented in Agda (so Kristina’s question can be formulated and can > presumably be formalized in Agda) but I don’t think we actually proved > it. > > Best, > Guillaume > > Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg <andersm...@gmail.com>: > > > > Hi Kristina, > > > > We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda: > > https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda > > > > However, I don't think we can even write down the general version of > > S^n as a type with a point and an n-loop with the schema implemented > > in Cubical Agda. As far as I know no other schema for HITs support > > this kind of types either. > > > > -- > > Anders > > > > On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova > > <sojakova...@gmail.com> wrote: > > > > > > Hello everybody, > > > > > > Is it worked out somewhere that the two definitions of Sn as a > > > suspension on one hand and a HIT with a point and an n-loop on the other > > > hand are equivalent? This is also an exercise in the book. I know > > > Favonia has some Agda code on spheres but I couldn't find this result in > > > there. > > > > > > Thanks, > > > > > > Kristina > > > > > > > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/db712ad2-396f-4328-bb73-898dcb956834%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/DBF368F2-295C-4175-93F2-1EA01D49B95D%40wesleyan.edu.

[-- Attachment #1: Type: text/plain, Size: 1449 bytes --] Dear all, As a reminder, CT Octoberfest 2019 will be held at Johns Hopkins University, Baltimore on the 26th and 27th of October. The meeting is free and open to all. All details, including instructions on contributing a talk or ``registering'', and accommodation and travel recommendations, are available on the website: https://ct-octoberfest.github.io . In conjunction with Octoberfest we are pleased to announce a plenary talk, joint with the Johns Hopkins Category Theory seminar, at 17h00 on Friday the 26th of October: Mike Shulman will be talking on the theme of internal languages. Those wishing to speak should send an email to ctoctoberfest19@math.jhu.edu with the subject ``Submission'' including the submission title and any notes or special requests. The talk submission deadline is the 25th of September, anywhere on earth. For any queries related to the meeting please do not hesitate to contact tslil clingman at tslil@jhu.edu or the meeting email address ctoctoberfest19@math.jhu.edu. We hope to see you there! -- 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/BYAPR01MB5351EE85F1F6A2793FCBBA1BB98E0%40BYAPR01MB5351.prod.exchangelabs.com. [-- Attachment #2: Type: text/html, Size: 2507 bytes --]

In ABCFHL, even the function fst(coe(ua(e))) : A -> B is only path-equal to fst(e) : A -> B. If I recall correctly, the issue is that composition in the Glue type that you use to implement ua doesn’t judgementally give you f; instead there is some morally-the-identity-composition (that would cancel with regularity) that gets stuck in. This is because the general algorithm for composition in the glue type has to coerce in the “base” of the glue type (B in Glue [alpha -> T] B), which in the case of ua(e) = Glue [x = 0 -> (A,e), x=1 -> (B,id)] B is degenerate in x, but in general might not be. I don’t recall any cubical type theories solving this, but I don’t remember the details of all of the other variations that have been explored well enough to say for sure. > On Sep 18, 2019, at 11:42 AM, Michael Shulman <shulman@sandiego.edu> wrote: > > Let Equiv(A,B) denote the type of half-adjoint equivalences, so that > an e:Equiv(A,B) consists of five data: a function A -> B, a function B > -> A, two homotopies, and a coherence 2-path. Using univalence, we > can make e into an identification ua(e) : A=B, and then back into an > equivalence coe(ua(e)) : Equiv(A,B), which is typally equal to e. > > Now we might wonder whether coe(ua(e)) might be in fact *judgmentally* > equal to e; or at least whether this might be true of some, if not > all, of its five components. In Book HoTT this is clearly not the > case, since univalence is posited as an axiom about which we know > nothing else. But what about cubical type theories? Can any of the > components of an equivalence e be recovered, up to judgmental > equality, from coe(ua(e))? (My guess would be that at least the > function A -> B, and probably also the function B -> A, can be > recovered, but perhaps not more.) > > -- > 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/CAOvivQzzSXNHs%2BzbPQTyHEuU53aHXJ0sPe4pr%2Byf0ahLGvUpVA%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/1DF8E802-2959-4BEF-A85A-3C6E5E7B9595%40wesleyan.edu.

Let Equiv(A,B) denote the type of half-adjoint equivalences, so that an e:Equiv(A,B) consists of five data: a function A -> B, a function B -> A, two homotopies, and a coherence 2-path. Using univalence, we can make e into an identification ua(e) : A=B, and then back into an equivalence coe(ua(e)) : Equiv(A,B), which is typally equal to e. Now we might wonder whether coe(ua(e)) might be in fact *judgmentally* equal to e; or at least whether this might be true of some, if not all, of its five components. In Book HoTT this is clearly not the case, since univalence is posited as an axiom about which we know nothing else. But what about cubical type theories? Can any of the components of an equivalence e be recovered, up to judgmental equality, from coe(ua(e))? (My guess would be that at least the function A -> B, and probably also the function B -> A, can be recovered, but perhaps not more.) -- 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/CAOvivQzzSXNHs%2BzbPQTyHEuU53aHXJ0sPe4pr%2Byf0ahLGvUpVA%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 24266 bytes --] Indeed, one can find traces of this in the note http://www.cse.chalmers.se/~coquand/compv1.pdf Thierry PS: The “glueing” operation was then introduced only as a computational way to transform an equivalence to a path and one needed another composition for the universe to get regularity. One insight was the reduction of “filling” to “composition” but this was using regularity. As explained in the thread, there was a bug with composition in the universe, found by Carlo, Dan and Bob. After this problem was made explicit, one could find another way (a little more complex) to reduce filling to composition which does not use regularity. It was then realised (by Anders and Simon) that “glueing” was already enough to get univalence. This was explained later by understanding that this “glueing” operation actually expresses the “equivalence extension property” (used in the simplicial set model for proving univalence). This was helped by the introduction of the notion of “partial elements” which also simplified the presentation and made proof checking much easier. We could recover a model but without Path = Id. It was really surprising, at least for me, that one could still define Id from Path (using Andrew Swan’s method). On 18 Sep 2019, at 14:16, Anders Mortberg <andersmortberg@gmail.com<mailto:andersmortberg@gmail.com>> wrote: I tried to recall what the problem with regularity for comp for universes was in CCHM and here's what I've come up with. As pointed out by Dan and Jasper we need an equation like "Glue [ phi |-> (A, reflEquiv) ] A = A" to get a regular version of the reduction of comp for U to comp for Glue. This indeed seems very unnatural and it is not what we tried. What we instead did in the old buggy version of cubicaltt was to add new hcomp_U values to CCHM for compositions of types and reduce comp in U to one of these: comp^i U [phi -> A] A0 = hcomp^i_U [phi -> A] A0 For regularity we need the following condition on hcomp_U (where "i # A" means that i does not occur in A, i.e. if we're only attaching degenerate sides to A0): if i # A then hcomp^i_U [phi -> A] A0 = A0 The problem is then to define comp^j (hcomp^i_U [phi -> A] A0) [psi -> B] B0 such that it satisfies the standard equations for comp/hcomp_U and regularity. There are in particular two regularity conditions that we need to take into account: 1. if j # (hcomp^i_U [phi -> A] A0) and j # B then comp^j (hcomp^i_U [phi -> A] A0) [psi -> B] B0 = B0 2. if i # A then comp^j (hcomp^i_U [phi -> A] A0) [psi -> B] B0 = comp^j A0 [psi -> B] B0 We achieved 1 by essentially doing the same algorithm as for comp Glue (which Jasper pointed out is indeed regular), but this only satisfied the equation comp^j (hcomp^i_U [] A0) [psi -> B] B0 = comp^j A0 [psi -> B] B0 and not the full version of 2. I think this is what Dan and the others found and reported to us, at least that's how I read the old thread. It might be possible to get 2 and not 1, but I would be very surprised if we can get both 1 and 2 by just adapting the algorithms. Indeed, in light of Andrew's negative results I would expect substantial changes and some new ideas to be necessary in order to give a constructive model of univalent type theory where Path = Id. -- Anders On Mon, Sep 16, 2019 at 10:17 PM Jasper Hugunin <jasperh@cs.washington.edu<mailto:jasperh@cs.washington.edu>> wrote: I agree with the problem of using Glue types for the composition operation in the universe. You could imagine an extra equation that Glue [ phi |-> (A, reflEquiv) ] A = A, but this is somehow unnatural. However, it is what I was postulating in step 1 of the initial message of this thread. (You then need comp Glue to respect this equation, which appears impossible.) The way to get around it is, in my opinion, to add a separate type former Box^i [ phi |-> T ] A for phi |- A = T(i1), satisfying the laws phi |- Box^i [ phi |-> T ] A = T(i0) and regularity: Box^i [ phi |-> A ] A = A. You then need comp Box to respect Box^i [ phi |-> A ] A = A, and this is also apparently not possible in CCHM, but you now have the extra information that A is a line of types. (Using Box to turn an equivalence into a line of types in the definition of comp Box is circular.) I've developed a notion of (regular) n-dimensional composition, which I think might suffice to complete the argument. If you call a notion of Box that satisfies Box^i [ phi |-> A ] A = A "regular Box's", then the problem can be reduced to saying that to give regular 1-dimensional composition of regular 1-dimensional boxes, you need some sort of "(doubly) regular 2-dimensional composition" for A, and in CCHM such we can only get this "2-dimensional composition" which is regular in one direction or the other. Of course (I haven't actually checked, but my intuition says that), once you have 2-dimensional composition you will need n-dimensional composition, and then hopefully regular (n+m)-dimensional composition for A will suffice to define regular n-dimensional composition of regular n-dimensional Box's. Below I'll put an explanation of my idea of regular n-dimensional composition (returning an (n-1)-dimensional cube), since it feels unfair to say "I know how to do this" and hide "how to do this". Unfortunately, it is quite complex; read at your own peril. I don't yet know how to intelligibly describe n-dimensional composition for Glue and Box. For now I'll just say that they should be essentially the same as in the 1-dimensional case, but with extra faces in the equiv and final hcomp steps corresponding to faces in the result. =============== In CCHM, the basic Kan operation is (comp^i A [ phi |-> a ] a0 : A(i1) [ phi |-> a(i1) ]) for i |- A with phi, i |- a : A and a0 : A(i0) [ phi |-> a(i0) ]. Regularity for this operation means that if A and a are independent of i, then comp^i A [ phi |-> a ] a0 = a0. We have regular composition for Glue types, but we don't have comp^i (Glue [ phi |-> (A, equivRefl) ] A) = comp^i A. Simplifying things a little, we can take hcom^i U [ phi |-> T ] A = Box^i [ phi |-> T(i := ~ i) ] A to be a new type former, and give that a regular composition operation. Here the thing blocking us from getting comp^i (Box^j [ phi |-> A ] A) = comp^i A is that, given i, j |- T with phi, i, j |- t : T and t0 : T(i0)(j0)[ phi |-> t(i0)(j0) ], we need a Path T(i1)(j1) (comp^i T(j1) [ phi |-> t(j1) ] (comp^j T(i0) [ phi |-> t(i0) ] t0)) (comp^j T(i1) [ phi |-> t(i1) ] (comp^i T(j0) [ phi |-> t(j0) ] t0)) which is refl if T is degenerate in i OR j. This path plays the role that pres does in composition for Glue. (I will write (i o j) for composition over j then over i, and (i = j) for composition over the diagonal (i = j). Then we want a path from (i o j) to (j o i) which is degenerate if T is degenerate in i OR j. We can't construct such a doubly regular path, but we can postulate it as a new operation our types have to have, as a sort of regular composition over two dimensions simultaneously. Write (i ?'[a] j) for this, where a gives the location in the path. However, my intuition tells me that while this two-dimensional regular composition may be preserved by all the usual type formers, optimistically including Glue and Box, because the two-dimensional composition for Box will have to satisfy an additional law comp2^i^j (Box [ phi |-> A ] A) = comp2^i^j A, we will end up needing some sort of three-dimensional analogue. Once we need dimensions 1 and 2, we will almost certainly need dimension n. But what should the type of three dimensional regular composition be? There are six ways to compose along the edges of a cube, forming a hexagon that we wan't to fill, but hexagons don't fit nicely into cubical type theory. Here, we remember that there is one more way to compose across a square: along the diagonal (comp^k T(i,j:=k) [ phi |-> t(i,j:=k) ] t0), which agrees with composing either right then up or up then right when T is degenerate in i or j (with regularity). Allowing diagonals, for each square we can give a path from the diagonal to going up then right, with swapping i and j giving a path to going right then up. Then if both of these are degenerate when T is degenerate in i or j, their composition is also, so we recover a path between (i o j) and (j o i). And this formulation can be extended to higher dimensions straightforwardly. For each n-cube i_1, ..., i_n |- A, we have an n-dimensional regular composition operation which is a (n-1)-dimensional cube. Consider notation (i_1 ?[j_1] i_2 ?[j_2] ... ?[j_n-1] i_n) This is supposed to represent composition in an n-cube indexed by the i's, where our position in the resulting (n-1)-cube is given by the j's. We have to describe the faces of this cube, which we describe by saying that ?[0] reduces to = and ?[1] reduces to o. Thus for 2-dimensional A, we have a line (i = j) --- (i ?[a] j) --- (i o j), and for three dimensional A, we have a square with four faces (i = j ?[a_2] k), (i o j ?[a_2] k), (i ?[a1] j = k) (i ?[a1] j o k), relating the four corners given by coercing over i then j then k, coercing over i then j and k simultaneously, coercing over i and j simultaneously then coercing over k, and coercing over i, j, and k simultaneously. The point is that this gives a well-defined notion of cube. We also have to define the regularity condition: what happens when A, a are degenerate in i_k? We require that (i_1 ... i_k-1 ?[j_k-1] i_k ?[j_k] i_k+1 ... i_n) is equal to (i_1 ... i_k-1 ?[j_k-1 v j_k] i_k+1 ... i_n), treating j_0 = j_n = 1. Extending this to = and o, if A, a are degenerate in i, then (i = j) and (i o j) reduce to (j). On a two-dimensional cube, this says that (i ?[a] j) reduces to (j) when A, a are degenerate in i, and to (i) when A, a are degenerate in j. (That this is all coherent is obvious to me, but I have no idea how to explain it well) This all gives a notion of n-dimensional regular composition, which takes an n-cube type A and partial term phi, i1, ..., in |- a and a base point a0 : A(i_k := 0)[ phi |-> a(i_k := 0) ] and returns an (n-1)-cube in A(i_k := 1) [ phi |-> everywhere a(i_k := 1) ]. There are three classes of equations that this has to satisfy, two for the face maps j_k = 0 and j_k = 1 in the output, and one for when A, a are degenerate in i_k. In the one-dimensional case, this is the same as the specification of the usual regular comp. Considering j_k to be formally extended with j_0 = j_n = 1, we get a "zero-dimensional" composition operation, which should be taken to be the identity. (I have no idea what it would mean to let j_0 and j_n vary) I am reasonably confident that this operation is closed under usual type formers (Pi, Sg, Path, ...) by essentially the same argument as for 1-dimensional comp. I think I have worked out how to give a regular n-dimensional composition operation for Glue, by essentially the same argument as in CCHM, but with additional faces for j_k = 1 in the equiv and final hcomp steps. In this setting, we want Box to also be m-dimensional: j_1 ... j_n-1 |- Box^i1...^im _{j_1}..._{j_n-1} [ phi |-> T ] A for phi, i1, ..., im |- T, with phi |- A = T(i_k := 1). I think I have worked out how to give a regular n-dimensional composition operation for m-dimensional Box, using essentially the same argument as for Glue, but replacing pres with the composition of two paths given by (m+n)-dimensional regular composition. To use Box as the regular n-dimensional composition operation for the universe, we need that (Box, comp Box) respects the equations for when j_k = 0, j_k = 1, or T is independent of j. My hope is that, as in the (1, 1) dimensional case, using (m+n)-dimensional regular composition for pres will make this work. I have sketched on paper that composition for Glue and Box are regular, but that is already pushing the limits of my confidence in paper calculations. Checking that comp Box respects the equations that it needs to is another layer more complex, and I haven't managed to do so on paper. However, by analogy with the (1, 1) dimensional case, I am hopeful. On Mon, Sep 16, 2019 at 3:01 PM Licata, Dan <dlicata@wesleyan.edu<mailto:dlicata@wesleyan.edu>> wrote: Wow! I read that pretty closely and couldn’t find a problem. That is surprising to me. Will look more later. What I was saying about fill for the aligning algorithm is also wrong — I wasn’t thinking that the type of the filling was also degenerate, but of course it is here. So that might work too. However, even if there can be a universe of regular types that is closed under glue types, there’s still a problem with using those glue types to show that that universe is itself regularly fibrant, I think? If you define comp U [phi -> i.T] B to be Glue [phi -> T(1),...] B then no matter how nice the equivalence is (eg the identity) when i doesn’t occur in T, the type will not equal B — that would be an extra equation about the Glue type constructor itself. Does that seem right? -Dan On Sep 16, 2019, at 1:09 PM, Jasper Hugunin <jasperh@cs.washington.edu<mailto:jasperh@cs.washington.edu>> wrote: Hi Dan, Of course. I'm thinking primarily of composition for Glue given in the CCHM paper you linked, reproduced below. As you know, the single potential issue is that we need pres of a degenerate filling problem and function to be reflexivity. I claim that this holds by regularity of composition in T and A, partly as a consequence of the fact that regularity of composition implies regularity of filling (that fill of a degenerate system is refl), which certainly holds for fill defined by connections (and I believe also holds for fill as defined in ABCFHL). (a) Given i |- B = Glue [ phi |-> (T, f) ] A, with psi, i |- b : B and b0 : B(i0)[ psi |-> b(i0) ], we want to compute b1 = comp^i B [ psi |-> b ] b0 : B(i1)[ psi |-> b(i1) ]. We set a := unglue b and a0 := unglue b0. Set delta := forall i. phi. Then we take: a1' := comp^i A [ psi |-> a ] a0 delta |- t1' := comp^i T [ psi |-> b ] b0 delta |- omega := pres^i f [ psi |-> b ] b0 phi(i1) |- (t, alpha) := equiv f(i1) [ delta |-> (t1', omega), psi |-> (b(i1), refl a1') ] a1' a1 := hcomp^j A(i1) [ phi(i1) |-> alpha j, psi |-> a(i1) ] a1' (note that in the regular setting the psi face is redundant) b1 := glue [ phi(i1) |-> t1 ] a1 With given i |- f : T -> A, with psi, i |- b : T and b0 : T(i0)[ psi |-> b(i0) ], we define pres^i f [ psi |-> b ] b0 = <j> comp^i A [ psi |-> f b, j = 1 |-> f (fill^i T [ psi |-> b ] b0) ] (f(i0) b0). (b) Now consider the regular case, where phi, T, f, and A are independent of i. We want that b1 = b0. We have that a is independent of i, and delta = phi. First consider delta (= phi) |- pres^i f [ psi |-> b ] b0. (This is the explanation of your first dash) Note that if comp^i A is regular, then fill^i A [ psi |-> b ] b0 = b This is <j> comp^i A [ psi |-> f b, j = 1 |-> f (fill^i T [ psi |-> t ] t0) ] (f t0) = <j> comp^i A [ psi |-> f b, j = 1 |-> f t0 ] (f t0) = <j> f t0. Thus pres of a degenerate filling problem and function is reflexivity. Going back to composition of Glue, a1' = a0 phi |- t1' = b0 phi |- omega = refl (f b0) phi |- (t1, alpha) = (t1', omega) (since delta = phi, so we end up in the delta face of equiv) a1 = a1' (the only dependence on j is via (alpha j), but alpha = omega = refl, so this filling problem is degenerate) b1 = glue [ phi |-> t1 ] a1 = glue [ phi |-> b0 ] a0 = glue [ phi |-> b0 ] (unglue b0) = b0 (by eta, see Figure 4 in CCHM) Thus this algorithm for composition of Glue is regular. Other algorithms, such as the one in ABCFHL, may not be, but I am prone to believe that there exist regular algorithms in other settings including Orton-Pitts and Cartesian cubes. Best regards, - Jasper Hugunin On Mon, Sep 16, 2019 at 12:18 PM Licata, Dan <dlicata@wesleyan.edu<mailto:dlicata@wesleyan.edu>> wrote: Hi Jasper, It would help me follow the discussion if you could say a little more about (a) which version of composition for Glue exactly you mean (because there is at least the one in the CCHM paper and the “aligned” one from Orton-Pitts, which are intensionally different, as well as other possible variations), and (b) include some of your reasoning for why you think things are regular, to make it easier for me and others to reconstruct. My current understanding is that - For CCHM proper https://arxiv.org/pdf/1611.02108.pdf the potential issue is with the ‘pres’ path omega, which via the equiv operation ends up in alpha, so the system in a1 may not be degenerate even if the input is. Do you think this does work out to be degenerate? - For the current version of ABCFHL https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf which uses aligning “all the way at the outside”, an issue is with the adjust_com operation on page 20, which is later used for aligning (in that case beta is (forall i phi)). The potential issue is that adjust_com uses a *filler*, not just a composition from 0 to 1, so even if t doesn’t depend on z, the filling does, and the outer com won’t cancel. In CCHM, filling is defined using connections, so it’s a little different, but I think there still has to be a dependence on z for it to even type check — it should come up because of the connection term that is substituted into the type of the composition problem. So I’d guess there is still a problem in the aligned algorithm for CCHM. However, it would be great if this is wrong and something does work! -Dan On Sep 15, 2019, at 10:18 PM, Jasper Hugunin <jasperh@cs.washington.edu<mailto:jasperh@cs.washington.edu>> wrote: This doesn't seem right; as far as I can tell, composition for Glue types in CCHM preserves regularity and reduces to composition in A on phi. - Jasper Hugunin On Sun, Sep 15, 2019 at 3:28 AM Anders Mortberg <anders.mortberg@math.su.se<mailto:anders.mortberg@math.su.se>> wrote: Hi Jasper, Indeed, the problem is to construct an algorithm for comp (or even coe/transp) for Glue that reduces to the one of A when phi is true while still preserving regularity. It was pointed out independently by Sattler and Orton around 2016 that one can factor out this step in our algorithm in a separate lemma that is now called "alignment". This is Thm 6.13 in Orton-Pitts and discussed in a paragraph in the end of section 2.11 of ABCFHL. Unless I'm misremembering this is exactly where regularity for comp for Glue types break down. In this step we do an additional comp/hcomp that inserts an additional forall i. phi face making the comp/coe irregular. One could imagine there being a way to modify the algorithm to avoid this, maybe by inlining the alignment step... But despite considerable efforts no one has been able to figure this out and I think Swan's recent paper (https://arxiv.org/abs/1808.00920v3) shows that this is not even possible! Another approach would be to have weak Glue types that don't strictly reduce to A when phi is true, but this causes problems for the composition in the universe and would be weird for cubical type theory... In light of Swan's negative results I think we need a completely new approach if we ever hope to solve this problem. Luckily for you Andrew Swan is starting as a postdoc over in Baker Hall in October, so he can explain his counterexamples to you in person. Best, Anders On Sun, Sep 15, 2019 at 7:57 AM Jasper Hugunin <jasperh@cs.washington.edu<mailto:jasperh@cs.washington.edu>> wrote: Offline, Carlo Angiuli showed me that the difficulty was in part 1, because of a subtlety I had been forgetting. Since types are *Kan* cubical sets, we need that the Kan operations agree as well as the sets. So part 1 could be thought of as (Glue [ phi |-> equivRefl A ] A, compGlue) = (A, compA), and getting that the Kan operations to agree was/is difficult. (Now that I know what the answer is, it is clear that this was already explained in the initial discussion.) Humbly, - Jasper Hugunin On Fri, Sep 13, 2019 at 2:10 AM Jasper Hugunin <jasperh@cs.washington.edu<mailto:jasperh@cs.washington.edu>> wrote: Hello all, I've been trying to understand better why composition for the universe does not satisfy regularity. Since comp^i [ phi |-> E ] A is defined as (roughly) Glue [ phi |-> equiv^i E ] A, I would expect regularity to follow from two parts: 1. That Glue [ phi |-> equivRefl A ] A reduces to A (a sort of regularity condition for the Glue type constructor itself) 2. That equiv^i (refl A) reduces to equivRefl A I'm curious as to which (or both) of these parts was the issue, or if regularity for the universe was supposed to follow from a different argument. Context: I've been studying and using CCHM cubical type theory recently, and often finding myself wishing that J computed strictly. If I understand correctly, early implementations of ctt did have strict J for Path types, and this was justified by a "regularity" condition on the composition operation, but as discussed in this thread on the HoTT mailing list, the definition of composition for the universe was found to not satisfy regularity. I don't remember seeing the regularity condition defined anywhere, but my understanding is that it requires that composition in a degenerate line of types, with the system of constraints giving the sides of the box also degenerate in that direction, reduces to just the bottom of the box. This seems to be closed under the usual type formers, plus Glue, but not the universe with computation defined as in the CCHM paper (for trivial reasons and non-trivial reasons; it gets stuck at the start with Glue [ phi |-> equiv^i refl ] A not reducing to anything). Best regards, - Jasper Hugunin -- 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/CAGTS-a9oS0CQDGKgj7ghCh8%2BZwAcAefiTg4JJVHemV3HUPcPEg%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8SZx8PiaD-9rq5QWffU75Wz8myrXD1g5P3DCjSO%3DfvOQ%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8E03C3BMEwi-T4qjet4EbCgnePhR3Ffa1MepxNmtZoUA%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCpp%3DEMvH%2BXtRn7AfyjRDjmiwxfML2JQqKyPjXAhM%2BM2vcjw%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/C1FA3BE5-6469-47F7-9049-914A6AFC68BA%40chalmers.se. [-- Attachment #2: Type: text/html, Size: 31258 bytes --]

I tried to recall what the problem with regularity for comp for universes was in CCHM and here's what I've come up with. As pointed out by Dan and Jasper we need an equation like "Glue [ phi |-> (A, reflEquiv) ] A = A" to get a regular version of the reduction of comp for U to comp for Glue. This indeed seems very unnatural and it is not what we tried. What we instead did in the old buggy version of cubicaltt was to add new hcomp_U values to CCHM for compositions of types and reduce comp in U to one of these: comp^i U [phi -> A] A0 = hcomp^i_U [phi -> A] A0 For regularity we need the following condition on hcomp_U (where "i # A" means that i does not occur in A, i.e. if we're only attaching degenerate sides to A0): if i # A then hcomp^i_U [phi -> A] A0 = A0 The problem is then to define comp^j (hcomp^i_U [phi -> A] A0) [psi -> B] B0 such that it satisfies the standard equations for comp/hcomp_U and regularity. There are in particular two regularity conditions that we need to take into account: 1. if j # (hcomp^i_U [phi -> A] A0) and j # B then comp^j (hcomp^i_U [phi -> A] A0) [psi -> B] B0 = B0 2. if i # A then comp^j (hcomp^i_U [phi -> A] A0) [psi -> B] B0 = comp^j A0 [psi -> B] B0 We achieved 1 by essentially doing the same algorithm as for comp Glue (which Jasper pointed out is indeed regular), but this only satisfied the equation comp^j (hcomp^i_U [] A0) [psi -> B] B0 = comp^j A0 [psi -> B] B0 and not the full version of 2. I think this is what Dan and the others found and reported to us, at least that's how I read the old thread. It might be possible to get 2 and not 1, but I would be very surprised if we can get both 1 and 2 by just adapting the algorithms. Indeed, in light of Andrew's negative results I would expect substantial changes and some new ideas to be necessary in order to give a constructive model of univalent type theory where Path = Id. -- Anders On Mon, Sep 16, 2019 at 10:17 PM Jasper Hugunin <jasperh@cs.washington.edu> wrote: > > I agree with the problem of using Glue types for the composition operation in the universe. > You could imagine an extra equation that Glue [ phi |-> (A, reflEquiv) ] A = A, but this is somehow unnatural. > However, it is what I was postulating in step 1 of the initial message of this thread. > (You then need comp Glue to respect this equation, which appears impossible.) > > The way to get around it is, in my opinion, to add a separate type former Box^i [ phi |-> T ] A for phi |- A = T(i1), satisfying the laws phi |- Box^i [ phi |-> T ] A = T(i0) and regularity: Box^i [ phi |-> A ] A = A. > You then need comp Box to respect Box^i [ phi |-> A ] A = A, and this is also apparently not possible in CCHM, but you now have the extra information that A is a line of types. (Using Box to turn an equivalence into a line of types in the definition of comp Box is circular.) > > I've developed a notion of (regular) n-dimensional composition, which I think might suffice to complete the argument. > If you call a notion of Box that satisfies Box^i [ phi |-> A ] A = A "regular Box's", then the problem can be reduced to saying that to give regular 1-dimensional composition of regular 1-dimensional boxes, you need some sort of "(doubly) regular 2-dimensional composition" for A, and in CCHM such we can only get this "2-dimensional composition" which is regular in one direction or the other. > Of course (I haven't actually checked, but my intuition says that), once you have 2-dimensional composition you will need n-dimensional composition, and then hopefully regular (n+m)-dimensional composition for A will suffice to define regular n-dimensional composition of regular n-dimensional Box's. > > Below I'll put an explanation of my idea of regular n-dimensional composition (returning an (n-1)-dimensional cube), since it feels unfair to say "I know how to do this" and hide "how to do this". > Unfortunately, it is quite complex; read at your own peril. > > I don't yet know how to intelligibly describe n-dimensional composition for Glue and Box. > For now I'll just say that they should be essentially the same as in the 1-dimensional case, but with extra faces in the equiv and final hcomp steps corresponding to faces in the result. > > =============== > > In CCHM, the basic Kan operation is (comp^i A [ phi |-> a ] a0 : A(i1) [ phi |-> a(i1) ]) for i |- A with phi, i |- a : A and a0 : A(i0) [ phi |-> a(i0) ]. > Regularity for this operation means that if A and a are independent of i, then comp^i A [ phi |-> a ] a0 = a0. > We have regular composition for Glue types, but we don't have comp^i (Glue [ phi |-> (A, equivRefl) ] A) = comp^i A. > Simplifying things a little, we can take hcom^i U [ phi |-> T ] A = Box^i [ phi |-> T(i := ~ i) ] A to be a new type former, and give that a regular composition operation. > Here the thing blocking us from getting comp^i (Box^j [ phi |-> A ] A) = comp^i A is that, given i, j |- T with phi, i, j |- t : T and t0 : T(i0)(j0)[ phi |-> t(i0)(j0) ], > we need a Path T(i1)(j1) (comp^i T(j1) [ phi |-> t(j1) ] (comp^j T(i0) [ phi |-> t(i0) ] t0)) (comp^j T(i1) [ phi |-> t(i1) ] (comp^i T(j0) [ phi |-> t(j0) ] t0)) which is refl if T is degenerate in i OR j. > This path plays the role that pres does in composition for Glue. > (I will write (i o j) for composition over j then over i, and (i = j) for composition over the diagonal (i = j). Then we want a path from (i o j) to (j o i) which is degenerate if T is degenerate in i OR j. > > We can't construct such a doubly regular path, but we can postulate it as a new operation our types have to have, as a sort of regular composition over two dimensions simultaneously. Write (i ?'[a] j) for this, where a gives the location in the path. > However, my intuition tells me that while this two-dimensional regular composition may be preserved by all the usual type formers, optimistically including Glue and Box, because the two-dimensional composition for Box will have to satisfy an additional law comp2^i^j (Box [ phi |-> A ] A) = comp2^i^j A, we will end up needing some sort of three-dimensional analogue. > Once we need dimensions 1 and 2, we will almost certainly need dimension n. > > But what should the type of three dimensional regular composition be? There are six ways to compose along the edges of a cube, forming a hexagon that we wan't to fill, but hexagons don't fit nicely into cubical type theory. > Here, we remember that there is one more way to compose across a square: along the diagonal (comp^k T(i,j:=k) [ phi |-> t(i,j:=k) ] t0), which agrees with composing either right then up or up then right when T is degenerate in i or j (with regularity). > Allowing diagonals, for each square we can give a path from the diagonal to going up then right, with swapping i and j giving a path to going right then up. Then if both of these are degenerate when T is degenerate in i or j, their composition is also, so we recover a path between (i o j) and (j o i). And this formulation can be extended to higher dimensions straightforwardly. > > For each n-cube i_1, ..., i_n |- A, we have an n-dimensional regular composition operation which is a (n-1)-dimensional cube. Consider notation (i_1 ?[j_1] i_2 ?[j_2] ... ?[j_n-1] i_n) This is supposed to represent composition in an n-cube indexed by the i's, where our position in the resulting (n-1)-cube is given by the j's. We have to describe the faces of this cube, which we describe by saying that ?[0] reduces to = and ?[1] reduces to o. > Thus for 2-dimensional A, we have a line (i = j) --- (i ?[a] j) --- (i o j), and for three dimensional A, we have a square with four faces (i = j ?[a_2] k), (i o j ?[a_2] k), (i ?[a1] j = k) (i ?[a1] j o k), relating the four corners given by coercing over i then j then k, coercing over i then j and k simultaneously, coercing over i and j simultaneously then coercing over k, and coercing over i, j, and k simultaneously. > The point is that this gives a well-defined notion of cube. > We also have to define the regularity condition: what happens when A, a are degenerate in i_k? We require that (i_1 ... i_k-1 ?[j_k-1] i_k ?[j_k] i_k+1 ... i_n) is equal to (i_1 ... i_k-1 ?[j_k-1 v j_k] i_k+1 ... i_n), treating j_0 = j_n = 1. > Extending this to = and o, if A, a are degenerate in i, then (i = j) and (i o j) reduce to (j). > On a two-dimensional cube, this says that (i ?[a] j) reduces to (j) when A, a are degenerate in i, and to (i) when A, a are degenerate in j. > (That this is all coherent is obvious to me, but I have no idea how to explain it well) > > This all gives a notion of n-dimensional regular composition, which takes an n-cube type A and partial term phi, i1, ..., in |- a and a base point a0 : A(i_k := 0)[ phi |-> a(i_k := 0) ] and returns an (n-1)-cube in A(i_k := 1) [ phi |-> everywhere a(i_k := 1) ]. > There are three classes of equations that this has to satisfy, two for the face maps j_k = 0 and j_k = 1 in the output, and one for when A, a are degenerate in i_k. > In the one-dimensional case, this is the same as the specification of the usual regular comp. > Considering j_k to be formally extended with j_0 = j_n = 1, we get a "zero-dimensional" composition operation, which should be taken to be the identity. (I have no idea what it would mean to let j_0 and j_n vary) > I am reasonably confident that this operation is closed under usual type formers (Pi, Sg, Path, ...) by essentially the same argument as for 1-dimensional comp. > I think I have worked out how to give a regular n-dimensional composition operation for Glue, by essentially the same argument as in CCHM, but with additional faces for j_k = 1 in the equiv and final hcomp steps. > > In this setting, we want Box to also be m-dimensional: j_1 ... j_n-1 |- Box^i1...^im _{j_1}..._{j_n-1} [ phi |-> T ] A for phi, i1, ..., im |- T, with phi |- A = T(i_k := 1). > I think I have worked out how to give a regular n-dimensional composition operation for m-dimensional Box, using essentially the same argument as for Glue, but replacing pres with the composition of two paths given by (m+n)-dimensional regular composition. > To use Box as the regular n-dimensional composition operation for the universe, we need that (Box, comp Box) respects the equations for when j_k = 0, j_k = 1, or T is independent of j. > My hope is that, as in the (1, 1) dimensional case, using (m+n)-dimensional regular composition for pres will make this work. > > I have sketched on paper that composition for Glue and Box are regular, but that is already pushing the limits of my confidence in paper calculations. > Checking that comp Box respects the equations that it needs to is another layer more complex, and I haven't managed to do so on paper. > However, by analogy with the (1, 1) dimensional case, I am hopeful. > > On Mon, Sep 16, 2019 at 3:01 PM Licata, Dan <dlicata@wesleyan.edu> wrote: >> >> Wow! I read that pretty closely and couldn’t find a problem. That is surprising to me. Will look more later. >> >> What I was saying about fill for the aligning algorithm is also wrong — I wasn’t thinking that the type of the filling was also degenerate, but of course it is here. So that might work too. >> >> However, even if there can be a universe of regular types that is closed under glue types, there’s still a problem with using those glue types to show that that universe is itself regularly fibrant, I think? If you define comp U [phi -> i.T] B to be Glue [phi -> T(1),...] B then no matter how nice the equivalence is (eg the identity) when i doesn’t occur in T, the type will not equal B — that would be an extra equation about the Glue type constructor itself. Does that seem right? >> >> -Dan >> >> On Sep 16, 2019, at 1:09 PM, Jasper Hugunin <jasperh@cs.washington.edu> wrote: >> >> Hi Dan, >> >> Of course. I'm thinking primarily of composition for Glue given in the CCHM paper you linked, reproduced below. >> As you know, the single potential issue is that we need pres of a degenerate filling problem and function to be reflexivity. I claim that this holds by regularity of composition in T and A, partly as a consequence of the fact that regularity of composition implies regularity of filling (that fill of a degenerate system is refl), which certainly holds for fill defined by connections (and I believe also holds for fill as defined in ABCFHL). >> >> (a) >> Given i |- B = Glue [ phi |-> (T, f) ] A, with psi, i |- b : B and b0 : B(i0)[ psi |-> b(i0) ], we want to compute b1 = comp^i B [ psi |-> b ] b0 : B(i1)[ psi |-> b(i1) ]. >> We set a := unglue b and a0 := unglue b0. >> Set delta := forall i. phi. >> Then we take: >> a1' := comp^i A [ psi |-> a ] a0 >> delta |- t1' := comp^i T [ psi |-> b ] b0 >> delta |- omega := pres^i f [ psi |-> b ] b0 >> phi(i1) |- (t, alpha) := equiv f(i1) [ delta |-> (t1', omega), psi |-> (b(i1), refl a1') ] a1' >> a1 := hcomp^j A(i1) [ phi(i1) |-> alpha j, psi |-> a(i1) ] a1' (note that in the regular setting the psi face is redundant) >> b1 := glue [ phi(i1) |-> t1 ] a1 >> >> With given i |- f : T -> A, with psi, i |- b : T and b0 : T(i0)[ psi |-> b(i0) ], we define >> pres^i f [ psi |-> b ] b0 = <j> comp^i A [ psi |-> f b, j = 1 |-> f (fill^i T [ psi |-> b ] b0) ] (f(i0) b0). >> >> (b) >> Now consider the regular case, where phi, T, f, and A are independent of i. We want that b1 = b0. >> We have that a is independent of i, and delta = phi. >> >> First consider delta (= phi) |- pres^i f [ psi |-> b ] b0. (This is the explanation of your first dash) >> Note that if comp^i A is regular, then fill^i A [ psi |-> b ] b0 = b >> This is <j> comp^i A [ psi |-> f b, j = 1 |-> f (fill^i T [ psi |-> t ] t0) ] (f t0) = <j> comp^i A [ psi |-> f b, j = 1 |-> f t0 ] (f t0) = <j> f t0. >> Thus pres of a degenerate filling problem and function is reflexivity. >> >> Going back to composition of Glue, >> a1' = a0 >> phi |- t1' = b0 >> phi |- omega = refl (f b0) >> phi |- (t1, alpha) = (t1', omega) (since delta = phi, so we end up in the delta face of equiv) >> a1 = a1' (the only dependence on j is via (alpha j), but alpha = omega = refl, so this filling problem is degenerate) >> b1 = glue [ phi |-> t1 ] a1 = glue [ phi |-> b0 ] a0 = glue [ phi |-> b0 ] (unglue b0) = b0 (by eta, see Figure 4 in CCHM) >> >> Thus this algorithm for composition of Glue is regular. >> Other algorithms, such as the one in ABCFHL, may not be, but I am prone to believe that there exist regular algorithms in other settings including Orton-Pitts and Cartesian cubes. >> >> Best regards, >> - Jasper Hugunin >> >> On Mon, Sep 16, 2019 at 12:18 PM Licata, Dan <dlicata@wesleyan.edu> wrote: >>> >>> Hi Jasper, >>> >>> It would help me follow the discussion if you could say a little more about (a) which version of composition for Glue exactly you mean (because there is at least the one in the CCHM paper and the “aligned” one from Orton-Pitts, which are intensionally different, as well as other possible variations), and (b) include some of your reasoning for why you think things are regular, to make it easier for me and others to reconstruct. >>> >>> My current understanding is that >>> >>> - For CCHM proper https://arxiv.org/pdf/1611.02108.pdf the potential issue is with the ‘pres’ path omega, which via the equiv operation ends up in alpha, so the system in a1 may not be degenerate even if the input is. Do you think this does work out to be degenerate? >>> >>> - For the current version of ABCFHL https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf which uses aligning “all the way at the outside”, an issue is with the adjust_com operation on page 20, which is later used for aligning (in that case beta is (forall i phi)). The potential issue is that adjust_com uses a *filler*, not just a composition from 0 to 1, so even if t doesn’t depend on z, the filling does, and the outer com won’t cancel. In CCHM, filling is defined using connections, so it’s a little different, but I think there still has to be a dependence on z for it to even type check — it should come up because of the connection term that is substituted into the type of the composition problem. So I’d guess there is still a problem in the aligned algorithm for CCHM. >>> >>> However, it would be great if this is wrong and something does work! >>> >>> -Dan >>> >>> > On Sep 15, 2019, at 10:18 PM, Jasper Hugunin <jasperh@cs.washington.edu> wrote: >>> > >>> > This doesn't seem right; as far as I can tell, composition for Glue types in CCHM preserves regularity and reduces to composition in A on phi. >>> > >>> > - Jasper Hugunin >>> > >>> > On Sun, Sep 15, 2019 at 3:28 AM Anders Mortberg <anders.mortberg@math.su.se> wrote: >>> > Hi Jasper, >>> > >>> > Indeed, the problem is to construct an algorithm for comp (or even >>> > coe/transp) for Glue that reduces to the one of A when phi is true >>> > while still preserving regularity. It was pointed out independently by >>> > Sattler and Orton around 2016 that one can factor out this step in our >>> > algorithm in a separate lemma that is now called "alignment". This is >>> > Thm 6.13 in Orton-Pitts and discussed in a paragraph in the end of >>> > section 2.11 of ABCFHL. Unless I'm misremembering this is exactly >>> > where regularity for comp for Glue types break down. In this step we >>> > do an additional comp/hcomp that inserts an additional forall i. phi >>> > face making the comp/coe irregular. >>> > >>> > One could imagine there being a way to modify the algorithm to avoid >>> > this, maybe by inlining the alignment step... But despite considerable >>> > efforts no one has been able to figure this out and I think Swan's >>> > recent paper (https://arxiv.org/abs/1808.00920v3) shows that this is >>> > not even possible! >>> > >>> > Another approach would be to have weak Glue types that don't strictly >>> > reduce to A when phi is true, but this causes problems for the >>> > composition in the universe and would be weird for cubical type >>> > theory... >>> > >>> > In light of Swan's negative results I think we need a completely new >>> > approach if we ever hope to solve this problem. Luckily for you Andrew >>> > Swan is starting as a postdoc over in Baker Hall in October, so he can >>> > explain his counterexamples to you in person. >>> > >>> > Best, >>> > Anders >>> > >>> > On Sun, Sep 15, 2019 at 7:57 AM Jasper Hugunin >>> > <jasperh@cs.washington.edu> wrote: >>> > > >>> > > Offline, Carlo Angiuli showed me that the difficulty was in part 1, because of a subtlety I had been forgetting. >>> > > >>> > > Since types are *Kan* cubical sets, we need that the Kan operations agree as well as the sets. >>> > > So part 1 could be thought of as (Glue [ phi |-> equivRefl A ] A, compGlue) = (A, compA), and getting that the Kan operations to agree was/is difficult. >>> > > (Now that I know what the answer is, it is clear that this was already explained in the initial discussion.) >>> > > >>> > > Humbly, >>> > > - Jasper Hugunin >>> > > >>> > > On Fri, Sep 13, 2019 at 2:10 AM Jasper Hugunin <jasperh@cs.washington.edu> wrote: >>> > >> >>> > >> Hello all, >>> > >> >>> > >> I've been trying to understand better why composition for the universe does not satisfy regularity. >>> > >> Since comp^i [ phi |-> E ] A is defined as (roughly) Glue [ phi |-> equiv^i E ] A, I would expect regularity to follow from two parts: >>> > >> 1. That Glue [ phi |-> equivRefl A ] A reduces to A (a sort of regularity condition for the Glue type constructor itself) >>> > >> 2. That equiv^i (refl A) reduces to equivRefl A >>> > >> I'm curious as to which (or both) of these parts was the issue, or if regularity for the universe was supposed to follow from a different argument. >>> > >> >>> > >> Context: >>> > >> I've been studying and using CCHM cubical type theory recently, and often finding myself wishing that J computed strictly. >>> > >> If I understand correctly, early implementations of ctt did have strict J for Path types, and this was justified by a "regularity" condition on the composition operation, but as discussed in this thread on the HoTT mailing list, the definition of composition for the universe was found to not satisfy regularity. >>> > >> I don't remember seeing the regularity condition defined anywhere, but my understanding is that it requires that composition in a degenerate line of types, with the system of constraints giving the sides of the box also degenerate in that direction, reduces to just the bottom of the box. This seems to be closed under the usual type formers, plus Glue, but not the universe with computation defined as in the CCHM paper (for trivial reasons and non-trivial reasons; it gets stuck at the start with Glue [ phi |-> equiv^i refl ] A not reducing to anything). >>> > >> >>> > >> Best regards, >>> > >> - Jasper Hugunin >>> > > >>> > > -- >>> > > 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/CAGTS-a9oS0CQDGKgj7ghCh8%2BZwAcAefiTg4JJVHemV3HUPcPEg%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/CAGTS-a8SZx8PiaD-9rq5QWffU75Wz8myrXD1g5P3DCjSO%3DfvOQ%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/CAGTS-a8E03C3BMEwi-T4qjet4EbCgnePhR3Ffa1MepxNmtZoUA%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/CAMWCpp%3DEMvH%2BXtRn7AfyjRDjmiwxfML2JQqKyPjXAhM%2BM2vcjw%40mail.gmail.com.

[-- Attachment #1.1: Type: text/plain, Size: 3433 bytes --] Let me elaborate a bit on my answer. One might naively try to copy Dan and Guillaume's definition and write the following in Cubical Agda: Omega : (A : Type₀) → A → Type₀ Omega A a = (a ≡ a) itOmega : ℕ → (A : Type₀) → A → Type₀ itOmega zero A a = Omega A a itOmega (suc n) A a = itOmega n (Omega A a) refl data Sn (n : ℕ) : Type₀ where base : Sn n surf : itOmega n (Sn n) base However Agda will complain as surf is not constructing an element of Sn. This might seem a bit funny as Cubical Agda is perfectly happy with data S³ : Type₀ where base : S³ surf : Path (Path (base ≡ base) refl refl) refl refl But what is happening under the hood is that surf is a constructor taking i, j, and k in the interval and returning an element of S^3 with boundary "base" whenever i, j and k are 0 or 1. In cubicaltt we can write this HIT in the following way: data S3 = base | surf <i j k> [ (i=0) -> base , (i=1) -> base , (j=0) -> base , (j=1) -> base , (k=0) -> base , (k=1) -> base ] The problem is then clearer: in order to write the surf constructor of Sn we would have to quantify over n interval variables and specify the boundary of the n-cell. This is what that is not supported by any of the cubical schemas for HITs. -- Anders On Wednesday, September 18, 2019 at 11:00:22 AM UTC+2, Guillaume Brunerie wrote: > > Hi, > > We give a definition of S^n with one point and one n-loop by > introduction/elimination/reduction rules in our paper with Dan Licata > (https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can be > implemented in Agda (so Kristina’s question can be formulated and can > presumably be formalized in Agda) but I don’t think we actually proved > it. > > Best, > Guillaume > > Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg <andersm...@gmail.com > <javascript:>>: > > > > Hi Kristina, > > > > We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda: > > https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda > > > > However, I don't think we can even write down the general version of > > S^n as a type with a point and an n-loop with the schema implemented > > in Cubical Agda. As far as I know no other schema for HITs support > > this kind of types either. > > > > -- > > Anders > > > > On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova > > <sojakova...@gmail.com <javascript:>> wrote: > > > > > > Hello everybody, > > > > > > Is it worked out somewhere that the two definitions of Sn as a > > > suspension on one hand and a HIT with a point and an n-loop on the > other > > > hand are equivalent? This is also an exercise in the book. I know > > > Favonia has some Agda code on spheres but I couldn't find this result > in > > > there. > > > > > > Thanks, > > > > > > Kristina > > > > > > > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/db712ad2-396f-4328-bb73-898dcb956834%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 19638 bytes --]

Hi, We give a definition of S^n with one point and one n-loop by introduction/elimination/reduction rules in our paper with Dan Licata (https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can be implemented in Agda (so Kristina’s question can be formulated and can presumably be formalized in Agda) but I don’t think we actually proved it. Best, Guillaume Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg <andersmortberg@gmail.com>: > > Hi Kristina, > > We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda: > https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda > > However, I don't think we can even write down the general version of > S^n as a type with a point and an n-loop with the schema implemented > in Cubical Agda. As far as I know no other schema for HITs support > this kind of types either. > > -- > Anders > > On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova > <sojakova.kristina@gmail.com> wrote: > > > > Hello everybody, > > > > Is it worked out somewhere that the two definitions of Sn as a > > suspension on one hand and a HIT with a point and an n-loop on the other > > hand are equivalent? This is also an exercise in the book. I know > > Favonia has some Agda code on spheres but I couldn't find this result in > > there. > > > > Thanks, > > > > Kristina > > > > > > -- > > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/6c150b9c-fba6-47c1-2a6d-975b90f64638%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/CAMWCppm0sB2ZDMPM-jUYVpn8qxFJEfep6rsZs%3D8k%3Dhh6yGQF1w%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/CAFJ3QW%2BznvLhFgBODptrjnKcY8QaEH8BxD3adrgRUNvo5fU%2BEQ%40mail.gmail.com.