Right, I would say that interpreting in a representing model structure is the limit of current technology. Maybe one day we'll be able to interpret directly in an infinity-topos, but not yet. On Thu, Apr 18, 2019 at 3:09 AM Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: > > I only had a rough glance at your paper. But as it seems you don't > interpret directly in the infty toposes but rather in some > representing model structure. > No complaint because I don't expect otherwise. > > In any case it is quite an achievement to get universes "strongly `a > la Tarski". > > Thomas > > -- > 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. > For more options, visit https://groups.google.com/d/optout. -- 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. For more options, visit https://groups.google.com/d/optout.

I only had a rough glance at your paper. But as it seems you don't interpret directly in the infty toposes but rather in some representing model structure. No complaint because I don't expect otherwise. In any case it is quite an achievement to get universes "strongly `a la Tarski". Thomas -- 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. For more options, visit https://groups.google.com/d/optout.

Here's a brief summary of the steps: 1. Every Grothendieck (∞, 1)-topos can be presented by an accessible left exact left Bousfield localization of an injective model structure on a category of enriched simplicial presheaves. 2. Such presentations are right proper Cisinski model categories, hence (as we already knew) model MLTT, even with many HITs, but not previously known to model universes. 3. The fibrations in an injective model structure have no explicit "cofibrantly generated" description in terms of a lifting property, but it turns out they do have a fairly explicit "algebraic" description in terms of the rectifiability of homotopy coherent natural transformations (a homotopical version of "coflexible algebras"). 4. Now define a presheaf U by U(x) = the set of injective fibrations over the representable C(-,x) *equipped with* such fibrancy structure (suitably rectified to become a strict presheaf), and we get a fibrant and univalent universe. 5. Finally, any accessible left exact localization can be presented internally by a lex modality (using the recent characterization thereof by Anel-Biedermann-Finster-Joyal), and the universe of modal types for a lex modality is modal, giving a universe for the localized model structure. For more detail, you can read the introduction to the paper (or the whole thing, of course), or look at these slides from last month's Midwest HoTT seminar: http://home.sandiego.edu/~shulman/papers/injmodel-talk.pdf On Wed, Apr 17, 2019 at 3:59 PM 'Martin Escardo' via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> wrote: > > On 16/04/2019 13:06, Ali Caglayan wrote: > > Mike has released this new preprint on the arXiv: > > > > All (∞,1)-toposes have strict univalent universes > > <https://arxiv.org/abs/1904.07004> > > > > Quoting the abstract: > > > > Thus, homotopy type theory can be used as a formal language for > > reasoning internally to (∞, 1)-toposes, just as higher-order logic is > > used for 1-toposes. > > This is awesome. > > Perhaps it deserves a short explanation (or at least listing) of the > crucial steps gere in this list. > > Best, > Martin > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- 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. For more options, visit https://groups.google.com/d/optout.

On 16/04/2019 13:06, Ali Caglayan wrote: > Mike has released this new preprint on the arXiv: > > All (∞,1)-toposes have strict univalent universes > <https://arxiv.org/abs/1904.07004> > > Quoting the abstract: > > Thus, homotopy type theory can be used as a formal language for > reasoning internally to (∞, 1)-toposes, just as higher-order logic is > used for 1-toposes. This is awesome. Perhaps it deserves a short explanation (or at least listing) of the crucial steps gere in this list. Best, Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 648 bytes --] Mike has released this new preprint on the arXiv: All (∞,1)-toposes have strict univalent universes <https://arxiv.org/abs/1904.07004> Quoting the abstract: Thus, homotopy type theory can be used as a formal language for reasoning internally to (∞, 1)-toposes, just as higher-order logic is used for 1-toposes. :)) -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 935 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 7104 bytes --] FOURTH SYMPOSIUM ON COMPOSITIONAL STRUCTURES (SYCO 4) Chapman University, California, USA 22-23 May, 2019 http://events.cs.bham.ac.uk/syco/4/ 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. The first SYCO was in September 2018, at the University of Birmingham. The second SYCO was in December 2018, at the University of Strathclyde. The third SYCO was in March 2019, at the University of Oxford. Each meeting attracted about 70 participants. 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 will be 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 John Baez, University of California, Riverside Tobias Fritz, Perimeter Institute for Theoretical Physics Nina Otter, University of California, Los Angeles (One more speaker to be confirmed) # IMPORTANT DATES All times are anywhere-on-earth. - Submission deadline: Wednesday 24 April 2019 - Author notification: Wednesday 1 May 2019 - Travel support application deadline: Wednesday 8 May 2019 - Registration deadline: TBA - Symposium dates: Wednesday 22 and Thursday 23 May 2019 # SUBMISSIONS Submission is by EasyChair, via the following link: - https://easychair.org/conferences/?conf=syco4 Submissions should present research results in sufficient detail to allow them to be properly considered by members of the programme committee, who will assess papers with regards to significance, clarity, correctness, and scope. We encourage the submission of work in progress, as well as mature results. There are no proceedings, so work can be submitted even if it has been previously published, or has been submitted for consideration elsewhere. There is no specific formatting requirement, and no page limit, although for long submissions authors should understand that reviewers may not be able to read the entire document in detail. # FINANCIAL SUPPORT Some funding is available to cover travel and subsistence costs, with a priority for students and junior researchers. To apply for this funding, please contact the local organizer Alexander Kurz (axhkrz@gmail.com) with subject line "SYCO 4 funding request" by Wednesday, 8 May, with a short statement of your current status, travel costs, and funding required. # PROGRAMME COMMITTEE Miriam Backens, University of Oxford Ross Duncan, University of Strathclyde and Cambridge Quantum Computing Brendan Fong, Massachusetts Institute of Technology Stefano Gogioso, University of Oxford Amar Hadzihasanovic, Kyoto University Chris Heunen, University of Edinburgh Dominic Horsman, University of Grenoble Martti Karvonen, University of Edinburgh Kohei Kishida, Dalhousie University (chair) Aleks Kissinger, Radboud University Nijmegen Andre Kornell, University of California, Davis Martha Lewis, University of Amsterdam Samuel Mimram, École Polytechnique Benjamin Musto, University of Oxford Nina Otter, University of California, Los Angeles Simona Paoli, University of Leicester Dorette Pronk, Dalhousie University Mehrnoosh Sadrzadeh, Queen Mary Pawel Sobocinski, University of Southampton Joshua Tan, University of Oxford Sean Tull, University of Oxford Dominic Verdon, University of Bristol Jamie Vicary, University of Birmingham and University of Oxford Maaike Zwart, University of Oxford -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 8867 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 6414 bytes --] FOURTH SYMPOSIUM ON COMPOSITIONAL STRUCTURES (SYCO 4) Chapman University, California, USA 22-23 May, 2019 http://events.cs.bham.ac.uk/syco/4/ 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. The first SYCO was in September 2018, at the University of Birmingham. The second SYCO was in December 2018, at the University of Strathclyde. The third SYCO was in March 2019, at the University of Oxford. Each meeting attracted about 70 participants. 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 will be 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 TBA # IMPORTANT DATES All times are anywhere-on-earth. - Submission deadline: Wednesday 24 April 2019 - Author notification: Wednesday 1 May 2019 - Registration deadline: TBA - Symposium dates: Wednesday 22 and Thursday 23 May 2019 # SUBMISSIONS Submission is by EasyChair, via the following link: - https://easychair.org/conferences/?conf=syco4 Submissions should present research results in sufficient detail to allow them to be properly considered by members of the programme committee, who will assess papers with regards to significance, clarity, correctness, and scope. We encourage the submission of work in progress, as well as mature results. There are no proceedings, so work can be submitted even if it has been previously published, or has been submitted for consideration elsewhere. There is no specific formatting requirement, and no page limit, although for long submissions authors should understand that reviewers may not be able to read the entire document in detail. # PROGRAMME COMMITTEE Miriam Backens, University of Oxford Ross Duncan, University of Strathclyde and Cambridge Quantum Computing Brendan Fong, Massachusetts Institute of Technology Stefano Gogioso, University of Oxford Amar Hadzihasanovic, Kyoto University Chris Heunen, University of Edinburgh Dominic Horsman, University of Grenoble Martti Karvonen, University of Edinburgh Kohei Kishida, Dalhousie University (chair) Andre Kornell, University of California, Davis Martha Lewis, University of Amsterdam Samuel Mimram, École Polytechnique Benjamin Musto, University of Oxford Nina Otter, University of California, Los Angeles Simona Paoli, University of Leicester Dorette Pronk, Dalhousie University Mehrnoosh Sadrzadeh, Queen Mary Pawel Sobocinski, University of Southampton Joshua Tan, University of Oxford Sean Tull, University of Oxford Dominic Verdon, University of Bristol Jamie Vicary, University of Birmingham and University of Oxford Maaike Zwart, University of Oxford -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 8141 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2770 bytes --] *************************************** ** THIRD ANNOUNCEMENT ** and ** CALL FOR CONTRIBUTIONS ** ** CATEGORY THEORY 2019 ** (CT2019) ** ** UNIVERSITY OF EDINBURGH ** ** 7-13 JULY 2019 ***************************************** Dear Colleagues, We are pleased to announce the 2019 International Conference on Category Theory (CT2019), which will take place at the University of Edinburgh from 7-13 July 2019. The *Invited Speakers* are as follows: • John Baez (Riverside) • Neil Ghani (Strathclyde) • Marco Grandis (Genoa) • Simona Paoli (Leicester) • Emily Riehl (Johns Hopkins) • Mike Shulman (San Diego) • Manuela Sobral (Coimbra) Moreover, there will be a tutorial lecture on "Graphical Linear Algebra" by: • Pawel Sobocinski (Southampton) and a public event on "Inclusion-exclusion in mathematics and beyond" by: • Eugenia Cheng (Chicago) *Submission* for CT2019 is handled by EasyChair through the link: https://easychair.org/conferences/?conf=ct20190 <https://easychair.org/conferences/?conf=ct20190> The *deadline* for submissions is *May 1*, with notification of acceptance on June 1. To submit, you will need to make an EasyChair account, which is a simple process. Submissions should be in the form of a brief (1 page) abstract. *Registration* is independent of paper submission and can be done on the conference website: http://conferences.inf.ed.ac.uk/ct2019/ <http://conferences.inf.ed.ac.uk/ct2019/> The registration fee is £90 for early career participants, and £180 for established career participants, and will include tea breaks, lunches, and the conference dinner. When you register, you may also apply for *funding support*. Successful applicants will receive funding for accommodation, but not for travel or the registration fee. Registration is open until May 1 if you are applying for funding support, or June 14 if you are not. Decisions on funding support will be given in mid-May. *Inquiries* may be directed to the following email address: categorytheory2019@gmail.com <mailto:categorytheory2019@gmail.com> We look forward to seeing you in Edinburgh! The Organizing Committee: Steve Awodey, Richard Garner, Chris Heunen (chair), Tom Leinster, Christina Vasilakopoulou The Scientific Committee: Steve Awodey (chair), Julie Bergner, Gabriella Bohm, John Bourke, Eugenia Cheng, Robin Cockett, Chris Heunen, Zurab Janelidze, Dominic Verity -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 7251 bytes --]

[-- Attachment #1: Type: text/plain, Size: 4410 bytes --] ===================================================== Call for Participation and Contributed Papers ===================================================== Mathematical Logic and Constructivity: The Scope and Limits of Neutral Constructivism Stockholm, Sweden, August 20-23, 2019 http://logic.math.su.se/mloc-2019/ Deadline for contributed talks: May 31, 2019 ===================================================== With Errett Bishop's seminal work Foundations of Constructive Analysis 1967, a neutral position in the foundations of constructive mathematics emerged. It avoided Brouwer's assumptions about choice-sequences and continuity, and it did not assume that every total function on the natural numbers is computable. This made the position palatable also to the classical mathematician, and it is in the intersection of the three realms of foundations, commonly designated by the abbreviations INT, RUSS and CLASS. Successful full-fledged formal logical foundations for neutral constructivism exists, among the most well-known are Aczel-Myhill set theory and Martin-Löf type theory. Neutral constructive mathematics may also be studied for systems that make fewer ontological assumptions, which is important for reverse mathematics. To the surprise of many in constructive mathematics a new principle about sequences, the boundedness principle BD-N, was discovered, and found to be true in all the three realms without being true in neutral constructvism. Further principles of this kind are being investigated. In type theory new axioms have been discovered, such as the univalence axiom, whose constructive status was only later settled. Important questions are whether new axioms can be modelled indirectly using neutral constructive methods, or whether they can be directly justified. This workshop aims to focus on the scope and limits of neutral constructivism. The study of neutral constructivism paves the way for further developments of interactive proof systems, which is of strategic importance for verification of software, and in particular, correctness-by-construction software. INVITED SPEAKERS INCLUDE * Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand * Thierry Coquand, Chalmers and Göteborg University, Sweden * Martin Escardo, University of Birminham, England (to be confirmed) * Makoto Fujiwara, Waseda University, Japan * Nicola Gambino, Leeds University, England * Henri Lombardi, Université Franche-Comté, France * Maria Emilia Maietti, University of Padova, Italy * Takako Nemoto, JAIST, Japan * Iosif Petrakis, L-M University, Munich, Germany * Hideki Tsuiki, Kyoto University, Japan (to be confirmed) * Chuangjie Xu, L-M University, Munich, Germany * Keita Yokoyama, JAIST, Japan FURTHER SPEAKERS * Hajime Ishihara, JAIST, Japan * Anders Mörtberg, Carnegie Mellon University and Stockholm University CONTRIBUTED TALKS Proposals for contributed talks are welcome and are to be submitted via the EasyChair system: https://easychair.org/conferences/?conf=mloc19 Suggested length of abstract: half a page (max 2 pages). Deadline for contributed talks: May 31, 2019 (anywhere on Earth) Notification of acceptance: June 14, 2019 PROGRAM COMMITTEE * Hajime Ishihara, JAIST, Japan (co-chair) * Tatsuji Kawai, JAIST, Japan * Peter LeFanu Lumsdaine, Stockholm University * Anders Mörtberg, Carnegie Mellon University and Stockholm University * Erik Palmgren, Stockholm University (co-chair) REGISTRATION The workshop is free of charge, but to aid planning please register by sending the organizers an email mloc19@math.su.se<mailto:mloc19@math.su.se> with name and affilliation at the latest August 13, 2019. VENUE Department of Mathematics, Stockholm University, Sweden WEB PAGES http://logic.math.su.se/mloc-2019/ IMPORTANT DATES 2 April 2019 registration opens 31 May 2019 abstracts for contributed talks 14 June 2019 notification of acceptance 13 August 2019 registration closes 20-23 August 2019 conference -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 6424 bytes --]

In set theory there are the Zermelo universes, namely the V_\lambda for limit ordinals \lambda > \omega. They have nice closure properties in particular closure under exponentiation but what they are lacking are closure under replacement, i.e. for all A in U and f : A -> U the image of f is in U. Type theoretically this corresponds to the possibility of defining families in U by recursion over some A \in U. On the other hand in realizability models modest sets from a universe U with excellent closure properties, in particular for every A \in U and B : A -> U its sum \Sigma(A,B) \in U again. So it's very model dependent whether there exist small universes with excellent closure properties. But of course Prop or Omega is not part of such a universe. Thomas -- 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. For more options, visit https://groups.google.com/d/optout.

Registration is now open until May 17! -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- 11th International School on Rewriting (ISR'19) 1-6 July 2019, MINES ParisTech, France https://isr2019.mines-paristech.fr/ Deadline for registration: May 17 -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Rewriting is a simple yet powerful model of computation with numerous applications in computer science and many other fields: logic, mathematics, programming languages, model checking, quantum computing, biology, music... ISR'19 is hosted in the center of Paris and proposes to master students, PhD students and researchers, two parallel tracks: - basic track: introduction to first-order term rewriting and λ-calculus with lectures by Aart Middeldorp, Sarah Winkler and Femke van Raamsdonk - advanced track: lectures on rewriting theory and applications . Automated complexity analysis of term rewrite systems, Martin Avanzini . Reachability in logically constrained term rewriting systems, Ștefan Ciobâcă . Deduction modulo rewriting, Gilles Dowek . Introduction to graph rewriting, Rachid Echahed . Rewriting and music, Florent Jacquemard . Picturing quantum processes, rewriting quantum pictures, Aleks Kissinger . Stochastic graph rewriting and (executable) knowledge representation for molecular biology, Jean Krivine . Higher-order term rewriting, Cynthia Kop . Homotopy and homology of rewriting, Yves Lafont . Rewriting in theorem proving, Christopher Lynch . Formal specification and analysis of real-time systems in Real-Time Maude, Peter Csaba Ölveczky . Infinitary rewriting and streams, Hans Zantema The organizers are Frédéric Blanqui (INRIA, LSV and ENS Paris-Saclay) and Olivier Hermant (MINES ParisTech). ISR'19 is promoted by the IFIP WG1.6 and supported by the DIM RFSI, the Région Ile-de-France, INRIA, CNRS, the GDR GPL and the LSV. -- 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. For more options, visit https://groups.google.com/d/optout.

In the usual constructions of models of type theory in ZFC set theory (including homotopical ones using model categories), we take the universes to classify the sets/spaces/objects of "cardinality" bounded by some cardinal number k. To ensure these universes are closed under both Sigma- and Pi-types, we need k to be an inaccessible [1], the existence of which is not proven by ZFC. However, ZFC does prove the existence of many cardinals with weaker closure properties. For instance, it proves there are arbitrarily large regular cardinals, and indeed arbitrarily large regular cardinals closed under powers (-)^A for any fixed A. Similarly, it proves there are arbitrarily large strong limit cardinals, and indeed arbitrarily large strong limit cardinals with any fixed cofinality. If we use these cardinals to build universes in type theory, I think we can probably obtain something like this: 1. For any universe U, there is a "regular successor universe" V such that U:V, V is closed under Sigma-types and Id-types, and V is closed under Pi-types with domain in U. 2. For any universe U, there is a "strong-limit successor universe" W such that U:W, W is closed under Pi-types (including binary product types, i.e. non-dependent Sigma-types) and Id-types, and W is closed under Sigma-types with domain in U. Has anyone studied type theory with universes like this? Or more generally type theories containing universes with weaker closure properties under type formers? And what can and can't we do in such a type theory? One thing we (apparently) can't do would be to iterate (e.g. by Nat-rec) some construction on types that sends a type X to some type that includes X in the domain of both a Sigma and a Pi. Are there naturally-occurring examples of such? There are of course definitions we use all the time that do involve a type in both the domain of a Sigma and a Pi, such as IsContr(X) = Sigma(x:X) Pi(y:X) (x=y). In this case, there is an equivalent definition of IsContr that remains in the same strong-limit universe, IsContr(X) = X * Pi(x,y:X) (x=y). Thus, we can define the h-level hierarchy by recursion on n in any strong-limit universe. Are there other such constructions that irreducibly go up a universe level, and would the resulting inability to iterate them be a problem? (Regarding HITs, in set-theoretic models I think both regular and strong-limit universes would be closed under simple ones like pushouts, and there should at least exist regular universes closed under fancier recursive HITs. Of course in homotopical models we don't yet know how to obtain even inaccessible universes closed under HITs, but we might hope that if that problem is solved then the solution would work for arbitrarily large regular universes as well. That would for instance allow us to define spheres and truncations recursively on n.) [1]: Apparently one can also construct models of *predicative* type theory in much weaker classical set theories like Kripke-Platek, with "recursive inaccessibles" used instead of actual inaccessibles. However, if we add impredicative axioms like propositional resizing, then I think the use of ZFC with true inaccessibles seems more likely to be necessary. -- 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. For more options, visit https://groups.google.com/d/optout.

************************************************************** Second Call for Submissions -- Extended Deadline INTERNATIONAL CONFERENCE ON HOMOTOPY TYPE THEORY 12-17 August 2019 Carnegie Mellon University Pittsburgh USA https://hott.github.io/HoTT-2019 ************************************************************** Submissions of talks are open for the International Homotopy Type Theory conference (HoTT 2019), to be held from August 12th to 17th, 2019, at Carnegie Mellon University in Pittsburgh, USA. Contributions are welcome in all areas related to homotopy type theory, including but not limited to: * Homotopical and higher-categorical semantics of type theory * Synthetic homotopy theory * Applications of univalence and higher inductive types * Cubical type theories and cubical models * Formalization of mathematics and computer science in homotopy type theory / univalent foundations Please submit 1-paragraph abstracts through the EasyChair conference system here: https://easychair.org/conferences/?conf=hott2019 The submission deadline has been EXTENDED to 15 MAY 2019; we expect to notify accepted submissions by 1 June. If you need an earlier decision for some reason (e.g. to apply for funding), please submit your abstract by 15 APRIL and send an email to hott2019conference@gmail.com notifying us that you need an early decision. This conference is run on the "mathematics model" rather than the "computer science model": full papers will not be submitted, submissions will not be refereed, and submission is not a publication (although a proceedings volume might be organized afterwards). More information, including registration, accomodation options, and travel, will be available as the conference approaches at the web site https://hott.github.io/HoTT-2019/ . Please email hott2019conference@gmail.com with any questions. INVITED SPEAKERS Ulrik Buchholtz (TU Darmstadt, Germany) Dan Licata (Wesleyan University, USA) Andrew Pitts (University of Cambridge, UK) Emily Riehl (Johns Hopkins University, USA) Christian Sattler (University of Gothenburg, Sweden) Karol Szumilo (University of Leeds, UK) IMPORTANT DATES Submission deadline: 15 May (or 15 April for early notification) Registration Opens: 1 April Regular Notification Date: 1 June Final abstracts due: 15 June Early Registration deadline: 1 July (reduced fee) Late Registration deadline: 1 August (increased fee) Conference: 12-17 August 2019 SUMMER SCHOOL There will also be an associated Homotopy Type Theory Summer School in the preceding week, August 7th to 10th. The instructors and topics will be: Cubical methods: Anders Mortberg (Carnegie Mellon University, USA) Formalization in Agda: Guillaume Brunerie (Stockholm University, Sweden) Formalization in Coq: Kristina Sojakova (Cornell University, USA) Higher topos theory: Mathieu Anel (Carnegie Mellon University, USA) Semantics of type theory: Jonas Frey (Carnegie Mellon University, USA) Synthetic homotopy theory: Egbert Rijke (University of Illinois, USA) REGISTRATION Registration for the conference and the summer school will open on April 1, 2019. A limited amount of financial support will be available for students and postdoctoral researchers. SCIENTIFIC COMMITTEE Steve Awodey (Carnegie Mellon University, USA) Andrej Bauer (University of Ljubljana, Slovenia) Thierry Coquand (University of Gothenburg, Sweden) Nicola Gambino (University of Leeds, UK) Peter LeFanu Lumsdaine (Stockholm University, Sweden) Michael Shulman (University of San Diego, USA), chair We look forward to seeing you in Pittsburgh! -- 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. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 6303 bytes --] Jonas found a flaw... Thanks Jonas! (and forget what I said above) With kind regards, Egbert On Mon, Mar 18, 2019 at 11:40 PM Egbert Rijke <e.m.rijke@gmail.com> wrote: > So I guess you're right then... and I made a mistake. Thanks so much for > pointing it out! > > On Mon, Mar 18, 2019 at 11:33 PM Egbert Rijke <e.m.rijke@gmail.com> wrote: > >> Wait a minute... in the proof that it is Sigma-closed I do have the >> diagrams the wrong way around. Yikes! >> >> On Mon, Mar 18, 2019 at 11:27 PM Egbert Rijke <e.m.rijke@gmail.com> >> wrote: >> >>> Hi Jonas, >>> >>> The last question is easiest: I do everything internally, so maybe it is >>> different for external factorization systems. That I don't know. >>> >>> The first thing to show is that from a reflective factorization system >>> you get a modality. The modal types are the types for which the terminal >>> projection is in the right class. Then by factoring the terminal projection >>> you get the modal operator. Let's call it L. This gives a reflective >>> subuniverse (I believe you have no problem with this fact, but the proof is >>> easy, by orthogonality). Then you need to show that this reflective >>> subuniverse is closed under Sigma. If you have a family of modal types over >>> a modal type, then the Sigma should also be modal. Since the right class is >>> closed under composition, it suffices to show that the projection map is a >>> right map. This can be done by showing that it is right orthogonal to any >>> map in the left class. So indeed I claim that any reflective factorization >>> system gives rise to a modality in this way. >>> >>> Ah, and since this is now a private message I can attach the proof. >>> Hopefully it is not false... >>> >>> Best, >>> Egbert >>> >>> >>> >>> On Mon, Mar 18, 2019 at 11:15 PM Jonas Frey <jonas743@gmail.com> wrote: >>> >>>> Hi Egbert (answering privately), >>>> >>>> I think that's weird since at least in the 1-categorical setting, every >>>> reflection on say a locally presentable category determines a reflective >>>> factorization system whose left class consists of those maps that are >>>> inverted by the reflection (that's in the cassidy-hebert-kelly paper). I >>>> suppose that's also true for ∞-presentable categories so e.g. there's a >>>> reflective facsys whose left class consists of those maps that are inverted >>>> by localization at the degree two map of the circle. >>>> >>>> Are you saying that this rfsys is also the "formally etale facsys" of >>>> some modality? >>>> >>>> More generally, are you saying your claim also holds up for other >>>> infty-toposes than spaces? In this case, do you want the notion of >>>> factorization system to be understood internally? >>>> >>>> Jonas >>>> >>>> >>>> On Tue, 19 Mar 2019 at 00:01, Egbert Rijke <e.m.rijke@gmail.com> wrote: >>>> >>>>> Dear all, >>>>> >>>>> During my lecture on modal descent someone in the audience (my >>>>> apologies, I forgot who it was) asked the question >>>>> <https://www.youtube.com/watch?v=InaRkqKdyp4&t=900s> whether >>>>> reflective factorization systems (i.e. orthogonal factorization systems for >>>>> which the left class satisfies the 3-for-2 property) also characterize >>>>> modalities. I thought this was a very nice question, because we have a >>>>> theorem like that for stable factorization systems (i.e. orthogonal >>>>> factorization systems for which the left class is stable under pullback). >>>>> >>>>> During the lecture I didn't know the answer, but now I do: It is >>>>> indeed the case that modalities are equivalently described as reflective >>>>> factorization systems. I wanted to attach hand-written notes containing the >>>>> proof, but the files are too large to be contained in a message to this >>>>> google group. I'll write it up properly soon. >>>>> >>>>> In particular it follows that the poset of stable factorization >>>>> systems is the same as the poset of reflective factorization systems, even >>>>> though there are subtle differences between the stable factorization system >>>>> of a modality, and the reflective factorization system of a modality (i.e. >>>>> under this equivalence the left and right classes have to change slightly). >>>>> >>>>> My lecture is available via the link Felix just shared. >>>>> >>>>> With kind regards, >>>>> Egbert >>>>> >>>>> On Mon, Mar 18, 2019 at 11:53 AM Felix Wellen <felix.wellen@gmail.com> >>>>> wrote: >>>>> >>>>>> Dear all, >>>>>> >>>>>> I just finished uploading the recordings of last week's workshop >>>>>> >>>>>> Geometry in Modal HoTT >>>>>> <http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html#schedule> >>>>>> >>>>>> to youtube <https://www.youtube.com/channel/UCfQdw845tAduRwW6FnWC9KQ>. >>>>>> I'm afraid the audio is not good, but with enough volume it should be >>>>>> possible to understand everything. >>>>>> You can get an overview of the talks on the abstracts-page: >>>>>> >>>>>> http://www.andrew.cmu.edu/user/fwellen/abstracts.html >>>>>> >>>>>> All the best, >>>>>> Felix >>>>>> >>>>>> -- >>>>>> 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. >>>>>> For more options, visit https://groups.google.com/d/optout. >>>>>> >>>>> >>>>> >>>>> -- >>>>> egbertrijke.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. >>>>> For more options, visit https://groups.google.com/d/optout. >>>>> >>>> >>> >>> >> >> -- >> egbertrijke.com >> > > > -- > egbertrijke.com > -- egbertrijke.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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 10385 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2558 bytes --] Dear all, During my lecture on modal descent someone in the audience (my apologies, I forgot who it was) asked the question <https://www.youtube.com/watch?v=InaRkqKdyp4&t=900s> whether reflective factorization systems (i.e. orthogonal factorization systems for which the left class satisfies the 3-for-2 property) also characterize modalities. I thought this was a very nice question, because we have a theorem like that for stable factorization systems (i.e. orthogonal factorization systems for which the left class is stable under pullback). During the lecture I didn't know the answer, but now I do: It is indeed the case that modalities are equivalently described as reflective factorization systems. I wanted to attach hand-written notes containing the proof, but the files are too large to be contained in a message to this google group. I'll write it up properly soon. In particular it follows that the poset of stable factorization systems is the same as the poset of reflective factorization systems, even though there are subtle differences between the stable factorization system of a modality, and the reflective factorization system of a modality (i.e. under this equivalence the left and right classes have to change slightly). My lecture is available via the link Felix just shared. With kind regards, Egbert On Mon, Mar 18, 2019 at 11:53 AM Felix Wellen <felix.wellen@gmail.com> wrote: > Dear all, > > I just finished uploading the recordings of last week's workshop > > Geometry in Modal HoTT > <http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html#schedule> > > to youtube <https://www.youtube.com/channel/UCfQdw845tAduRwW6FnWC9KQ>. > I'm afraid the audio is not good, but with enough volume it should be > possible to understand everything. > You can get an overview of the talks on the abstracts-page: > > http://www.andrew.cmu.edu/user/fwellen/abstracts.html > > All the best, > Felix > > -- > 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. > For more options, visit https://groups.google.com/d/optout. > -- egbertrijke.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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 3891 bytes --]

The Department of Mathematics at Stockholm University invites applications for a PhD position in Computational Mathematics. A prospective student will have the opportunity to engage in exciting research related to programming logic, type theory, constructive mathematics and category theoretic foundations. The student will be part of the newly founded Computational Mathematics division. It will also be possible to collaborate with other groups in the department, such as the Mathematical Logic group (with experts on constructive mathematics and type theory like Per Martin-Löf, Erik Palmgren and Peter LeFanu Lumsdaine) and the Algebra, Geometry, Topology, and Combinatorics group. For further information and instructions on how to apply see https://www.su.se/english/about/working-at-su/phd?rmpage=job&rmjob=8652&rmlang=UK The deadline for application is April 23, 2019. If you are interested in applying and have any questions feel free to contact me. -- Anders Mörtberg <anders.mortberg@math.su.se> -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 788 bytes --] Dear all, I just finished uploading the recordings of last week's workshop Geometry in Modal HoTT <http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html#schedule> to youtube <https://www.youtube.com/channel/UCfQdw845tAduRwW6FnWC9KQ>. I'm afraid the audio is not good, but with enough volume it should be possible to understand everything. You can get an overview of the talks on the abstracts-page: http://www.andrew.cmu.edu/user/fwellen/abstracts.html All the best, Felix -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 1245 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1202 bytes --] I’ve been asked to pass along this job announcement for a friend. It’s a great opportunity to join a research community that I really admire in a beautiful part of the world. Please apply! Details below, Emily -- Greetings all, The Centre of Australian Category Theory at Macquarie University is advertising a 2-year postdoc in relation to a project entitled “Working synthetically in higher categorical structures”. It would be particularly suitable for people who work in higher categories, 2-categories, or homotopy type theory. Further information is available here http://jobs.mq.edu.au/cw/en/job/505375/postdoctoral-research-fellow-in-category-theory <http://jobs.mq.edu.au/cw/en/job/505375/postdoctoral-research-fellow-in-category-theory> or feel free to get in touch with Richard Garner, Ross Street, Dominic Verity, or me. Regards, Steve Lack. -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 3292 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 10441 bytes --] On Friday, 8 March 2019 15:13:14 UTC, dlicata wrote: > > nice! the negation trick is clever. > Yes, this is really nice. Martin, I don’t understand why this situation is any different than natural > numbers, though. If I have a closed term of type nat, I can normalize it, > but then I (externally) need to read through all of the successors to > figure out what number it is. (Or maybe I can only weak head normalize it, > in which case I need to interleave further weak head normalization after > every successor.) Is this an unbounded search? The parallel is to read > “hcom []” as successor and “|x,a|” as zero. > > Except that you would have different normal forms for the same thing, and this thing would be prefixed by an unbounded number of *printed* clock ticks. It is not right to say that unbounded search is needed, I agree. But it wouldn't be pleasant to have to see 10^6 ticks. I would rather wait for 10^6 units of time (which should be fast) and then see the answer than see a million hcomp's followed by the answer on my computer screen . :-) Fortunately, Anders says that the clock ticks are not printed in the version of cubical type theory implemented by Agda --cubical, which is nice! Martin > -Dan > > > On Mar 8, 2019, at 9:59 AM, Anders Mortberg <andersm...@gmail.com > <javascript:>> wrote: > > > > In fact, in Cubical Agda you will not get these hcomp's with empty > > systems. The reason is that because of the way hcomp works in Agda > > there is a very nice trick to implement the "generalized hcomp" > > operation of the paper that Dan linked to. I summarized the trick in: > > > > https://github.com/agda/agda/issues/3415 > > > > I added this to Agda some month ago and it should be possible to > > update Simon's canonicity proof to get a stronger result saying that > > the only elements of HITs in the empty context are point constructors > > (like in the AFH paper). For this to work you also have to impose a > > "validity" constraint (Def 12 in the ccctt paper Dan linked to) so > > that empty systems cannot result from substitutions. This is currently > > not done in Cubical Agda, but if you start with a term with only valid > > systems then you should never get an empty system. > > > > So the extraction of witnesses from existence statements should work > > as Martín said in Cubical Agda. > > > > -- > > Anders > > > > On Thu, Mar 7, 2019 at 6:23 PM Martín Hötzel Escardó > > <escardo...@gmail.com <javascript:>> wrote: > >> > >> And this is a wildly speculative question. If we used Andrew Swan's > identity type derived from the cubical path type only, as in the abstract > library file > https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.agda) > would we still get this phenomenon? Maybe not? What I mean is that we use > normal Agda, together with what is offered in that file and nothing else > (so that we are using HoTT book axiomatic type theory). Martin > >> > >> On Thursday, 7 March 2019 23:01:33 UTC, Martín Hötzel Escardó wrote: > >>> > >>> Oh, this is annoying, because it seems to mean that we would need > unbounded search (to drop all "hcom []"'s) until we can read the |x,a|, > which is against the spirit of, say, Martin-Loef type theories. Martin > >>> > >>> On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote: > >>>> > >>>> That would be true if the term you are normalizing is in the empty > interval context, and the cubical type theory has “empty system regularity” > (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). > >>>> > >>>> Otherwise, if you evaluate something in the empty interval context, > you might see something like > >>>> hcom [] (hcom [] (hcom [] (hcom [] (… |x,a| … )))) > >>>> with |x,a| in there somewhere. In HITs, Kan composition is treated > as a constructor of the type, and though there are no interesting lines to > compose in the empty interval context, the uninteresting compositions don’t > vanish in all flavors of cubical type theory. > >>>> > >>>>> On Mar 7, 2019, at 5:41 PM, Martín Hötzel Escardó < > escardo...@gmail.com> wrote: > >>>>> > >>>>> So I presume that when we ask cubical Agda to normalize a term of > type || Sigma (x:X), A x || we will get a term of the form |x,a| and so we > will see the x in normal form, where |-| is the map into the truncation, > right? Martin. > >>>>> > >>>>> On Thursday, 7 March 2019 21:52:12 UTC, Anders Mörtberg wrote: > >>>>> The existence property is proved for CCHM cubicaltt by Simon in: > >>>>> > >>>>> https://arxiv.org/abs/1607.04156 > >>>>> > >>>>> See corollary 5.2. This works a bit more generally than what Martín > said, in particular in any context with only dimension variables we can > compute a witness to an existence. So if in context G = i_1 : II, ..., i_n > : II (possibly empty) we have: > >>>>> > >>>>> G |- t : exists (x : X), A(x) > >>>>> > >>>>> then we can compute G |- u : X so that G |- B(u). > >>>>> > >>>>> -- > >>>>> Anders > >>>>> > >>>>> On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Martín Hötzel > Escardó wrote: > >>>>> I got confused now. :-) > >>>>> > >>>>> Seriously now, what you say seems related to the fact that from a > proof |- t : || X || in the empty context, you get |- x : X in cubical type > theory. This follows from Simon's canonicity result (at least for X=natural > numbers), and is like the so-called "existence property" in the internal > language of the free elementary topos. This says that from a proof |- > exists (x:X), A x in the empty context, you get |- x : X and |- A x. This > says that exists in the empty context behaves like Sigma. But only in the > empty context, because otherwise it behaves like "local existence" as in > Kripke-Joyal semantics. > >>>>> > >>>>> Martin > >>>>> > >>>>> On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote: > >>>>> Just in case anyone reading this thread later is confused about a > more beginner point than the ones Nicolai and Martin made, one possible > stumbling block here is that, if someone means “is inhabited” in an > external sense (there is a closed term of that type), then the answer is > yes (at least in some models): if ||A|| is inhabited then A is inhabited. > For example, in cubical models with canonicity, it is true that a closed > term of type ||A|| evaluates to a value that has as a subterm a closed term > of type A (the other values of ||A|| are some “formal compositions” of > values of ||A||, but there has to be an |a| in there at the base case). > This is consistent with what Martin and Nicolai said because “if A is > inhabited then B is inhabited” (in this external sense) doesn’t necessarily > mean there is a map A -> B internally. > >>>>> > >>>>> -Dan > >>>>> > >>>>>> On Mar 5, 2019, at 6:07 PM, Martín Hötzel Escardó < > escardo...@gmail.com> wrote: > >>>>>> > >>>>>> Or you can read the paper https://lmcs.episciences.org/3217/ > regarding what Nicolai said. > >>>>>> > >>>>>> Moreover, in the HoTT book, it is shown that if || X||->X holds for > all X, then univalence can't hold. (It is global choice, which can't be > invariant under equivalence.) > >>>>>> > >>>>>> The above paper shows that unrestricted ||X||->X it gives excluded > middle. > >>>>>> > >>>>>> However, for a lot of kinds of types one can show that ||X||->X > does hold. For example, if they have a constant endo-function. Moreover, > for any type X, the availability of ||X||->X is logically equivalent to the > availability of a constant map X->X (before we know whether X has a point > or not, in which case the availability of a constant endo-map is trivial). > >>>>>> > >>>>>> Martin > >>>>>> > >>>>>> On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote: > >>>>>> You can't have a function which, for all A, gives you ||A|| -> A. > See the exercises 3.11 and 3.12! > >>>>>> -- Nicolai > >>>>>> > >>>>>> On 05/03/19 22:31, Jean Joseph wrote: > >>>>>>> Hi, > >>>>>>> > >>>>>>> From the HoTT book, the truncation of any type A has two > constructors: > >>>>>>> > >>>>>>> 1) for any a : A, there is |a| : ||A|| > >>>>>>> 2) for any x,y : ||A||, x = y. > >>>>>>> > >>>>>>> I get that if A is inhabited, then ||A|| is inhabited by (1). But > is it true that, if ||A|| is inhabited, then A is inhabited? > >>>>>>> -- > >>>>>>> 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 > <javascript:>. > >>>>>>> For more options, visit https://groups.google.com/d/optout. > >>>>>> > >>>>>> > >>>>>> -- > >>>>>> 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 > <javascript:>. > >>>>>> For more options, visit https://groups.google.com/d/optout. > >>>>> > >>>>> > >>>>> -- > >>>>> 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 > <javascript:>. > >>>>> For more options, visit https://groups.google.com/d/optout. > >>>> > >> -- > >> 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 <javascript:>. > > >> For more options, visit https://groups.google.com/d/optout. > > -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 17374 bytes --]

nice! the negation trick is clever. Martin, I don’t understand why this situation is any different than natural numbers, though. If I have a closed term of type nat, I can normalize it, but then I (externally) need to read through all of the successors to figure out what number it is. (Or maybe I can only weak head normalize it, in which case I need to interleave further weak head normalization after every successor.) Is this an unbounded search? The parallel is to read “hcom []” as successor and “|x,a|” as zero. -Dan > On Mar 8, 2019, at 9:59 AM, Anders Mortberg <andersmortberg@gmail.com> wrote: > > In fact, in Cubical Agda you will not get these hcomp's with empty > systems. The reason is that because of the way hcomp works in Agda > there is a very nice trick to implement the "generalized hcomp" > operation of the paper that Dan linked to. I summarized the trick in: > > https://github.com/agda/agda/issues/3415 > > I added this to Agda some month ago and it should be possible to > update Simon's canonicity proof to get a stronger result saying that > the only elements of HITs in the empty context are point constructors > (like in the AFH paper). For this to work you also have to impose a > "validity" constraint (Def 12 in the ccctt paper Dan linked to) so > that empty systems cannot result from substitutions. This is currently > not done in Cubical Agda, but if you start with a term with only valid > systems then you should never get an empty system. > > So the extraction of witnesses from existence statements should work > as Martín said in Cubical Agda. > > -- > Anders > > On Thu, Mar 7, 2019 at 6:23 PM Martín Hötzel Escardó > <escardo.martin@gmail.com> wrote: >> >> And this is a wildly speculative question. If we used Andrew Swan's identity type derived from the cubical path type only, as in the abstract library file https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.agda) would we still get this phenomenon? Maybe not? What I mean is that we use normal Agda, together with what is offered in that file and nothing else (so that we are using HoTT book axiomatic type theory). Martin >> >> On Thursday, 7 March 2019 23:01:33 UTC, Martín Hötzel Escardó wrote: >>> >>> Oh, this is annoying, because it seems to mean that we would need unbounded search (to drop all "hcom []"'s) until we can read the |x,a|, which is against the spirit of, say, Martin-Loef type theories. Martin >>> >>> On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote: >>>> >>>> That would be true if the term you are normalizing is in the empty interval context, and the cubical type theory has “empty system regularity” (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). >>>> >>>> Otherwise, if you evaluate something in the empty interval context, you might see something like >>>> hcom [] (hcom [] (hcom [] (hcom [] (… |x,a| … )))) >>>> with |x,a| in there somewhere. In HITs, Kan composition is treated as a constructor of the type, and though there are no interesting lines to compose in the empty interval context, the uninteresting compositions don’t vanish in all flavors of cubical type theory. >>>> >>>>> On Mar 7, 2019, at 5:41 PM, Martín Hötzel Escardó <escardo...@gmail.com> wrote: >>>>> >>>>> So I presume that when we ask cubical Agda to normalize a term of type || Sigma (x:X), A x || we will get a term of the form |x,a| and so we will see the x in normal form, where |-| is the map into the truncation, right? Martin. >>>>> >>>>> On Thursday, 7 March 2019 21:52:12 UTC, Anders Mörtberg wrote: >>>>> The existence property is proved for CCHM cubicaltt by Simon in: >>>>> >>>>> https://arxiv.org/abs/1607.04156 >>>>> >>>>> See corollary 5.2. This works a bit more generally than what Martín said, in particular in any context with only dimension variables we can compute a witness to an existence. So if in context G = i_1 : II, ..., i_n : II (possibly empty) we have: >>>>> >>>>> G |- t : exists (x : X), A(x) >>>>> >>>>> then we can compute G |- u : X so that G |- B(u). >>>>> >>>>> -- >>>>> Anders >>>>> >>>>> On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Martín Hötzel Escardó wrote: >>>>> I got confused now. :-) >>>>> >>>>> Seriously now, what you say seems related to the fact that from a proof |- t : || X || in the empty context, you get |- x : X in cubical type theory. This follows from Simon's canonicity result (at least for X=natural numbers), and is like the so-called "existence property" in the internal language of the free elementary topos. This says that from a proof |- exists (x:X), A x in the empty context, you get |- x : X and |- A x. This says that exists in the empty context behaves like Sigma. But only in the empty context, because otherwise it behaves like "local existence" as in Kripke-Joyal semantics. >>>>> >>>>> Martin >>>>> >>>>> On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote: >>>>> Just in case anyone reading this thread later is confused about a more beginner point than the ones Nicolai and Martin made, one possible stumbling block here is that, if someone means “is inhabited” in an external sense (there is a closed term of that type), then the answer is yes (at least in some models): if ||A|| is inhabited then A is inhabited. For example, in cubical models with canonicity, it is true that a closed term of type ||A|| evaluates to a value that has as a subterm a closed term of type A (the other values of ||A|| are some “formal compositions” of values of ||A||, but there has to be an |a| in there at the base case). This is consistent with what Martin and Nicolai said because “if A is inhabited then B is inhabited” (in this external sense) doesn’t necessarily mean there is a map A -> B internally. >>>>> >>>>> -Dan >>>>> >>>>>> On Mar 5, 2019, at 6:07 PM, Martín Hötzel Escardó <escardo...@gmail.com> wrote: >>>>>> >>>>>> Or you can read the paper https://lmcs.episciences.org/3217/ regarding what Nicolai said. >>>>>> >>>>>> Moreover, in the HoTT book, it is shown that if || X||->X holds for all X, then univalence can't hold. (It is global choice, which can't be invariant under equivalence.) >>>>>> >>>>>> The above paper shows that unrestricted ||X||->X it gives excluded middle. >>>>>> >>>>>> However, for a lot of kinds of types one can show that ||X||->X does hold. For example, if they have a constant endo-function. Moreover, for any type X, the availability of ||X||->X is logically equivalent to the availability of a constant map X->X (before we know whether X has a point or not, in which case the availability of a constant endo-map is trivial). >>>>>> >>>>>> Martin >>>>>> >>>>>> On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote: >>>>>> You can't have a function which, for all A, gives you ||A|| -> A. See the exercises 3.11 and 3.12! >>>>>> -- Nicolai >>>>>> >>>>>> On 05/03/19 22:31, Jean Joseph wrote: >>>>>>> Hi, >>>>>>> >>>>>>> From the HoTT book, the truncation of any type A has two constructors: >>>>>>> >>>>>>> 1) for any a : A, there is |a| : ||A|| >>>>>>> 2) for any x,y : ||A||, x = y. >>>>>>> >>>>>>> I get that if A is inhabited, then ||A|| is inhabited by (1). But is it true that, if ||A|| is inhabited, then A is inhabited? >>>>>>> -- >>>>>>> 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. >>>>>>> For more options, visit https://groups.google.com/d/optout. >>>>>> >>>>>> >>>>>> -- >>>>>> 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. >>>>>> For more options, visit https://groups.google.com/d/optout. >>>>> >>>>> >>>>> -- >>>>> 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. >>>>> For more options, visit https://groups.google.com/d/optout. >>>> >> -- >> 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. >> For more options, visit https://groups.google.com/d/optout. -- 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. For more options, visit https://groups.google.com/d/optout.

In fact, in Cubical Agda you will not get these hcomp's with empty systems. The reason is that because of the way hcomp works in Agda there is a very nice trick to implement the "generalized hcomp" operation of the paper that Dan linked to. I summarized the trick in: https://github.com/agda/agda/issues/3415 I added this to Agda some month ago and it should be possible to update Simon's canonicity proof to get a stronger result saying that the only elements of HITs in the empty context are point constructors (like in the AFH paper). For this to work you also have to impose a "validity" constraint (Def 12 in the ccctt paper Dan linked to) so that empty systems cannot result from substitutions. This is currently not done in Cubical Agda, but if you start with a term with only valid systems then you should never get an empty system. So the extraction of witnesses from existence statements should work as Martín said in Cubical Agda. -- Anders On Thu, Mar 7, 2019 at 6:23 PM Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: > > And this is a wildly speculative question. If we used Andrew Swan's identity type derived from the cubical path type only, as in the abstract library file https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.agda) would we still get this phenomenon? Maybe not? What I mean is that we use normal Agda, together with what is offered in that file and nothing else (so that we are using HoTT book axiomatic type theory). Martin > > On Thursday, 7 March 2019 23:01:33 UTC, Martín Hötzel Escardó wrote: >> >> Oh, this is annoying, because it seems to mean that we would need unbounded search (to drop all "hcom []"'s) until we can read the |x,a|, which is against the spirit of, say, Martin-Loef type theories. Martin >> >> On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote: >>> >>> That would be true if the term you are normalizing is in the empty interval context, and the cubical type theory has “empty system regularity” (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). >>> >>> Otherwise, if you evaluate something in the empty interval context, you might see something like >>> hcom [] (hcom [] (hcom [] (hcom [] (… |x,a| … )))) >>> with |x,a| in there somewhere. In HITs, Kan composition is treated as a constructor of the type, and though there are no interesting lines to compose in the empty interval context, the uninteresting compositions don’t vanish in all flavors of cubical type theory. >>> >>> > On Mar 7, 2019, at 5:41 PM, Martín Hötzel Escardó <escardo...@gmail.com> wrote: >>> > >>> > So I presume that when we ask cubical Agda to normalize a term of type || Sigma (x:X), A x || we will get a term of the form |x,a| and so we will see the x in normal form, where |-| is the map into the truncation, right? Martin. >>> > >>> > On Thursday, 7 March 2019 21:52:12 UTC, Anders Mörtberg wrote: >>> > The existence property is proved for CCHM cubicaltt by Simon in: >>> > >>> > https://arxiv.org/abs/1607.04156 >>> > >>> > See corollary 5.2. This works a bit more generally than what Martín said, in particular in any context with only dimension variables we can compute a witness to an existence. So if in context G = i_1 : II, ..., i_n : II (possibly empty) we have: >>> > >>> > G |- t : exists (x : X), A(x) >>> > >>> > then we can compute G |- u : X so that G |- B(u). >>> > >>> > -- >>> > Anders >>> > >>> > On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Martín Hötzel Escardó wrote: >>> > I got confused now. :-) >>> > >>> > Seriously now, what you say seems related to the fact that from a proof |- t : || X || in the empty context, you get |- x : X in cubical type theory. This follows from Simon's canonicity result (at least for X=natural numbers), and is like the so-called "existence property" in the internal language of the free elementary topos. This says that from a proof |- exists (x:X), A x in the empty context, you get |- x : X and |- A x. This says that exists in the empty context behaves like Sigma. But only in the empty context, because otherwise it behaves like "local existence" as in Kripke-Joyal semantics. >>> > >>> > Martin >>> > >>> > On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote: >>> > Just in case anyone reading this thread later is confused about a more beginner point than the ones Nicolai and Martin made, one possible stumbling block here is that, if someone means “is inhabited” in an external sense (there is a closed term of that type), then the answer is yes (at least in some models): if ||A|| is inhabited then A is inhabited. For example, in cubical models with canonicity, it is true that a closed term of type ||A|| evaluates to a value that has as a subterm a closed term of type A (the other values of ||A|| are some “formal compositions” of values of ||A||, but there has to be an |a| in there at the base case). This is consistent with what Martin and Nicolai said because “if A is inhabited then B is inhabited” (in this external sense) doesn’t necessarily mean there is a map A -> B internally. >>> > >>> > -Dan >>> > >>> > > On Mar 5, 2019, at 6:07 PM, Martín Hötzel Escardó <escardo...@gmail.com> wrote: >>> > > >>> > > Or you can read the paper https://lmcs.episciences.org/3217/ regarding what Nicolai said. >>> > > >>> > > Moreover, in the HoTT book, it is shown that if || X||->X holds for all X, then univalence can't hold. (It is global choice, which can't be invariant under equivalence.) >>> > > >>> > > The above paper shows that unrestricted ||X||->X it gives excluded middle. >>> > > >>> > > However, for a lot of kinds of types one can show that ||X||->X does hold. For example, if they have a constant endo-function. Moreover, for any type X, the availability of ||X||->X is logically equivalent to the availability of a constant map X->X (before we know whether X has a point or not, in which case the availability of a constant endo-map is trivial). >>> > > >>> > > Martin >>> > > >>> > > On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote: >>> > > You can't have a function which, for all A, gives you ||A|| -> A. See the exercises 3.11 and 3.12! >>> > > -- Nicolai >>> > > >>> > > On 05/03/19 22:31, Jean Joseph wrote: >>> > >> Hi, >>> > >> >>> > >> From the HoTT book, the truncation of any type A has two constructors: >>> > >> >>> > >> 1) for any a : A, there is |a| : ||A|| >>> > >> 2) for any x,y : ||A||, x = y. >>> > >> >>> > >> I get that if A is inhabited, then ||A|| is inhabited by (1). But is it true that, if ||A|| is inhabited, then A is inhabited? >>> > >> -- >>> > >> 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. >>> > >> For more options, visit https://groups.google.com/d/optout. >>> > > >>> > > >>> > > -- >>> > > 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. >>> > > For more options, visit https://groups.google.com/d/optout. >>> > >>> > >>> > -- >>> > 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. >>> > For more options, visit https://groups.google.com/d/optout. >>> > -- > 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. > For more options, visit https://groups.google.com/d/optout. -- 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. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 7219 bytes --] And this is a wildly speculative question. If we used Andrew Swan's identity type derived from the cubical path type only, as in the abstract library file https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.agda) would we still get this phenomenon? Maybe not? What I mean is that we use normal Agda, together with what is offered in that file and nothing else (so that we are using HoTT book axiomatic type theory). Martin On Thursday, 7 March 2019 23:01:33 UTC, Martín Hötzel Escardó wrote: > > Oh, this is annoying, because it seems to mean that we would need > unbounded search (to drop all "hcom []"'s) until we can read the |x,a|, > which is against the spirit of, say, Martin-Loef type theories. Martin > > On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote: >> >> That would be true if the term you are normalizing is in the empty >> interval context, and the cubical type theory has “empty system regularity” >> (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). >> >> Otherwise, if you evaluate something in the empty interval context, you >> might see something like >> hcom [] (hcom [] (hcom [] (hcom [] (… |x,a| … )))) >> with |x,a| in there somewhere. In HITs, Kan composition is treated as a >> constructor of the type, and though there are no interesting lines to >> compose in the empty interval context, the uninteresting compositions don’t >> vanish in all flavors of cubical type theory. >> >> > On Mar 7, 2019, at 5:41 PM, Martín Hötzel Escardó <escardo...@gmail.com> >> wrote: >> > >> > So I presume that when we ask cubical Agda to normalize a term of type >> || Sigma (x:X), A x || we will get a term of the form |x,a| and so we will >> see the x in normal form, where |-| is the map into the truncation, right? >> Martin. >> > >> > On Thursday, 7 March 2019 21:52:12 UTC, Anders Mörtberg wrote: >> > The existence property is proved for CCHM cubicaltt by Simon in: >> > >> > https://arxiv.org/abs/1607.04156 >> > >> > See corollary 5.2. This works a bit more generally than what Martín >> said, in particular in any context with only dimension variables we can >> compute a witness to an existence. So if in context G = i_1 : II, ..., i_n >> : II (possibly empty) we have: >> > >> > G |- t : exists (x : X), A(x) >> > >> > then we can compute G |- u : X so that G |- B(u). >> > >> > -- >> > Anders >> > >> > On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Martín Hötzel Escardó >> wrote: >> > I got confused now. :-) >> > >> > Seriously now, what you say seems related to the fact that from a proof >> |- t : || X || in the empty context, you get |- x : X in cubical type >> theory. This follows from Simon's canonicity result (at least for X=natural >> numbers), and is like the so-called "existence property" in the internal >> language of the free elementary topos. This says that from a proof |- >> exists (x:X), A x in the empty context, you get |- x : X and |- A x. This >> says that exists in the empty context behaves like Sigma. But only in the >> empty context, because otherwise it behaves like "local existence" as in >> Kripke-Joyal semantics. >> > >> > Martin >> > >> > On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote: >> > Just in case anyone reading this thread later is confused about a more >> beginner point than the ones Nicolai and Martin made, one possible >> stumbling block here is that, if someone means “is inhabited” in an >> external sense (there is a closed term of that type), then the answer is >> yes (at least in some models): if ||A|| is inhabited then A is inhabited. >> For example, in cubical models with canonicity, it is true that a closed >> term of type ||A|| evaluates to a value that has as a subterm a closed term >> of type A (the other values of ||A|| are some “formal compositions” of >> values of ||A||, but there has to be an |a| in there at the base case). >> This is consistent with what Martin and Nicolai said because “if A is >> inhabited then B is inhabited” (in this external sense) doesn’t necessarily >> mean there is a map A -> B internally. >> > >> > -Dan >> > >> > > On Mar 5, 2019, at 6:07 PM, Martín Hötzel Escardó < >> escardo...@gmail.com> wrote: >> > > >> > > Or you can read the paper https://lmcs.episciences.org/3217/ >> regarding what Nicolai said. >> > > >> > > Moreover, in the HoTT book, it is shown that if || X||->X holds for >> all X, then univalence can't hold. (It is global choice, which can't be >> invariant under equivalence.) >> > > >> > > The above paper shows that unrestricted ||X||->X it gives excluded >> middle. >> > > >> > > However, for a lot of kinds of types one can show that ||X||->X does >> hold. For example, if they have a constant endo-function. Moreover, for any >> type X, the availability of ||X||->X is logically equivalent to the >> availability of a constant map X->X (before we know whether X has a point >> or not, in which case the availability of a constant endo-map is trivial). >> > > >> > > Martin >> > > >> > > On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote: >> > > You can't have a function which, for all A, gives you ||A|| -> A. See >> the exercises 3.11 and 3.12! >> > > -- Nicolai >> > > >> > > On 05/03/19 22:31, Jean Joseph wrote: >> > >> Hi, >> > >> >> > >> From the HoTT book, the truncation of any type A has two >> constructors: >> > >> >> > >> 1) for any a : A, there is |a| : ||A|| >> > >> 2) for any x,y : ||A||, x = y. >> > >> >> > >> I get that if A is inhabited, then ||A|| is inhabited by (1). But is >> it true that, if ||A|| is inhabited, then A is inhabited? >> > >> -- >> > >> 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. >> > >> For more options, visit https://groups.google.com/d/optout. >> > > >> > > >> > > -- >> > > 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. >> > > For more options, visit https://groups.google.com/d/optout. >> > >> > >> > -- >> > 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. >> > For more options, visit https://groups.google.com/d/optout. >> >> -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 10223 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 6618 bytes --] Oh, this is annoying, because it seems to mean that we would need unbounded search (to drop all "hcom []"'s) until we can read the |x,a|, which is against the spirit of, say, Martin-Loef type theories. Martin On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote: > > That would be true if the term you are normalizing is in the empty > interval context, and the cubical type theory has “empty system regularity” > (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). > > Otherwise, if you evaluate something in the empty interval context, you > might see something like > hcom [] (hcom [] (hcom [] (hcom [] (… |x,a| … )))) > with |x,a| in there somewhere. In HITs, Kan composition is treated as a > constructor of the type, and though there are no interesting lines to > compose in the empty interval context, the uninteresting compositions don’t > vanish in all flavors of cubical type theory. > > > On Mar 7, 2019, at 5:41 PM, Martín Hötzel Escardó <escardo...@gmail.com > <javascript:>> wrote: > > > > So I presume that when we ask cubical Agda to normalize a term of type > || Sigma (x:X), A x || we will get a term of the form |x,a| and so we will > see the x in normal form, where |-| is the map into the truncation, right? > Martin. > > > > On Thursday, 7 March 2019 21:52:12 UTC, Anders Mörtberg wrote: > > The existence property is proved for CCHM cubicaltt by Simon in: > > > > https://arxiv.org/abs/1607.04156 > > > > See corollary 5.2. This works a bit more generally than what Martín > said, in particular in any context with only dimension variables we can > compute a witness to an existence. So if in context G = i_1 : II, ..., i_n > : II (possibly empty) we have: > > > > G |- t : exists (x : X), A(x) > > > > then we can compute G |- u : X so that G |- B(u). > > > > -- > > Anders > > > > On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Martín Hötzel Escardó > wrote: > > I got confused now. :-) > > > > Seriously now, what you say seems related to the fact that from a proof > |- t : || X || in the empty context, you get |- x : X in cubical type > theory. This follows from Simon's canonicity result (at least for X=natural > numbers), and is like the so-called "existence property" in the internal > language of the free elementary topos. This says that from a proof |- > exists (x:X), A x in the empty context, you get |- x : X and |- A x. This > says that exists in the empty context behaves like Sigma. But only in the > empty context, because otherwise it behaves like "local existence" as in > Kripke-Joyal semantics. > > > > Martin > > > > On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote: > > Just in case anyone reading this thread later is confused about a more > beginner point than the ones Nicolai and Martin made, one possible > stumbling block here is that, if someone means “is inhabited” in an > external sense (there is a closed term of that type), then the answer is > yes (at least in some models): if ||A|| is inhabited then A is inhabited. > For example, in cubical models with canonicity, it is true that a closed > term of type ||A|| evaluates to a value that has as a subterm a closed term > of type A (the other values of ||A|| are some “formal compositions” of > values of ||A||, but there has to be an |a| in there at the base case). > This is consistent with what Martin and Nicolai said because “if A is > inhabited then B is inhabited” (in this external sense) doesn’t necessarily > mean there is a map A -> B internally. > > > > -Dan > > > > > On Mar 5, 2019, at 6:07 PM, Martín Hötzel Escardó < > escardo...@gmail.com> wrote: > > > > > > Or you can read the paper https://lmcs.episciences.org/3217/ > regarding what Nicolai said. > > > > > > Moreover, in the HoTT book, it is shown that if || X||->X holds for > all X, then univalence can't hold. (It is global choice, which can't be > invariant under equivalence.) > > > > > > The above paper shows that unrestricted ||X||->X it gives excluded > middle. > > > > > > However, for a lot of kinds of types one can show that ||X||->X does > hold. For example, if they have a constant endo-function. Moreover, for any > type X, the availability of ||X||->X is logically equivalent to the > availability of a constant map X->X (before we know whether X has a point > or not, in which case the availability of a constant endo-map is trivial). > > > > > > Martin > > > > > > On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote: > > > You can't have a function which, for all A, gives you ||A|| -> A. See > the exercises 3.11 and 3.12! > > > -- Nicolai > > > > > > On 05/03/19 22:31, Jean Joseph wrote: > > >> Hi, > > >> > > >> From the HoTT book, the truncation of any type A has two > constructors: > > >> > > >> 1) for any a : A, there is |a| : ||A|| > > >> 2) for any x,y : ||A||, x = y. > > >> > > >> I get that if A is inhabited, then ||A|| is inhabited by (1). But is > it true that, if ||A|| is inhabited, then A is inhabited? > > >> -- > > >> 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 > <javascript:>. > > >> For more options, visit https://groups.google.com/d/optout. > > > > > > > > > -- > > > 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 <javascript:>. > > > > For more options, visit https://groups.google.com/d/optout. > > > > > > -- > > 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 <javascript:>. > > > For more options, visit https://groups.google.com/d/optout. > > -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 10303 bytes --]

That would be true if the term you are normalizing is in the empty interval context, and the cubical type theory has “empty system regularity” (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). Otherwise, if you evaluate something in the empty interval context, you might see something like hcom [] (hcom [] (hcom [] (hcom [] (… |x,a| … )))) with |x,a| in there somewhere. In HITs, Kan composition is treated as a constructor of the type, and though there are no interesting lines to compose in the empty interval context, the uninteresting compositions don’t vanish in all flavors of cubical type theory. > On Mar 7, 2019, at 5:41 PM, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: > > So I presume that when we ask cubical Agda to normalize a term of type || Sigma (x:X), A x || we will get a term of the form |x,a| and so we will see the x in normal form, where |-| is the map into the truncation, right? Martin. > > On Thursday, 7 March 2019 21:52:12 UTC, Anders Mörtberg wrote: > The existence property is proved for CCHM cubicaltt by Simon in: > > https://arxiv.org/abs/1607.04156 > > See corollary 5.2. This works a bit more generally than what Martín said, in particular in any context with only dimension variables we can compute a witness to an existence. So if in context G = i_1 : II, ..., i_n : II (possibly empty) we have: > > G |- t : exists (x : X), A(x) > > then we can compute G |- u : X so that G |- B(u). > > -- > Anders > > On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Martín Hötzel Escardó wrote: > I got confused now. :-) > > Seriously now, what you say seems related to the fact that from a proof |- t : || X || in the empty context, you get |- x : X in cubical type theory. This follows from Simon's canonicity result (at least for X=natural numbers), and is like the so-called "existence property" in the internal language of the free elementary topos. This says that from a proof |- exists (x:X), A x in the empty context, you get |- x : X and |- A x. This says that exists in the empty context behaves like Sigma. But only in the empty context, because otherwise it behaves like "local existence" as in Kripke-Joyal semantics. > > Martin > > On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote: > Just in case anyone reading this thread later is confused about a more beginner point than the ones Nicolai and Martin made, one possible stumbling block here is that, if someone means “is inhabited” in an external sense (there is a closed term of that type), then the answer is yes (at least in some models): if ||A|| is inhabited then A is inhabited. For example, in cubical models with canonicity, it is true that a closed term of type ||A|| evaluates to a value that has as a subterm a closed term of type A (the other values of ||A|| are some “formal compositions” of values of ||A||, but there has to be an |a| in there at the base case). This is consistent with what Martin and Nicolai said because “if A is inhabited then B is inhabited” (in this external sense) doesn’t necessarily mean there is a map A -> B internally. > > -Dan > > > On Mar 5, 2019, at 6:07 PM, Martín Hötzel Escardó <escardo...@gmail.com> wrote: > > > > Or you can read the paper https://lmcs.episciences.org/3217/ regarding what Nicolai said. > > > > Moreover, in the HoTT book, it is shown that if || X||->X holds for all X, then univalence can't hold. (It is global choice, which can't be invariant under equivalence.) > > > > The above paper shows that unrestricted ||X||->X it gives excluded middle. > > > > However, for a lot of kinds of types one can show that ||X||->X does hold. For example, if they have a constant endo-function. Moreover, for any type X, the availability of ||X||->X is logically equivalent to the availability of a constant map X->X (before we know whether X has a point or not, in which case the availability of a constant endo-map is trivial). > > > > Martin > > > > On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote: > > You can't have a function which, for all A, gives you ||A|| -> A. See the exercises 3.11 and 3.12! > > -- Nicolai > > > > On 05/03/19 22:31, Jean Joseph wrote: > >> Hi, > >> > >> From the HoTT book, the truncation of any type A has two constructors: > >> > >> 1) for any a : A, there is |a| : ||A|| > >> 2) for any x,y : ||A||, x = y. > >> > >> I get that if A is inhabited, then ||A|| is inhabited by (1). But is it true that, if ||A|| is inhabited, then A is inhabited? > >> -- > >> 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. > >> For more options, visit https://groups.google.com/d/optout. > > > > > > -- > > 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. > > For more options, visit https://groups.google.com/d/optout. > > > -- > 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. > For more options, visit https://groups.google.com/d/optout. -- 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. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 5162 bytes --] So I presume that when we ask cubical Agda to normalize a term of type || Sigma (x:X), A x || we will get a term of the form |x,a| and so we will see the x in normal form, where |-| is the map into the truncation, right? Martin. On Thursday, 7 March 2019 21:52:12 UTC, Anders Mörtberg wrote: > > The existence property is proved for CCHM cubicaltt by Simon in: > > https://arxiv.org/abs/1607.04156 > > See corollary 5.2. This works a bit more generally than what Martín said, > in particular in any context with only dimension variables we can compute a > witness to an existence. So if in context G = i_1 : II, ..., i_n : II > (possibly empty) we have: > > G |- t : exists (x : X), A(x) > > then we can compute G |- u : X so that G |- B(u). > > -- > Anders > > On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Martín Hötzel Escardó > wrote: >> >> I got confused now. :-) >> >> Seriously now, what you say seems related to the fact that from a proof >> |- t : || X || in the empty context, you get |- x : X in cubical type >> theory. This follows from Simon's canonicity result (at least for X=natural >> numbers), and is like the so-called "existence property" in the internal >> language of the free elementary topos. This says that from a proof |- >> exists (x:X), A x in the empty context, you get |- x : X and |- A x. This >> says that exists in the empty context behaves like Sigma. But only in the >> empty context, because otherwise it behaves like "local existence" as in >> Kripke-Joyal semantics. >> >> Martin >> >> On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote: >>> >>> Just in case anyone reading this thread later is confused about a more >>> beginner point than the ones Nicolai and Martin made, one possible >>> stumbling block here is that, if someone means “is inhabited” in an >>> external sense (there is a closed term of that type), then the answer is >>> yes (at least in some models): if ||A|| is inhabited then A is inhabited. >>> For example, in cubical models with canonicity, it is true that a closed >>> term of type ||A|| evaluates to a value that has as a subterm a closed term >>> of type A (the other values of ||A|| are some “formal compositions” of >>> values of ||A||, but there has to be an |a| in there at the base case). >>> This is consistent with what Martin and Nicolai said because “if A is >>> inhabited then B is inhabited” (in this external sense) doesn’t necessarily >>> mean there is a map A -> B internally. >>> >>> -Dan >>> >>> > On Mar 5, 2019, at 6:07 PM, Martín Hötzel Escardó < >>> escardo...@gmail.com> wrote: >>> > >>> > Or you can read the paper https://lmcs.episciences.org/3217/ >>> regarding what Nicolai said. >>> > >>> > Moreover, in the HoTT book, it is shown that if || X||->X holds for >>> all X, then univalence can't hold. (It is global choice, which can't be >>> invariant under equivalence.) >>> > >>> > The above paper shows that unrestricted ||X||->X it gives excluded >>> middle. >>> > >>> > However, for a lot of kinds of types one can show that ||X||->X does >>> hold. For example, if they have a constant endo-function. Moreover, for any >>> type X, the availability of ||X||->X is logically equivalent to the >>> availability of a constant map X->X (before we know whether X has a point >>> or not, in which case the availability of a constant endo-map is trivial). >>> > >>> > Martin >>> > >>> > On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote: >>> > You can't have a function which, for all A, gives you ||A|| -> A. See >>> the exercises 3.11 and 3.12! >>> > -- Nicolai >>> > >>> > On 05/03/19 22:31, Jean Joseph wrote: >>> >> Hi, >>> >> >>> >> From the HoTT book, the truncation of any type A has two >>> constructors: >>> >> >>> >> 1) for any a : A, there is |a| : ||A|| >>> >> 2) for any x,y : ||A||, x = y. >>> >> >>> >> I get that if A is inhabited, then ||A|| is inhabited by (1). But is >>> it true that, if ||A|| is inhabited, then A is inhabited? >>> >> -- >>> >> 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. >>> >> For more options, visit https://groups.google.com/d/optout. >>> > >>> > >>> > -- >>> > 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. >>> > For more options, visit https://groups.google.com/d/optout. >>> >>> -- 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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 7386 bytes --]