LICS 2020 will include two "HoTT heavy" sessions (B5 on Wednesday July 8 and E5 on Friday July 10). The talks are already online, and participation in the Q/A session will be live via Zoom. Registration is free: https://lics2020.saarland-informatics-campus.de/schedule/ -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D5AEEB22-F17C-4452-826F-C3F6E16A1972%40cmu.edu.

[-- Attachment #1.1: Type: text/plain, Size: 2517 bytes --] The Compositional Systems and Methods group at the Tallinn University of Technology, Estonia (https://compose.ioc.ee) is seeking highly qualified PhD candidates. The ideal student should have a solid grounding in category theory, and in at least one of the following areas: programming languages, concurrency theory, quantum computing, database and information systems, or machine learning. The group’s lingua franca is category theory and our research concerns mathematical foundations, as well as various applications in computer science and related disciplines. We are working on relational algebra and functorial semantics, open games, process languages for smart contracts, string diagrams, compositional descriptions of models of computation and concurrency, lenses and optics in functional programming, type theory, and several other topics. The group is led by Pawel Sobocinski, has two postdoctoral researchers, Edward Morehouse and Fosco Loregian, and four PhD students: Elena Di Lavore, Nathan Haydon, Chad Nester and Mario Román. One additional postdoctoral researcher will be recruited in the autumn of 2020. Our research is supported by the ESF funded Estonian IT Academy research measure. The group’s ethos emphasises openness, and inter-group collaboration is highly encouraged. We maintain an active member-led seminar series and hold regular group meetings, research retreats in the Estonian countryside, and various cross-cutting research activities. The successful students will be awarded a generous stipend and be provided with computing equipment and resources for travelling to conferences, summer schools, and other events relevant to their projects. Applicants should hold a Masters degree in Computer Science, Mathematics or a closely related field. To apply, send a CV and a motivation letter outlining your research interests to Pawel Sobocinski pawel.sobocinski@taltech.ee. APPLICATION DEADLINE: July 31, 2020 STARTING DATE: November 2020 or as per agreement Fosco Loregian Edward Morehouse Pawel Sobocinski -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/be861f35-c084-47c8-be72-bbf1d17b82e7o%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2827 bytes --]

CALL FOR PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations July 5-7, 2020, The Internet https://hott-uf.github.io/2020 Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Registration Registration is free of charge, but required. The details can be found on the event website. # Invited talks * Carlo Angiuli (Carnegie Mellon University) From raw terms to recollement * Liron Cohen (Ben-Gurion University) Building Effectful Realizability Models, Uniformly * Pierre-Louis Curien (Université de Paris) A syntactic approach to opetopes, opetopic sets and opetopic categories # Contributed talks 21 talks were accepted by the Program Committee. Their titles and abstracts are available on the event website. # Schedule The event will take place from July 5-7, 2020. The talks are scheduled between 2 PM and 7:30 PM CEST (UTC+2). Detailed schedule is now available on the website. # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario) -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3O9E5m4iAkxxX7xMCGHnnsdE71c_nHWvPhNoVKMjtfe_w%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 4282 bytes --] ===================================== CALL FOR PARTICIPATION Logical Frameworks and Meta-Languages: Theory and Practice<https://lfmtp.org/workshops/2020/program.shtml> LFMTP 2020 On-line conference, ==> 29-30 June 2020 <== Affiliated with FSCD 2020 and IJCAR 2020<https://fscd-ijcar-2020.org/>. The 2020 editions of LFMTP will be held online and it will consists of - 8 regular talks - 2 invited talks by Elaine Pimentel and Andre Popescu Participation will be free, but a preregistration is required to join the video meetings of the events. Registration page<https://fscd-ijcar-2020.org/register> ===================================== ABOUT LFMTP Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2020 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages, process calculi and related formally specified systems. * Formalisation of model-theoretic and proof-theoretic semantics of logics. ABOUT LFMTP Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2020 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages, process calculi and related formally specified systems. * Formalisation of model-theoretic and proof-theoretic semantics of logics. * Applications of logical frameworks: proof-carrying architectures, proof exchange and transformation, program refactoring, etc. * Techniques for programming with binders in functional programming languages such as Haskell, OCaml or Agda, and logic programming languages such as lambda Prolog or Alpha-Prolog. * Design and implementation of systems and tools related to meta-languages and logical frameworks PROGRAM COMMITTEE David Baelde, LSV, ENS Paris-Saclay & Inria Paris Frédéric Blanqui, INRIA Alberto Ciaffaglione, University of Udine Dennis Müller, Friedrich-Alexander-University Erlangen-Nürnberg Michael Norrish, Data61 Carlos Olarte, Universidade Federal do Rio Grande do Norde Claudio Sacerdoti Coen, University of Bologna (PC Co-Chair) Ulrich Schöpp, fortiss GmbH Alwen Tiu, Australian National University (PC Co-Chair) Tjark Weber, Uppsala University -- Prof. Claudio Sacerdoti Coen Department of Computer Science and Engineering University of Bologna -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1e271a79fb520a5a1d0b62c88580436d049b826a.camel%40unibo.it. [-- Attachment #2: Type: text/html, Size: 6021 bytes --]

The HoTTEST Conference of 2020 is next week, from Monday to Friday, with two talks per day at 10:30am and 12pm EDT (UTC-4). The Zoom link is https://zoom.us/j/994874377 Speakers and titles Brandon Doherty (University of Western Ontario) Cubical models of (∞,1)-categories Eric Finster (University of Birmingham) Weak structures from strict ones Valery Isaev (JetBrains Research and Higher School of Economics) Indexed type theories Peter LeFanu Lumsdaine (Stockholm University) What are we thinking when we present a type theory? David Jaz Myers (Johns Hopkins University) Higher Schreier theory Paige Randall North (Ohio State University) A higher structure identity principle Anja Petković (University of Ljubljana) Equality checking for finitary type theories Mitchell Riley (Wesleyan University) Synthetic spectra via a monadic and comonadic modality Mike Shulman (University of San Diego) Type-theoretic model toposes Taichi Uemura (University of Amsterdam) Abstract type theories Further information, including abstracts and schedule, can be found at https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_conference_2020.html The talks are also listed at https://researchseminars.org/seminar/HoTTEST2020 On behalf of the organizers, Dan Christensen Chris Kapulkin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/875zbw1d95.fsf%40uwo.ca.

[-- Attachment #1.1: Type: text/plain, Size: 2918 bytes --] Due to the sanitary crisis in May, the EPIT2020 summer school has been postponed to October ==================================================================== Spring School on Theoretical Computer Science (EPIT) – Homotopy Type Theory Ile d’Oléron, CAES CNRS La vieille Perrotine, France. 19th-23th Oct 2020 https://epit2020cnrs.inria.fr ==================================================================== On Monday, March 2, 2020 at 8:14:48 PM UTC+1, nicolas tabareau wrote: > > [This is a reminder that the deadline for pre-registration is ** March 15, > 2020 **, note > that we are pleased to have to new lectures by Valery Isaev and Paige > North] > > ==================================================================== > > Spring School on Theoretical Computer Science (EPIT) – Homotopy Type Theory > > Ile d’Oléron, CAES CNRS La vieille Perrotine, France. > > 25th-29th May 2020 > > https://epit2020cnrs.inria.fr > > ==================================================================== > > The EPIT is a French thematic school proposing, on an yearly basis, an > intensive 5-day long training, > specializing on a particular topic in theoretical computer science. It is > primarily addressed to PhD students, > Post-doctoral researchers and junior academics. > > The 2020 edition of the EPIT will be centered around Homotopy Type Theory, > a research topic at the junction > of Computer Science and Mathematics. Our hope is hence to provide an > introduction that is accessible > to researchers in both areas. > > Pre-registration is now open, please visit > https://epit2020cnrs.inria.fr/registration/ to know more. > > For any question, please contact epit2020@sciencesconf.org > > NB: As the number of places is limited, we have fixed a deadline for > pre-registration to ** March 15, 2020 **. > > -------------------------------------------------------------------- > Lecturers > > Andrej Bauer (Ljubljana University): > Introduction to Homotopy Type Theory > > Guillaume Brunerie (Stockholm University): > Synthetic Homotopy Theory > > Valery Isaev (JetBrain, Saint Petersburg): > The Arend proof assistant > > Anders Mörtberg (Stockholm University): > Cubical Type Theory > > Paige North (Ohio State University): > Directed Homotopy Type Theory > > Andy Pitts (Cambridge University): > Models of (Univalent) Type Theory > > Bas Spitters (Aarhus University): > The Coq-HoTT library > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/7a9f7238-8336-45f7-ad11-b8f2e5a370a0o%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 9258 bytes --]

[-- Attachment #1: Type: text/plain, Size: 5017 bytes --] Hi, Here's a simple countermodel that shows that the Martin-Löf eliminator (two-sided eliminator) for identity types is not strong enough to derive transport in the absence of Pi-types. Consider the initial model of a type theory with Id, refl, a closed type A, a type family B over A, and closed terms x,y : A, b : B x and p : Id_A x y. It can be shown that the only terms of that model are the variables, the weakenings of the generators and their iterated refls. Because there is no closed term of type B y, transport does not hold in this model. However, unless I missed some cases, it is still possible to define the Martin-Löf eliminator by case distinction on the elimination target. Best, Rafaël On 3/23/20 10:54 AM, Ambrus Kaposi wrote: > Hi, > > Sorry for resurrecting an old thread, I just wanted to document that > Frobenius J can be derived from Paulin-Mohring J without Pi, Sigma or > universes: > https://github.com/akaposi/hiit-signatures/blob/master/formalization/FrobeniusJDeriv.agda > This was observed by Rafael Bocquet and András Kovács in October 2019, > but maybe other people have known about this. > > We mention this briefly in our paper on HIIT signatures where > Paulin-Mohring J can be used on previous equality constructors but we > don't have Pi, Sigma or (usual) universes: > https://lmcs.episciences.org/6100 > > Cheers, > Ambrus > > 2018. július 13., péntek 13:05:47 UTC+2 időpontban Valery Isaev a > következőt írta: > > > 2018-07-13 13:38 GMT+03:00 Peter LeFanu Lumsdaine > <p.l.l...@gmail.com <javascript:>>: > > On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev > <valer...@gmail.com <javascript:>> wrote: > > Hi Peter, > > I've been thinking about such eliminators lately too. It > seems that they are derivable from ordinary eliminator for > most type-theoretic constructions as long as we have > identity types and sigma types. > > > Thankyou — very nice observation, and (at least to me) quite > surprising! > > > I was surprised too. The case of coproducts is especially unexpected. > > I mean a strong version of Id: > > > Side note: this is I think more widely known as the > Paulin-Mohring or one-sided eliminator for Id-types; the HoTT > book calls it based path-induction. > > The fact that the Frobenius version is strictly > stronger is known in folklore, but not written up > anywhere I know of. One way to show this is to take > any non right proper model category (e.g. the model > structure for quasi-categories on simplicial sets), > and take the model of given by its (TC,F) wfs; this > will model the simple version of Id-types but not the > Frobenius version. > > Are you sure this is true? It seems that we can interpret > the strong version of J even in non right proper model > categories. Then the argument I gave above shows that the > Frobenius version is also definable. > > > Ah, yes — there was a mistake in the argument I had in mind. > In that case, do we really know for sure that the Frobenius > versions are really strictly stronger? > > I don't know how to prove this, but it seems that we can't even > define transport without Frobenius J. Also, if we do have > transport and we know that types of the form \Sigma (x : A) > Id(a,x) are contractible, then the "one-sided J" is definable, so > if we want to prove that the Frobenius version does not follows > from the non-Frobenius, we need to find a model where either > transport is not definable or \Sigma (x : A) Id(a,x) is not > contractible. > > –p. > > > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/ade5cab1-5df2-41c9-b412-ac561fbe77bc%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/ade5cab1-5df2-41c9-b412-ac561fbe77bc%40googlegroups.com?utm_medium=email&utm_source=footer>. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/17a9e7e7-e03b-cf03-58de-5f1f77d74469%40ens.fr. [-- Attachment #2: Type: text/html, Size: 12088 bytes --]

It is my pleasure to announce the second in the series of online seminars on proof assistants. MMT: A Foundation-Independent Logical System Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2) Location: online at Zoom ID 989 0478 8985 (https://zoom.us/j/98904788985) Speaker: Florian Rabe (University of Erlangen) (https://kwarc.info/people/frabe/) Proof assistant: The MMT Language and System (https://uniformal.github.io/) Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committing to any foundational features like function types or propositions. All MMT algorithms are parametric in a set of rules, which are self-contained objects plugged in by the language designer. That results in a framework general enough to develop many formal systems including other logical frameworks in it, enabling the rapid prototyping of new language features. Despite this high level of generality, it is possible to develop sophisticated results in MMT. The current release includes, e.g., parsing, type reconstruction, module system, IDE-style editor, and interactive library browser. MMT is systematically designed to be extensible, providing multiple APIs and plugin interfaces, and thus provides a versatile infrastructure for system development and integration. This talk gives an overview of the current state of MMT and its future challenges. Examples are drawn from the LATIN project, a long-running project of building a modular, highly inter-related suite of formalizations of logics and related formal systems. After the talk, the video recording will be made available. Also see the anouncement on my blog at http://math.andrej.com/2020/05/15/mmt-a-foundation-independent-logical-system/ The spring schedule of talks is planned as follows: May 28, 2020: Brigitte Pientka - Beluga June 11, 2020: Conor McBride - Epigram 2 June 25, 2020: William J. Bowman, Cur July 2, 2020: Anders Mörtberg - cubicaltt (to be confirmed) July 9, 2020: Jon Sterling - redtt (to be confirmed) With kind regards, Andrej -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB0nkh2Q_YFsZEZDq0qx9EudT3dO5yaSFPWP5hVWtJSgykkrnQ%40mail.gmail.com.

[-- Attachment #1.1: Type: text/plain, Size: 814 bytes --] We have funding for PhD studentships in mathematics and computation in our Theoretical Computer Science group https://www.cs.bham.ac.uk/research/groupings/theory/ If you are interested, please approach an academic from the above web page, with Cc: to Martin Escardo, briefly explaining your research interests and academic qualifications. After you approach us we will give you further information and instructions. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/bf67c90a-2fa6-404a-9213-fc498f862be1%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1162 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2035 bytes --] I think the zulip chats might be slightly friendlier for newcomers than any of the sources you mentioned just because they're more casual. For instance, I asked some very naive questions on the lean zulip chat and wasn't made to feel like a complete idiot. Since zulip seems to be increasingly popular in other communities with an interest in formalized mathematics, this might also serve as a "recruiting opportunity" to get some new folks to start playing around with agda. Emily -- Associate Professor, Dept. of Mathematics Johns Hopkins University www.math.jhu.edu/~eriehl she/her On Wed, May 13, 2020 at 6:20 AM Nils Anders Danielsson <nad@cse.gu.se> wrote: > On 2020-05-13 13:29, Egbert Rijke wrote: > > I created a zulipchat for agda. Feel free to join! > > > > https://agda.zulipchat.com/join/dig82g1cmzd4bqrtp6o3qxaa/ > > Is there a need for yet another channel for communication about Agda? > People are already asking questions on the Agda mailing list, on the > GitHub bug tracker, on the IRC channel, on Gitter, on Reddit, and on > Stack Overflow. What is the purpose of adding yet another channel (which > additionally seems to require you to log in just to see what others have > written)? > > -- > /NAD > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/a17e988e-1455-3bc5-03c5-d24c5b07747a%40cse.gu.se > . > > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAjZwAb1mNUDUphDimRxJeUkYJkWq3VpgWYcCxbsgN5Uy2edQg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3558 bytes --]

On 2020-05-13 13:29, Egbert Rijke wrote: > I created a zulipchat for agda. Feel free to join! > > https://agda.zulipchat.com/join/dig82g1cmzd4bqrtp6o3qxaa/ Is there a need for yet another channel for communication about Agda? People are already asking questions on the Agda mailing list, on the GitHub bug tracker, on the IRC channel, on Gitter, on Reddit, and on Stack Overflow. What is the purpose of adding yet another channel (which additionally seems to require you to log in just to see what others have written)? -- /NAD -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/a17e988e-1455-3bc5-03c5-d24c5b07747a%40cse.gu.se.

[-- Attachment #1: Type: text/plain, Size: 559 bytes --] Dear all, I created a zulipchat for agda. Feel free to join! https://agda.zulipchat.com/join/dig82g1cmzd4bqrtp6o3qxaa/ With kind regards, Egbert -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1OBOVKUPKaxDb%2Bhkx7n%2BbFMqpEDkRjWTD%2BXds_x7y47CdA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1249 bytes --]

```
> FWIW there is no trouble at all with "internal categories" in HoTT;
what I meant is that they are "evil" in the sense that they allow one
to speak about equality of objects
but if you do it in the simplicial sets model of HoTT then they are not quite
the same as categories internal to sSet
they are rather the unstraightenings of simplicially enriched cats
whose homobjects are all contractible
the contractible objects in sSet are much richer than the subobjects of 1
one should not forget that the logic of sSet when viewed at
homotopically is boolean whereas the traditional logic of sSet is not
at all
but I do understand that ordinary finite limit cats do live in sSet
via nerve
Thomas
```

```
FWIW there is no trouble at all with "internal categories" in HoTT;
they just correspond to (pre)categories in the smallest universe.
Some of them will naturally be univalent categories, while others will
naturally be strict categories. If we want to "do category theory"
with the latter we can Rezk-complete them to univalent ones, but
sometimes this is unnecessary, e.g. if our goal is to talk about
"internal presheaves" on them then these are just contravariant
functors to the (univalent) category Set, and the universal property
of Rezk-completion says that it doesn't matter whether or not we
Rezk-complete the domain before talking about presheaves. In
addition, we get the bonus that when talking about univalent
categories internally we are externally talking about *stacks*, with
the "weak equivalences" automatically inverted (but if for some reason
we don't want to do that, we can stick with strict categories).
On Mon, May 11, 2020 at 9:37 AM <stre...@mathematik.tu-darmstadt.de> wrote:
>
> > Thank you for pointing out the case of the universe of constructible sets
> > L.
> > It is internal to ZF because it is was constructed from ordinals in ZF.
> > Could it be also external to ZF ?
>
> Anything internal can be externalized but not the other way round.
>
> The point I tried to make was that in the usual models of 2-level type
> theory the homotopical part is not internal to the ambient nonhomotopical
> part.
>
> > Gödel thought that ordinals and sets are real, like matter, but of a
> > different kind.
> > He was the first to use the full power of mathematics for studying formal
> > logic.
> > Most logicians believe that natural numbers are real.
> > They use natural numbers and induction for studying formal systems.
>
> Indeed, Goedel was the first one who took serious the difference between
> syntax and semantics. This was crucial for his findings.
> That he nevertheless was a dyed in the wool Platonist was a bit inconsequent
> but nobody is perfect :-)
>
> 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 HomotopyT...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/0388695a1dfc717f9c5e458937dff760.squirrel%40webmail.mathematik.tu-darmstadt.de.
```

> Thank you for pointing out the case of the universe of constructible sets > L. > It is internal to ZF because it is was constructed from ordinals in ZF. > Could it be also external to ZF ? Anything internal can be externalized but not the other way round. The point I tried to make was that in the usual models of 2-level type theory the homotopical part is not internal to the ambient nonhomotopical part. > GÃ¶del thought that ordinals and sets are real, like matter, but of a > different kind. > He was the first to use the full power of mathematics for studying formal > logic. > Most logicians believe that natural numbers are real. > They use natural numbers and induction for studying formal systems. Indeed, Goedel was the first one who took serious the difference between syntax and semantics. This was crucial for his findings. That he nevertheless was a dyed in the wool Platonist was a bit inconsequent but nobody is perfect :-) Thomas

Thank you for pointing out the case of the universe of constructible sets L. It is internal to ZF because it is was constructed from ordinals in ZF. Could it be also external to ZF ? Gödel thought that ordinals and sets are real, like matter, but of a different kind. He was the first to use the full power of mathematics for studying formal logic. Most logicians believe that natural numbers are real. They use natural numbers and induction for studying formal systems. Best, André PS: It is not easy to stop participating to this interesting discussion! ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] Sent: Monday, May 11, 2020 3:33 AM To: Joyal, André Cc: Ulrik Buchholtz; Homotopy Type Theory Subject: Re: [HoTT] Identity versus equality Dear Andr"e, the exo/endo distinction is different from external/internal. It is like L in set theory ZF which does not allow one to prove consisteny of ZF. (An aside: why do internal cats play such an important role in traditional topos theory and are evil in Hott?) Thomas

Dear Andr"e, the exo/endo distinction is different from external/internal. It is like L in set theory ZF which does not allow one to prove consisteny of ZF. (An aside: why do internal cats play such an important role in traditional topos theory and are evil in Hott?) Thomas

Quick info: - HoTT/UF 2020 will take place online on July 5-6, 2020 - Submission deadline: May 20, 2020 Details below. Best, Chris * Workshop on Homotopy Type Theory and Univalent Foundations July 5-6, 2020, The Internet https://hott-uf.github.io/2020 Abstract submission deadline: May 20, 2020 Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Invited talks * Carlo Angiuli (Carnegie Mellon University) * Liron Cohen (Ben-Gurion University) * Pierre-Louis Curien (Université de Paris) # Submissions * Abstract submission deadline: May 20, 2020 * Author notification: June 05, 2020 Submissions should consist of a title and an abstract, in pdf format, of no more than 2 pages, submitted via https://easychair.org/conferences/?conf=hottuf2020 Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. # Program committee * Benedikt Ahrens (University of Birmingham) * Paolo Capriotti (Technische Universität Darmstadt) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Birmingham) * Peter LeFanu Lumsdaine (Stockholm University) * Anders Mörtberg (Stockholm University) * Paige Randall North (Ohio State University) * Nicolas Tabareau (Inria Nantes) # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario)

```
Unfortunately, I must take a break from the present discussion.
I would like to thank David, Jon, Micheal, Nicolai, Steve, Thomas, Thorsten and Ulrik
for expressing their view on the problems raised.
I feel confident that we are collectively moving toward one or many solutiona.
Best,
André
________________________________________
From: Michael Shulman [shu...@sandiego.edu]
Sent: Sunday, May 10, 2020 4:22 PM
To: Nicolai Kraus
Cc: Joyal, André; Thomas Streicher; David Roberts; Thorsten Altenkirch; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality
I'm not sure I understand the meanings of "deep" and "shallow"
completely, but the dichotomy seems similar to what we sometimes call
"analytic" and "synthetic". Any foundational theory only
directly/synthetically represents a few concepts; all others have to
be encoded into it "analytically". In ZFC, the synthetic objects are
well-founded membership structures; in ETCS the synthetic objects are
featureless point-sets and functions; in HoTT the synthetic objects
are oo-groupoids.
It seems reasonable to me to argue that whenever we use the
fundamental objects of the framework we should treat them
synthetically, but not expect any other structures to be synthetic.
When working in ZFC, it would be perverse to constantly work with
well-founded membership structures rather than simply use sets. And
when working in HoTT, it would be perverse to work with oo-groupoids
defined in terms of set rather than simply use types. But neither ZFC
nor HoTT has a synthetic notion of "simplicial oo-groupoid" or
"oo-category", so in both cases those structures have to be defined
analytically -- the only difference is that the oo-groupoid
"ingredients" are in ZFC themselves analytic whereas in HoTT those
ingredients are synthetic.
On Sun, May 10, 2020 at 12:18 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> In the last paragraph of my message below, the words "deep" and "shallow" have to be swapped.
>
> On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>>
>> Dear André and everyone,
>>
>> I feel it's worth pointing out that there are two strategies to express
>> "everyday mathematics" in HoTT. In CS-speak, they would probably be
>> called "shallow embedding" and "deep embedding". Shallow embedding is
>> the "HoTT style", deep embedding is the "pre-HoTT type theory style".
>> Shallow means that one uses that the host language shares structure with
>> the object one wants to define, while deep means one doesn't. To explain
>> what I mean, let's look at the type theoretic definition of a group (a
>> 1-group, not a higher group).
>>
>> Definition using deep embedding: A group is a tuple
>> (X,h,e,o,i,assoc,...), where
>> X : Type -- carrier
>> h : is-0-truncated(X) -- carrier is set
>> e : X -- unit
>> o : X * X -> X -- composition
>> i : X -> X -- inverses
>> assoc : (h o g) o f = h o (g o f)
>> ... [and so on]
>>
>> Definition using shallow embedding: A group is a pointed connected 1-type.
>>
>> Fortunately, these definitions are equivalent (via the Eilenberg-McLan
>> spaces construction). But they behave differently when we want to work
>> with them or change them. It's easy to change the second definition to
>> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
>> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
>> is a nice way for the first definition. The second definition has better
>> computational properties than the first.
>>
>> When you say this:
>>
>> > But I find it frustrating that I cant do my everyday mathematics with it.
>> > For example, I cannot say
>> >
>> > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>>
>> You are referring to shallow embedding. In everyday mathematics, you
>> don't say (1) either. You probably say (1) with "Type" replaced by "Set"
>> or by "simplicial set". Both of these can be expressed straightforwardly
>> in type theory using only (h-)sets (i.e. embedding deeply).
>>
>> We strive to use shallow embedding as often as possible for the reasons
>> in the above example. But let's assume that we *can* say (1) in HoTT,
>> using "Type", because we find some encoding that we're reasonably happy
>> with; there's a question which I've asked myself before:
>>
>> Will we not destroy the advantages of deep (over shallow) embedding if
>> we fall back to encodings (and thus destroy the main selling point of
>> HoTT)? For me, the justification of still using deep embedding is that
>> statements using encodings (e.g. "the universe is a higher category)
>> might still imply statements which don't use encodings and are
>> interesting. However, if we want to develop a theory of certain higher
>> structures for it's own sake, then it's not so clear to me whether it's
>> really better to use the HoTT-style deep embedding.
>>
>> Kind regards,
>> Nicolai
>>
>>
>> On 09/05/2020 21:18, Joyal, André wrote:
>> > Dear Thomas,
>> >
>> > You wrote
>> >
>> > <<In my opinion the currenrly implemented type theories are essentially
>> > for proving and not for computing.
>> > But if you haven't mechanized PART of equational reasoning it would be
>> > much much more painful than it still is.
>> > But that is "only" a pragmatic issue.>>
>> >
>> > Type theory has very nice features. I wish they could be preserved and developped further.
>> > But I find it frustrating that I cant do my everyday mathematics with it.
>> > For example, I cannot say
>> >
>> > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>> > (2) Let G be a type equipped with a group structure;
>> > (3) Let BG be the classifying space of a group G;
>> > (4) Let Gr be the category of groups;
>> > (5) Let SType be the category of simplical types.
>> > (6) Let Map(X,Y) be the simplicial types of maps X--->Y
>> > between two simplicial types X and Y.
>> >
>> > It is crucial to have (1)
>> > For example, a group could be defined to
>> > be a simplicial object satisfying the Segal conditions.
>> > The classifying space of a group is the colimit of this simplicial object.
>> > The category of groups can be defined to be
>> > a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>> >
>> > Is there some aspects of type theory that we may give up as a price
>> > for solving these problems ?
>> >
>> >
>> > Best,
>> > André
>> >
>> > ________________________________________
>> > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
>> > Sent: Saturday, May 09, 2020 2:43 PM
>> > To: Joyal, André
>> > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
>> > Subject: Re: [HoTT] Identity versus equality
>> >
>> > Dear Andr'e,
>> >
>> >> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
>> >> The dream of a formal system in which every proof leads to an actual computation may be far off.
>> >> Not that we should abandon it, new discoveries are always possible.
>> >> Is there a version of type theory for proving and verifying, less
>> >> for computing?
>> > In my opinion the currenrly implemented type theories are essentially
>> > for proving and not for computing.
>> > But if you haven't mechanized PART of equational reasoning it would be
>> > much much more painful than it still is.
>> > But that is "only" a pragmatic issue.
>> >
>> >> The notations of type theory are very useful in homotopy theory.
>> >> But the absence of simplicial types is a serious obstacle to applications.
>> > In cubical type theory they sort of live well with cubes not being
>> > fibrant... They have them as pretypes. But maybe I misunderstand...
>> >
>> > Thomas
>> >
>>
```

```
I'm not sure I understand the meanings of "deep" and "shallow"
completely, but the dichotomy seems similar to what we sometimes call
"analytic" and "synthetic". Any foundational theory only
directly/synthetically represents a few concepts; all others have to
be encoded into it "analytically". In ZFC, the synthetic objects are
well-founded membership structures; in ETCS the synthetic objects are
featureless point-sets and functions; in HoTT the synthetic objects
are oo-groupoids.
It seems reasonable to me to argue that whenever we use the
fundamental objects of the framework we should treat them
synthetically, but not expect any other structures to be synthetic.
When working in ZFC, it would be perverse to constantly work with
well-founded membership structures rather than simply use sets. And
when working in HoTT, it would be perverse to work with oo-groupoids
defined in terms of set rather than simply use types. But neither ZFC
nor HoTT has a synthetic notion of "simplicial oo-groupoid" or
"oo-category", so in both cases those structures have to be defined
analytically -- the only difference is that the oo-groupoid
"ingredients" are in ZFC themselves analytic whereas in HoTT those
ingredients are synthetic.
On Sun, May 10, 2020 at 12:18 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> In the last paragraph of my message below, the words "deep" and "shallow" have to be swapped.
>
> On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>>
>> Dear André and everyone,
>>
>> I feel it's worth pointing out that there are two strategies to express
>> "everyday mathematics" in HoTT. In CS-speak, they would probably be
>> called "shallow embedding" and "deep embedding". Shallow embedding is
>> the "HoTT style", deep embedding is the "pre-HoTT type theory style".
>> Shallow means that one uses that the host language shares structure with
>> the object one wants to define, while deep means one doesn't. To explain
>> what I mean, let's look at the type theoretic definition of a group (a
>> 1-group, not a higher group).
>>
>> Definition using deep embedding: A group is a tuple
>> (X,h,e,o,i,assoc,...), where
>> X : Type -- carrier
>> h : is-0-truncated(X) -- carrier is set
>> e : X -- unit
>> o : X * X -> X -- composition
>> i : X -> X -- inverses
>> assoc : (h o g) o f = h o (g o f)
>> ... [and so on]
>>
>> Definition using shallow embedding: A group is a pointed connected 1-type.
>>
>> Fortunately, these definitions are equivalent (via the Eilenberg-McLan
>> spaces construction). But they behave differently when we want to work
>> with them or change them. It's easy to change the second definition to
>> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
>> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
>> is a nice way for the first definition. The second definition has better
>> computational properties than the first.
>>
>> When you say this:
>>
>> > But I find it frustrating that I cant do my everyday mathematics with it.
>> > For example, I cannot say
>> >
>> > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>>
>> You are referring to shallow embedding. In everyday mathematics, you
>> don't say (1) either. You probably say (1) with "Type" replaced by "Set"
>> or by "simplicial set". Both of these can be expressed straightforwardly
>> in type theory using only (h-)sets (i.e. embedding deeply).
>>
>> We strive to use shallow embedding as often as possible for the reasons
>> in the above example. But let's assume that we *can* say (1) in HoTT,
>> using "Type", because we find some encoding that we're reasonably happy
>> with; there's a question which I've asked myself before:
>>
>> Will we not destroy the advantages of deep (over shallow) embedding if
>> we fall back to encodings (and thus destroy the main selling point of
>> HoTT)? For me, the justification of still using deep embedding is that
>> statements using encodings (e.g. "the universe is a higher category)
>> might still imply statements which don't use encodings and are
>> interesting. However, if we want to develop a theory of certain higher
>> structures for it's own sake, then it's not so clear to me whether it's
>> really better to use the HoTT-style deep embedding.
>>
>> Kind regards,
>> Nicolai
>>
>>
>> On 09/05/2020 21:18, Joyal, André wrote:
>> > Dear Thomas,
>> >
>> > You wrote
>> >
>> > <<In my opinion the currenrly implemented type theories are essentially
>> > for proving and not for computing.
>> > But if you haven't mechanized PART of equational reasoning it would be
>> > much much more painful than it still is.
>> > But that is "only" a pragmatic issue.>>
>> >
>> > Type theory has very nice features. I wish they could be preserved and developped further.
>> > But I find it frustrating that I cant do my everyday mathematics with it.
>> > For example, I cannot say
>> >
>> > (1) Let X:\Delta^{op}---->Type be a simplicial type;
>> > (2) Let G be a type equipped with a group structure;
>> > (3) Let BG be the classifying space of a group G;
>> > (4) Let Gr be the category of groups;
>> > (5) Let SType be the category of simplical types.
>> > (6) Let Map(X,Y) be the simplicial types of maps X--->Y
>> > between two simplicial types X and Y.
>> >
>> > It is crucial to have (1)
>> > For example, a group could be defined to
>> > be a simplicial object satisfying the Segal conditions.
>> > The classifying space of a group is the colimit of this simplicial object.
>> > The category of groups can be defined to be
>> > a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>> >
>> > Is there some aspects of type theory that we may give up as a price
>> > for solving these problems ?
>> >
>> >
>> > Best,
>> > André
>> >
>> > ________________________________________
>> > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
>> > Sent: Saturday, May 09, 2020 2:43 PM
>> > To: Joyal, André
>> > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
>> > Subject: Re: [HoTT] Identity versus equality
>> >
>> > Dear Andr'e,
>> >
>> >> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
>> >> The dream of a formal system in which every proof leads to an actual computation may be far off.
>> >> Not that we should abandon it, new discoveries are always possible.
>> >> Is there a version of type theory for proving and verifying, less
>> >> for computing?
>> > In my opinion the currenrly implemented type theories are essentially
>> > for proving and not for computing.
>> > But if you haven't mechanized PART of equational reasoning it would be
>> > much much more painful than it still is.
>> > But that is "only" a pragmatic issue.
>> >
>> >> The notations of type theory are very useful in homotopy theory.
>> >> But the absence of simplicial types is a serious obstacle to applications.
>> > In cubical type theory they sort of live well with cubes not being
>> > fibrant... They have them as pretypes. But maybe I misunderstand...
>> >
>> > Thomas
>> >
>>
```

On 10/05/2020, 15:06, "Michael Shulman" <shu...@sandiego.edu> wrote: On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type We can certainly *talk* about simplicial types in 2LTT as exofunctors from the exocategory Delta to the exocategory Type. I assume the point you're making is that we don't have a (fibrant) *type of* simplicial types, whereas we do have a fibrant type of semisimplicial types (under appropriate axioms)? Yes, by talking about I meant within HoTT. I mean we want to understand them as structures not just as some set-level encoding. Also I find the Kan-condition more natural in HoTT because we just need to state an equivalence. On the level of set-level Mathematics we either hide the witness or we need to introduce uniformity conditions. I also don't think it is an issue that Delta is not direct because Delta is based on the hack to build identities into the framework but obtain composition via the Kan condition. Hence I think we should represent identities in the same way as composition. > You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist. Personally, I think the best axiom to use here is that exo-Nat is *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy. We don't know how to model "exo-Nat is fibrant" in all higher toposes, but it's easy to interpret "exo-Nat is cofibrant" in such models, since Pi-types with domain exo-Nat are just externally-infinite products. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

[-- Attachment #1: Type: text/plain, Size: 5896 bytes --] In the last paragraph of my message below, the words "deep" and "shallow" have to be swapped. On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus <nicola...@gmail.com> wrote: > Dear André and everyone, > > I feel it's worth pointing out that there are two strategies to express > "everyday mathematics" in HoTT. In CS-speak, they would probably be > called "shallow embedding" and "deep embedding". Shallow embedding is > the "HoTT style", deep embedding is the "pre-HoTT type theory style". > Shallow means that one uses that the host language shares structure with > the object one wants to define, while deep means one doesn't. To explain > what I mean, let's look at the type theoretic definition of a group (a > 1-group, not a higher group). > > Definition using deep embedding: A group is a tuple > (X,h,e,o,i,assoc,...), where > X : Type -- carrier > h : is-0-truncated(X) -- carrier is set > e : X -- unit > o : X * X -> X -- composition > i : X -> X -- inverses > assoc : (h o g) o f = h o (g o f) > ... [and so on] > > Definition using shallow embedding: A group is a pointed connected 1-type. > > Fortunately, these definitions are equivalent (via the Eilenberg-McLan > spaces construction). But they behave differently when we want to work > with them or change them. It's easy to change the second definition to > define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 , > arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there > is a nice way for the first definition. The second definition has better > computational properties than the first. > > When you say this: > > > But I find it frustrating that I cant do my everyday mathematics with > it. > > For example, I cannot say > > > > (1) Let X:\Delta^{op}---->Type be a simplicial type; > > You are referring to shallow embedding. In everyday mathematics, you > don't say (1) either. You probably say (1) with "Type" replaced by "Set" > or by "simplicial set". Both of these can be expressed straightforwardly > in type theory using only (h-)sets (i.e. embedding deeply). > > We strive to use shallow embedding as often as possible for the reasons > in the above example. But let's assume that we *can* say (1) in HoTT, > using "Type", because we find some encoding that we're reasonably happy > with; there's a question which I've asked myself before: > > Will we not destroy the advantages of deep (over shallow) embedding if > we fall back to encodings (and thus destroy the main selling point of > HoTT)? For me, the justification of still using deep embedding is that > statements using encodings (e.g. "the universe is a higher category) > might still imply statements which don't use encodings and are > interesting. However, if we want to develop a theory of certain higher > structures for it's own sake, then it's not so clear to me whether it's > really better to use the HoTT-style deep embedding. > > Kind regards, > Nicolai > > > On 09/05/2020 21:18, Joyal, André wrote: > > Dear Thomas, > > > > You wrote > > > > <<In my opinion the currenrly implemented type theories are essentially > > for proving and not for computing. > > But if you haven't mechanized PART of equational reasoning it would be > > much much more painful than it still is. > > But that is "only" a pragmatic issue.>> > > > > Type theory has very nice features. I wish they could be preserved and > developped further. > > But I find it frustrating that I cant do my everyday mathematics with it. > > For example, I cannot say > > > > (1) Let X:\Delta^{op}---->Type be a simplicial type; > > (2) Let G be a type equipped with a group structure; > > (3) Let BG be the classifying space of a group G; > > (4) Let Gr be the category of groups; > > (5) Let SType be the category of simplical types. > > (6) Let Map(X,Y) be the simplicial types of maps X--->Y > > between two simplicial types X and Y. > > > > It is crucial to have (1) > > For example, a group could be defined to > > be a simplicial object satisfying the Segal conditions. > > The classifying space of a group is the colimit of this simplicial > object. > > The category of groups can be defined to be > > a simplicial objects satisfiying the Rezk conditions (a complete Segal > space). > > > > Is there some aspects of type theory that we may give up as a price > > for solving these problems ? > > > > > > Best, > > André > > > > ________________________________________ > > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] > > Sent: Saturday, May 09, 2020 2:43 PM > > To: Joyal, André > > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; > homotopyt...@googlegroups.com > > Subject: Re: [HoTT] Identity versus equality > > > > Dear Andr'e, > > > >> By the way, if type theory is not very effective in practice, why do we > insist that it should always compute? > >> The dream of a formal system in which every proof leads to an actual > computation may be far off. > >> Not that we should abandon it, new discoveries are always possible. > >> Is there a version of type theory for proving and verifying, less > >> for computing? > > In my opinion the currenrly implemented type theories are essentially > > for proving and not for computing. > > But if you haven't mechanized PART of equational reasoning it would be > > much much more painful than it still is. > > But that is "only" a pragmatic issue. > > > >> The notations of type theory are very useful in homotopy theory. > >> But the absence of simplicial types is a serious obstacle to > applications. > > In cubical type theory they sort of live well with cubes not being > > fibrant... They have them as pretypes. But maybe I misunderstand... > > > > Thomas > > > > [-- Attachment #2: Type: text/html, Size: 7081 bytes --]

I thought so but now Nicolai says it is not? From a type-theoretic point of view it seems more natural to say that indexed M-types are fibrant even if the index is not. Saying that natural numbers are cofibrant assigns a special role to one particular inductive type. Thorsten On 10/05/2020, 15:35, "Michael Shulman" <shu...@sandiego.edu> wrote: Many or all coinductive types can be constructed, at least up to equivalence, using Pi-types and (some kind of) Nat. Is there any chance that "exo-Nat is cofibrant" could be used to justify the existence/fibrancy of the coinductive types you want? On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus <nicola...@gmail.com> wrote: > > On 10/05/2020 15:01, Michael Shulman wrote: > > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch > > <Thorsten....@nottingham.ac.uk> wrote: > >> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type > > We can certainly *talk* about simplicial types in 2LTT as exofunctors > > from the exocategory Delta to the exocategory Type. I assume the > > point you're making is that we don't have a (fibrant) *type of* > > simplicial types, whereas we do have a fibrant type of semisimplicial > > types (under appropriate axioms)? > > Judging from the rest of his message, I believe that Thorsten was > talking about the direct replacement construction in Christian's and my > abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant", > this gives us a fibrant type that one could call "simplicial types" (and > Thorsten does). But of course it's an encoding. If we decide to use such > encodings, I fear we may lose the main advantage that the "axiomatic" > representations in HoTT have, namely avoiding encodings. (I mean the > "main advantage" of HoTT compared to traditional approaches, e.g. taking > bisimplicial sets.) > > >> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist. > > Personally, I think the best axiom to use here is that exo-Nat is > > *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy. We > > don't know how to model "exo-Nat is fibrant" in all higher toposes, > > but it's easy to interpret "exo-Nat is cofibrant" in such models, > > since Pi-types with domain exo-Nat are just externally-infinite > > products. > > I completely agree with your preference for this axiom :-) > But Thorsten does has a point if we consider the "engineering level" > that was discussed earlier in this thread. Allowing coinductive types > with exo-Nat as an index makes it possible to use your paper (Higher > Stucture Identity Principle, arXiv:2004.06572) and get a construction of > semi-simplicial types which is more convenient to use in a proof assistant. > > -- Nicolai This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

```
On Sun, May 10, 2020 at 9:51 AM Nicolai Kraus <nicola...@gmail.com> wrote:
> It's easy to change the second definition to
> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
> is a nice way for the first definition.
On the other hand, it's easy to change the first definition to define
monoids/semigroups/rings/fields/lattices/universal-algebras/etc., and
impossible to do the same for the second. I think the fact that
groups are part of the general theory of algebraic structures on sets
is more important to incorporate in a definition. The equivalence
between groups and connected pointed 1-types is better viewed as a
theorem than a definition.
And hence, the "definition" of oo-groups as connected pointed types is
more of a hack than a true definition. In an ideal world, that would
be a theorem too. (And the corresponding theorem in classical
mathematics has important content: there are important oo-groupoids
that are obtained by delooping oo-groups nontrivially.)
```

[-- Attachment #1: Type: text/plain, Size: 3323 bytes --] On Sun, May 10, 2020 at 4:35 PM Ulrik Buchholtz <ulrikbu...@gmail.com> wrote: > No need to apologize: I know I was being slightly provocative by > juxtaposing a question about sets cover (SC) and a comment on 2-level type > theory in this context, in order to provoke some discussion :-) > It worked :-) > Wouldn't you agree, however, that even though basic 2LTT is conservative > over HoTT, from a certain point of view, 2LTT privileges the “ground floor” > exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you > decorate the inner (fibrant, endo-) types as special, and leave the > exotypes undecorated, privileging the latter. While from a user's > perspective, however, it's the (inner) types that are > standard/mathematical, and the exotypes that are special. > I think I see where you are coming from. But for me, decorating the inner types as special was simply a pragmatic choice, not a philosophical one. Since most/all statements in the paper are "proper" 2LTT, there are more exo- / outer types involved than endo- / inner ones. But as a user, one is interested in the fibrant types (and maybe even assumes that they coincide with the inner theory), and only adds some small exo-sprinkles like "exo-Nat is cofibrant"; then, it makes sense to decorate the exo-types instead, as e.g. in https://arxiv.org/abs/2004.06572 And maybe it would be less confusing if we did the same in the paper that you linked to. I'm not sure. > And regardless of the decorations, the mere fact that we bring in the > exoset level makes the theory harder to justify from the philosophical > position that general homotopy types are not reducible to sets. One can in > fact see the conservativity result as foundational reduction (in the sense > of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) > from a system justified by the principle that everything is based on sets > to a system justified by a framework where that isn't the case. > That's interesting, thanks for the link! > Another connection is that it seems it should be easier to find an axiom, > which might imply SC, that would allow us to construct the type of > semi-simplicial types, rather than such an axiom that doesn't imply SC. But > I don't know any such axiom statable in book HoTT either way. > Good question. > BTW, you probably meant “simplicial set” above. And yes, that kind of > axiom would be the strongest expression of “everything is based sets”, and > it currently needs 2LTT to even be stated. > You're right, I meant "set". (Otherwise it'd be silly, a type X is the realization of the [fibrant replacement of] the constant presheaf X.) Nicolai > Cheers, > Ulrik > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b470-28958f8d7713%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b470-28958f8d7713%40googlegroups.com?utm_medium=email&utm_source=footer> > . > [-- Attachment #2: Type: text/html, Size: 5003 bytes --]