[-- Attachment #1: Type: text/plain, Size: 926 bytes --] Good morning, The page for submitting a talk for the 2nd International Conference on Homotopy Type Theory, to take place at Carnegie Mellon University from Monday 22nd to Thursday 24th May, 2023, is now open: https://hott.github.io/HoTT-2023//call-for-papers/ The deadline for submissions is 3rd March 2023. Talks reporting on work in progress are welcome. With best wishes, Nicola Gambino (on behalf of the scientific committee) Dr Nicola Gambino Reader in Pure Mathematics Department of Mathematics, University of Manchester -- 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/C62D4D8E-4EDF-4CB5-A289-058E932677E8%40manchester.ac.uk. [-- Attachment #2: Type: text/html, Size: 1930 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 4374 bytes --] Dear All, I am forwarding the announcement below for the ACT conference 2023. According to the PC chairs, submissions on categorical semantics of type theories are very welcome. Benedikt 6th Annual International Conference on Applied Category Theory (ACT2023) July 31 - August 4, 2023 https://act2023.github.io/ The Sixth International Conference on Applied Category Theory will take place at the University of Maryland from 31 July to 4 August 2023, preceded by the Adjoint School 2023 from 24 to 28 July. This conference follows previous events at Strathclyde (UK), Cambridge (UK), Cambridge (MA), Oxford (UK) and Leiden (NL). Applied category theory is important to a growing community of researchers who study computer science, logic, engineering, physics, biology, chemistry, social science, systems, linguistics and other subjects using category-theoretic tools. The background and experience of our members is as varied as the systems being studied. The goal of the Applied Category Theory conference series is to bring researchers together, strengthen the applied category theory community, disseminate the latest results, and facilitate further development of the field. SUBMISSIONS We accept submissions in English of original research papers, talks about work accepted/submitted/published elsewhere, and demonstrations of relevant software. Accepted original research papers will be published in a proceedings volume. The conference will include an industry showcase event and community meeting. We particularly encourage people from underrepresented groups to submit their work and the organizers are committed to non-discrimination, equity, and inclusion. Original research papers intended for conference proceedings should present original, high-quality work in the style of a computer science conference paper (up to 12 pages, not counting the bibliography; more detailed parts of proofs may be included in an appendix for the convenience of the reviewers). Please use the EPTCS style files available at < http://style.eptcs.org>. Such submissions should not be an abridged version of an existing journal article although pre-submission arXiv preprints are permitted. These submissions will be adjudicated for both a talk and publication in the conference proceedings. IMPORTANT DATES The following dates are all in 2023, and Anywhere On Earth. - Submission Deadline: Wednesday 3 May - Author Notification: Wednesday 7 June - Camera-ready version due: Tuesday 27 June - Conference begins: 31 July PROGRAM COMMITTEE Benedikt Ahrens Mike Mislove Mario Álvarez Picallo Sean Moss Matteo Capucci David Jaz Myers Titouan Carette Susan Niefield Bryce Clarke Jason Parker Carmen Constantin Evan Patterson Geoffrey Cruttwell Paige Randall North Giovanni de Felice Sophie Raynor Bojana Femic Emily Roff Marcelo Fiore Morgan Rogers Fabio Gadducci Mario Román Zeinab Galal Maru Sarazola Richard Garner Bas Spitters Neil Ghani Sam Staton (co-chair) Tamara von Glehn Dario Stein Amar Hadzihasanovic Eswaran Subrahmanian Masahito Hasegawa Walter Tholen Martha Lewis Christina Vasilakopoulou (co-chair) Sophie Libkind Christine Vespa Rory Lucyshyn-Wright Simon Willerton Sandra Mantovanni Glynn Winskel Jade Master Vladimir Zamdzhiev Konstantinos Meichanetzidis Fabio Zanasi Stefan Milius ORGANIZING COMMITTEE James Fairbanks, University of Florida Joseph P. Moeller, National Institute for Standards and Technology, USA Sam Staton, Oxford University Priyaa Varshinee Srinivasan, National Institute for Standards and Technology, USA Christina Vasilakopoulou, National Technical University of Athens STEERING COMMITTEE John Baez, University of California, Riverside Bob Coecke, Cambridge Quantum Dorette Pronk, Dalhousie University David Spivak, Topos Institute -- 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/d75fc6a8-ee5d-4e81-8d4f-a27be1c247d3n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 5313 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 3789 bytes --] In this thread, I follow the approach in Egbert Rijke's textbook in having a separate type judgment, rather than the HoTT book's judgment in having an infinite tower of universes and no separate type judgment, and I follow Agda in using the bare equals sign for definitional equality. In structural set theories like William Lawvere's ETCS or Mike Shulman's SEAR it is quite common to have equality only for the sorts of elements, functions, and relations, and not have any primitive equality relation for the sort of sets. This means that the only way to compare sets for "equality" is through a bijection of sets. In addition, Mike Shulman's talks on Higher Observational Type Theory back in May of 2022 includes a section where he talks about the right notion of "definitional univalence" is not using the usual notion of definitional equality of types, but rather strict bijection, where there are functions idtoequiv(a, b):Id_U(a, b) -> Equiv_U(a, b) equivtoid(a, b):Equiv_U(a, b) -> Id_U(a, b) between the identity types Id_U(a, b) and the type of equivalences Equiv_U(a, b) of elements a:U and b:U of a universe U, and definitional equalities of elements equivtoid(a, b)(idtoequiv(a, b)(p)) = p:Id_U(a, b) idtoequiv(a, b)(equivtoid(a, b)(R)) = R:Equiv_U(a, b) Using insights from structural set theory, one could go beyond definitional univalence in Mike Shulman's Higher Observational Type Theory and directly modify the structural rules for definitional equality of types so that it behaves not as an equivalence relation a la first order logic with equality, but rather strict bijection of types a la structural set theory, using the following rules: Gamma |- A = B type --------------------------------- Gamma, x:A |- f(x):B Gamma |- A = B type --------------------------------- Gamma, y:B |- g(y):A Gamma |- A = B type --------------------------------- Gamma, x:A |- g(f(x)) = x:A Gamma |- A = B type --------------------------------- Gamma, y:B |- f(g(y)) = y:B The variable conversion rule in dependent type theory then becomes substitution of g(y) for x, Gamma |- A = A' type Gamma, x:A, Delta(x) |- J(x) ------------------------------------------------------------------------------------ Gamma, y:A', Delta(g(y)) |- J(g(y)) The first congruence rule for substitution is the following rule Gamma |- a = a':A Gamma, x:A, Delta(x) |- B(x) type ------------------------------------------------------------------------------------ Gamma, Delta(a) |- B(a) = B(a') type and the strict bijection rules for definitional equality of types implies that f and g for the definitional equality B(a) = B(a') type are judgmental versions of transport. The second congruence rule for substitution becomes merely a judgmental version of application to paths: Gamma |- a = a':A Gamma, x:A, Delta(x) |- b(x):B(x) type ------------------------------------------------------------------------------------------ Gamma, Delta(a) |- b(a) = g(b(a')):B(a) Definitional univalence then becomes under this collection of structural rules the following rule Gamma |- U type Gamma |- A:U Gamma |- B:U ------------------------------------------------------------------------------------------ Gamma |- Id_U(A, B) = Eq_U(A, B) type from which one could derive Mike Shulman's original 4 rules for definitionally univalent universes. Madeleine Birchfield -- 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/45bf6ae5-b73b-4df2-a8bc-9aca972797e1n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 4668 bytes --]

Hello everyone, I am happy to announce a workshop on Internal Methods in Algebraic Geometry from 17th to 20th April, 2023, in Gothenburg, Sweden. Note that this is fairly close to HoTT/UF '23 - if you want to have both, you have one day, the 21st of April, to travel from Gothenburg to Vienna. The two topics of the workshop are presentation and discussion of recent results internal to the Zariski topos and models of homotopy type theory together with the axioms for synthetic algebraic geometry we use. More information is available here: https://felix-cherubini.de/internal-workshop-2.html Some familiarity with HoTT, the Zariski topos and algebraic geometry will be assumed. If you would like to participate, write an email to felix.cherubini@posteo.de All the best, Felix Cherubini -- 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/e1b35cc4-5cf1-68d1-3e21-38335abc77c2%40gmail.com.

[-- Attachment #1: Type: text/plain, Size: 10342 bytes --] Ah, you're right, sorry. I was confusing "being able to name particular universes as function outputs" with "bounded universe polymorphism". I retract my claim. Best, Jason On Sun, Jan 29, 2023 at 6:38 AM András Kovács <puttamalac@gmail.com> wrote: > Jason: I agree that externally indexed products imply bounded universe > polymorphism, but I don't understand how we can derive inconsistency from > that together with rational levels. The operation that scales rational > levels can only be defined externally so it doesn't really affect the > possible internal constructions. > > To be clear, by external products I mean e.g. the following for i : ℚ > > Product : (ℕ → Tyᵢ Γ) → Tyᵢ Γ > lam : ((n : ℕ) → Tmᵢ Γ (A n)) → Tmᵢ Γ (Product A) > app : Tmᵢ Γ (Product A) → (n : ℕ) → Tmᵢ Γ (A n) > > Jason Gross <jasongross9@gmail.com> ezt írta (időpont: 2023. jan. 28., > Szo, 21:26): > >> > I don't think access to internal universe quantifications is an >> inherent consequence of infinitary constructors. I'd rather say that it's >> an accidental side effect of Mike's formulation from 2014 that something >> like "λ i. Type i" is possible, and it can easily be ruled out. In Section >> 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such >> infinitary type constructors is specified without allowing internal >> universe quantification. This is essentially because the externally indexed >> sequence of types still has to live in a single fixed universe. >> >> As I understand it, this just rules out universe qualification that is >> not bounded above by a fixed universe, right? It seems to me that you >> still get internal quantization over levels less than a fixed level. And >> this is enough to make the construction generating inconsistency with >> Q-indexed universes go through. >> >> On Sat, Jan 28, 2023, 12:46 Michael Shulman <shulman@sandiego.edu> wrote: >> >>> Also, apparently Agda's Set-omega breaks subject reduction: >>> https://github.com/agda/agda/issues/5810 >>> >>> On Sat, Jan 28, 2023 at 7:21 AM Nicolai Kraus <nicolai.kraus@gmail.com> >>> wrote: >>> > >>> > That's an interesting observation! However, I think the question of >>> universe hierarchies is orthogonal to the question of infinitary type >>> constructors. >>> > >>> > I don't think access to internal universe quantifications is an >>> inherent consequence of infinitary constructors. I'd rather say that it's >>> an accidental side effect of Mike's formulation from 2014 that something >>> like "λ i. Type i" is possible, and it can easily be ruled out. In Section >>> 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such >>> infinitary type constructors is specified without allowing internal >>> universe quantification. This is essentially because the externally indexed >>> sequence of types still has to live in a single fixed universe. >>> > >>> > Agda actually *does* allow something like "λ i. Type i". While I view >>> constructions using it more as proof schemes than as single proofs ("book >>> HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found >>> it very useful. Without something like this, I don't see how we could have >>> formalised the statement that "Universe Un is not an n-type in a hierarchy >>> U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would >>> *not* regard the formalisation [3] as a single proof. I see it as an >>> externally indexed family of Nat-many proofs, and it's only a lucky >>> accident (using a feature of Agda that isn't even part of the considered >>> type theory) that it can be implemented. >>> > >>> > [1] https://arxiv.org/abs/1705.03307 >>> > [2] https://arxiv.org/abs/1311.4002 >>> > [3] >>> https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html >>> > >>> > Best wishes, >>> > Nicolai >>> > >>> > >>> > >>> > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> >>> wrote: >>> >> >>> >> (Resurrecting this thread because I stumbled upon it while rereading >>> A Formalized Interpreter, and I believe I have something new to add.) >>> >> >>> >> As I understand it, using `□A` to mean "syntax for A", an infinitary >>> type theory has rules like `(A → □B) → □(A → B)`. (Note that this is >>> exactly what HOAS does, which explains why it's so easy to write an >>> interpreter for HOAS without running into the semisimplicial types >>> coherence issues.) >>> >> >>> >> > Are there other more serious problems with an infinitary type >>> theory? >>> >> I think the answer to this is "it depends". In "An Order-Theoretic >>> Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed >>> Mullanix have a consistency proof for a system with rational-indexed >>> universes (and no explicit universe level quantification). However, >>> infinitary rules give access to internal universe quantification (consider >>> the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level >>> quantification rules out any "fractal-like" scheme of universes (such as >>> the rationals), because we can write an interpreter for "terms using >>> universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 >>> (because we have enough universes to do that), and then we can embed terms >>> with universes between 0 and 2 back into terms with universes between 0 and >>> 1 (divide universe indices by 2), and this loop gives inconsistency by >>> Gödel / Löb. >>> >> >>> >> So at the very least, having infinitary limits rules out some of the >>> more exotic universe level structures. >>> >> >>> >> Best, >>> >> Jason >>> >> >>> >> >>> >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> >>> wrote: >>> >>> >>> >>> Since the problem of defining infinite structures has come up in >>> >>> another thread, it may be a good time to bring up this idea, which >>> has >>> >>> been kicking around in my head for a while. I know that something >>> >>> similar has occurred to others as well. >>> >>> >>> >>> Logicians study infinitary logics in addition to finitary ones. Why >>> >>> can't we have an infinitary type theory? >>> >>> >>> >>> An infinitary type theory would include type-forming operations which >>> >>> take infinitely many inputs ("infinite" in the sense of the >>> >>> metatheory). The most obvious would be, say, the cartesian product >>> of >>> >>> infinitely many types, e.g. given types A0, A1, A2, ... (with the >>> >>> indexing being by external natural numbers), we would have a type >>> >>> Prod_i(Ai), and so on. Semantically, this would correspond to a >>> >>> category having infinite products. >>> >>> >>> >>> More useful than this would be a category having limits of towers of >>> >>> fibrations. I think this can be represented as a type former in an >>> >>> infinitary type theory as well, with a rule like >>> >>> >>> >>> Gamma |- A0 : Type >>> >>> Gamma, a0:A0 |- A1(a0) : Type >>> >>> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type >>> >>> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type >>> >>> ... >>> >>> ---------------------------------------- >>> >>> Gamma |- lim_i A_i : Type >>> >>> >>> >>> Then we would have a corresponding introduction form, like >>> >>> >>> >>> Gamma |- x0 : A0 >>> >>> Gamma |- x1 : A1(x0) >>> >>> Gamma |- x2 : A1(x0,x1) >>> >>> ... >>> >>> ------------------------------------- >>> >>> Gamma |- lam_i xi : lim_i A_i >>> >>> >>> >>> with elimination and computation rules. We might also need an >>> >>> "infinitary extensionality" axiom. >>> >>> >>> >>> It seems that in such a type theory, we ought to have no trouble >>> >>> defining (say) semisimplicial types, as the limit of the appropriate >>> >>> externally-defined tower of fibrations. >>> >>> >>> >>> Has anyone studied infinitary type theories before? Of course, they >>> >>> probably won't have all the good properties of finitary ones. For >>> >>> instance, I think judgmental equality isn't going to be decidable, >>> >>> since there's no way to algorithmically test the infinitely many >>> terms >>> >>> that go into a lam_i for equality. But other proposals like HTS are >>> >>> also giving up decidability. Are there other more serious problems >>> >>> with an infinitary type theory? >>> >>> >>> >>> Mike >>> >>> >>> >>> -- >>> >>> 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. >>> >> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com >>> . >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com >> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.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/CAKObCaoZUnvTfEOPdX8nwOUZM_M%3DnEoszZYizE4%2BypoymDLozQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 13688 bytes --]

[-- Attachment #1: Type: text/plain, Size: 9852 bytes --] Jason: I agree that externally indexed products imply bounded universe polymorphism, but I don't understand how we can derive inconsistency from that together with rational levels. The operation that scales rational levels can only be defined externally so it doesn't really affect the possible internal constructions. To be clear, by external products I mean e.g. the following for i : ℚ Product : (ℕ → Tyᵢ Γ) → Tyᵢ Γ lam : ((n : ℕ) → Tmᵢ Γ (A n)) → Tmᵢ Γ (Product A) app : Tmᵢ Γ (Product A) → (n : ℕ) → Tmᵢ Γ (A n) Jason Gross <jasongross9@gmail.com> ezt írta (időpont: 2023. jan. 28., Szo, 21:26): > > I don't think access to internal universe quantifications is an inherent > consequence of infinitary constructors. I'd rather say that it's an > accidental side effect of Mike's formulation from 2014 that something like > "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, > strengthening A1-3 of the 2LTT paper [1], a type theory with such > infinitary type constructors is specified without allowing internal > universe quantification. This is essentially because the externally indexed > sequence of types still has to live in a single fixed universe. > > As I understand it, this just rules out universe qualification that is not > bounded above by a fixed universe, right? It seems to me that you still > get internal quantization over levels less than a fixed level. And this is > enough to make the construction generating inconsistency with Q-indexed > universes go through. > > On Sat, Jan 28, 2023, 12:46 Michael Shulman <shulman@sandiego.edu> wrote: > >> Also, apparently Agda's Set-omega breaks subject reduction: >> https://github.com/agda/agda/issues/5810 >> >> On Sat, Jan 28, 2023 at 7:21 AM Nicolai Kraus <nicolai.kraus@gmail.com> >> wrote: >> > >> > That's an interesting observation! However, I think the question of >> universe hierarchies is orthogonal to the question of infinitary type >> constructors. >> > >> > I don't think access to internal universe quantifications is an >> inherent consequence of infinitary constructors. I'd rather say that it's >> an accidental side effect of Mike's formulation from 2014 that something >> like "λ i. Type i" is possible, and it can easily be ruled out. In Section >> 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such >> infinitary type constructors is specified without allowing internal >> universe quantification. This is essentially because the externally indexed >> sequence of types still has to live in a single fixed universe. >> > >> > Agda actually *does* allow something like "λ i. Type i". While I view >> constructions using it more as proof schemes than as single proofs ("book >> HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found >> it very useful. Without something like this, I don't see how we could have >> formalised the statement that "Universe Un is not an n-type in a hierarchy >> U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would >> *not* regard the formalisation [3] as a single proof. I see it as an >> externally indexed family of Nat-many proofs, and it's only a lucky >> accident (using a feature of Agda that isn't even part of the considered >> type theory) that it can be implemented. >> > >> > [1] https://arxiv.org/abs/1705.03307 >> > [2] https://arxiv.org/abs/1311.4002 >> > [3] >> https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html >> > >> > Best wishes, >> > Nicolai >> > >> > >> > >> > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> >> wrote: >> >> >> >> (Resurrecting this thread because I stumbled upon it while rereading A >> Formalized Interpreter, and I believe I have something new to add.) >> >> >> >> As I understand it, using `□A` to mean "syntax for A", an infinitary >> type theory has rules like `(A → □B) → □(A → B)`. (Note that this is >> exactly what HOAS does, which explains why it's so easy to write an >> interpreter for HOAS without running into the semisimplicial types >> coherence issues.) >> >> >> >> > Are there other more serious problems with an infinitary type theory? >> >> I think the answer to this is "it depends". In "An Order-Theoretic >> Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed >> Mullanix have a consistency proof for a system with rational-indexed >> universes (and no explicit universe level quantification). However, >> infinitary rules give access to internal universe quantification (consider >> the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level >> quantification rules out any "fractal-like" scheme of universes (such as >> the rationals), because we can write an interpreter for "terms using >> universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 >> (because we have enough universes to do that), and then we can embed terms >> with universes between 0 and 2 back into terms with universes between 0 and >> 1 (divide universe indices by 2), and this loop gives inconsistency by >> Gödel / Löb. >> >> >> >> So at the very least, having infinitary limits rules out some of the >> more exotic universe level structures. >> >> >> >> Best, >> >> Jason >> >> >> >> >> >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> >> wrote: >> >>> >> >>> Since the problem of defining infinite structures has come up in >> >>> another thread, it may be a good time to bring up this idea, which has >> >>> been kicking around in my head for a while. I know that something >> >>> similar has occurred to others as well. >> >>> >> >>> Logicians study infinitary logics in addition to finitary ones. Why >> >>> can't we have an infinitary type theory? >> >>> >> >>> An infinitary type theory would include type-forming operations which >> >>> take infinitely many inputs ("infinite" in the sense of the >> >>> metatheory). The most obvious would be, say, the cartesian product of >> >>> infinitely many types, e.g. given types A0, A1, A2, ... (with the >> >>> indexing being by external natural numbers), we would have a type >> >>> Prod_i(Ai), and so on. Semantically, this would correspond to a >> >>> category having infinite products. >> >>> >> >>> More useful than this would be a category having limits of towers of >> >>> fibrations. I think this can be represented as a type former in an >> >>> infinitary type theory as well, with a rule like >> >>> >> >>> Gamma |- A0 : Type >> >>> Gamma, a0:A0 |- A1(a0) : Type >> >>> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type >> >>> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type >> >>> ... >> >>> ---------------------------------------- >> >>> Gamma |- lim_i A_i : Type >> >>> >> >>> Then we would have a corresponding introduction form, like >> >>> >> >>> Gamma |- x0 : A0 >> >>> Gamma |- x1 : A1(x0) >> >>> Gamma |- x2 : A1(x0,x1) >> >>> ... >> >>> ------------------------------------- >> >>> Gamma |- lam_i xi : lim_i A_i >> >>> >> >>> with elimination and computation rules. We might also need an >> >>> "infinitary extensionality" axiom. >> >>> >> >>> It seems that in such a type theory, we ought to have no trouble >> >>> defining (say) semisimplicial types, as the limit of the appropriate >> >>> externally-defined tower of fibrations. >> >>> >> >>> Has anyone studied infinitary type theories before? Of course, they >> >>> probably won't have all the good properties of finitary ones. For >> >>> instance, I think judgmental equality isn't going to be decidable, >> >>> since there's no way to algorithmically test the infinitely many terms >> >>> that go into a lam_i for equality. But other proposals like HTS are >> >>> also giving up decidability. Are there other more serious problems >> >>> with an infinitary type theory? >> >>> >> >>> Mike >> >>> >> >>> -- >> >>> 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. >> >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com >> . >> > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.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/CAA3CDBYe%2BOnZedPWdVNLKJKfWwM77gVe_-7v4WmU%3DwQd17EkdA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 12958 bytes --]

[-- Attachment #1: Type: text/plain, Size: 8403 bytes --] > I don't think access to internal universe quantifications is an inherent consequence of infinitary constructors. I'd rather say that it's an accidental side effect of Mike's formulation from 2014 that something like "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary type constructors is specified without allowing internal universe quantification. This is essentially because the externally indexed sequence of types still has to live in a single fixed universe. As I understand it, this just rules out universe qualification that is not bounded above by a fixed universe, right? It seems to me that you still get internal quantization over levels less than a fixed level. And this is enough to make the construction generating inconsistency with Q-indexed universes go through. On Sat, Jan 28, 2023, 12:46 Michael Shulman <shulman@sandiego.edu> wrote: > Also, apparently Agda's Set-omega breaks subject reduction: > https://github.com/agda/agda/issues/5810 > > On Sat, Jan 28, 2023 at 7:21 AM Nicolai Kraus <nicolai.kraus@gmail.com> > wrote: > > > > That's an interesting observation! However, I think the question of > universe hierarchies is orthogonal to the question of infinitary type > constructors. > > > > I don't think access to internal universe quantifications is an inherent > consequence of infinitary constructors. I'd rather say that it's an > accidental side effect of Mike's formulation from 2014 that something like > "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, > strengthening A1-3 of the 2LTT paper [1], a type theory with such > infinitary type constructors is specified without allowing internal > universe quantification. This is essentially because the externally indexed > sequence of types still has to live in a single fixed universe. > > > > Agda actually *does* allow something like "λ i. Type i". While I view > constructions using it more as proof schemes than as single proofs ("book > HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found > it very useful. Without something like this, I don't see how we could have > formalised the statement that "Universe Un is not an n-type in a hierarchy > U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would > *not* regard the formalisation [3] as a single proof. I see it as an > externally indexed family of Nat-many proofs, and it's only a lucky > accident (using a feature of Agda that isn't even part of the considered > type theory) that it can be implemented. > > > > [1] https://arxiv.org/abs/1705.03307 > > [2] https://arxiv.org/abs/1311.4002 > > [3] > https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html > > > > Best wishes, > > Nicolai > > > > > > > > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> > wrote: > >> > >> (Resurrecting this thread because I stumbled upon it while rereading A > Formalized Interpreter, and I believe I have something new to add.) > >> > >> As I understand it, using `□A` to mean "syntax for A", an infinitary > type theory has rules like `(A → □B) → □(A → B)`. (Note that this is > exactly what HOAS does, which explains why it's so easy to write an > interpreter for HOAS without running into the semisimplicial types > coherence issues.) > >> > >> > Are there other more serious problems with an infinitary type theory? > >> I think the answer to this is "it depends". In "An Order-Theoretic > Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed > Mullanix have a consistency proof for a system with rational-indexed > universes (and no explicit universe level quantification). However, > infinitary rules give access to internal universe quantification (consider > the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level > quantification rules out any "fractal-like" scheme of universes (such as > the rationals), because we can write an interpreter for "terms using > universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 > (because we have enough universes to do that), and then we can embed terms > with universes between 0 and 2 back into terms with universes between 0 and > 1 (divide universe indices by 2), and this loop gives inconsistency by > Gödel / Löb. > >> > >> So at the very least, having infinitary limits rules out some of the > more exotic universe level structures. > >> > >> Best, > >> Jason > >> > >> > >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> > wrote: > >>> > >>> Since the problem of defining infinite structures has come up in > >>> another thread, it may be a good time to bring up this idea, which has > >>> been kicking around in my head for a while. I know that something > >>> similar has occurred to others as well. > >>> > >>> Logicians study infinitary logics in addition to finitary ones. Why > >>> can't we have an infinitary type theory? > >>> > >>> An infinitary type theory would include type-forming operations which > >>> take infinitely many inputs ("infinite" in the sense of the > >>> metatheory). The most obvious would be, say, the cartesian product of > >>> infinitely many types, e.g. given types A0, A1, A2, ... (with the > >>> indexing being by external natural numbers), we would have a type > >>> Prod_i(Ai), and so on. Semantically, this would correspond to a > >>> category having infinite products. > >>> > >>> More useful than this would be a category having limits of towers of > >>> fibrations. I think this can be represented as a type former in an > >>> infinitary type theory as well, with a rule like > >>> > >>> Gamma |- A0 : Type > >>> Gamma, a0:A0 |- A1(a0) : Type > >>> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type > >>> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type > >>> ... > >>> ---------------------------------------- > >>> Gamma |- lim_i A_i : Type > >>> > >>> Then we would have a corresponding introduction form, like > >>> > >>> Gamma |- x0 : A0 > >>> Gamma |- x1 : A1(x0) > >>> Gamma |- x2 : A1(x0,x1) > >>> ... > >>> ------------------------------------- > >>> Gamma |- lam_i xi : lim_i A_i > >>> > >>> with elimination and computation rules. We might also need an > >>> "infinitary extensionality" axiom. > >>> > >>> It seems that in such a type theory, we ought to have no trouble > >>> defining (say) semisimplicial types, as the limit of the appropriate > >>> externally-defined tower of fibrations. > >>> > >>> Has anyone studied infinitary type theories before? Of course, they > >>> probably won't have all the good properties of finitary ones. For > >>> instance, I think judgmental equality isn't going to be decidable, > >>> since there's no way to algorithmically test the infinitely many terms > >>> that go into a lam_i for equality. But other proposals like HTS are > >>> also giving up decidability. Are there other more serious problems > >>> with an infinitary type theory? > >>> > >>> Mike > >>> > >>> -- > >>> 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. > >> To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 11155 bytes --]

Also, apparently Agda's Set-omega breaks subject reduction: https://github.com/agda/agda/issues/5810 On Sat, Jan 28, 2023 at 7:21 AM Nicolai Kraus <nicolai.kraus@gmail.com> wrote: > > That's an interesting observation! However, I think the question of universe hierarchies is orthogonal to the question of infinitary type constructors. > > I don't think access to internal universe quantifications is an inherent consequence of infinitary constructors. I'd rather say that it's an accidental side effect of Mike's formulation from 2014 that something like "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary type constructors is specified without allowing internal universe quantification. This is essentially because the externally indexed sequence of types still has to live in a single fixed universe. > > Agda actually *does* allow something like "λ i. Type i". While I view constructions using it more as proof schemes than as single proofs ("book HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found it very useful. Without something like this, I don't see how we could have formalised the statement that "Universe Un is not an n-type in a hierarchy U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would *not* regard the formalisation [3] as a single proof. I see it as an externally indexed family of Nat-many proofs, and it's only a lucky accident (using a feature of Agda that isn't even part of the considered type theory) that it can be implemented. > > [1] https://arxiv.org/abs/1705.03307 > [2] https://arxiv.org/abs/1311.4002 > [3] https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html > > Best wishes, > Nicolai > > > > On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> wrote: >> >> (Resurrecting this thread because I stumbled upon it while rereading A Formalized Interpreter, and I believe I have something new to add.) >> >> As I understand it, using `□A` to mean "syntax for A", an infinitary type theory has rules like `(A → □B) → □(A → B)`. (Note that this is exactly what HOAS does, which explains why it's so easy to write an interpreter for HOAS without running into the semisimplicial types coherence issues.) >> >> > Are there other more serious problems with an infinitary type theory? >> I think the answer to this is "it depends". In "An Order-Theoretic Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed Mullanix have a consistency proof for a system with rational-indexed universes (and no explicit universe level quantification). However, infinitary rules give access to internal universe quantification (consider the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level quantification rules out any "fractal-like" scheme of universes (such as the rationals), because we can write an interpreter for "terms using universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 (because we have enough universes to do that), and then we can embed terms with universes between 0 and 2 back into terms with universes between 0 and 1 (divide universe indices by 2), and this loop gives inconsistency by Gödel / Löb. >> >> So at the very least, having infinitary limits rules out some of the more exotic universe level structures. >> >> Best, >> Jason >> >> >> On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> wrote: >>> >>> Since the problem of defining infinite structures has come up in >>> another thread, it may be a good time to bring up this idea, which has >>> been kicking around in my head for a while. I know that something >>> similar has occurred to others as well. >>> >>> Logicians study infinitary logics in addition to finitary ones. Why >>> can't we have an infinitary type theory? >>> >>> An infinitary type theory would include type-forming operations which >>> take infinitely many inputs ("infinite" in the sense of the >>> metatheory). The most obvious would be, say, the cartesian product of >>> infinitely many types, e.g. given types A0, A1, A2, ... (with the >>> indexing being by external natural numbers), we would have a type >>> Prod_i(Ai), and so on. Semantically, this would correspond to a >>> category having infinite products. >>> >>> More useful than this would be a category having limits of towers of >>> fibrations. I think this can be represented as a type former in an >>> infinitary type theory as well, with a rule like >>> >>> Gamma |- A0 : Type >>> Gamma, a0:A0 |- A1(a0) : Type >>> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type >>> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type >>> ... >>> ---------------------------------------- >>> Gamma |- lim_i A_i : Type >>> >>> Then we would have a corresponding introduction form, like >>> >>> Gamma |- x0 : A0 >>> Gamma |- x1 : A1(x0) >>> Gamma |- x2 : A1(x0,x1) >>> ... >>> ------------------------------------- >>> Gamma |- lam_i xi : lim_i A_i >>> >>> with elimination and computation rules. We might also need an >>> "infinitary extensionality" axiom. >>> >>> It seems that in such a type theory, we ought to have no trouble >>> defining (say) semisimplicial types, as the limit of the appropriate >>> externally-defined tower of fibrations. >>> >>> Has anyone studied infinitary type theories before? Of course, they >>> probably won't have all the good properties of finitary ones. For >>> instance, I think judgmental equality isn't going to be decidable, >>> since there's no way to algorithmically test the infinitely many terms >>> that go into a lam_i for equality. But other proposals like HTS are >>> also giving up decidability. Are there other more serious problems >>> with an infinitary type theory? >>> >>> Mike >>> >>> -- >>> 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. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpypv0OieLCmivNYHYf7f8VnN1zWaKbafO-EP7kkPxg1dA%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 7160 bytes --] That's an interesting observation! However, I think the question of universe hierarchies is orthogonal to the question of infinitary type constructors. I don't think access to internal universe quantifications is an inherent consequence of infinitary constructors. I'd rather say that it's an accidental side effect of Mike's formulation from 2014 that something like "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary type constructors is specified without allowing internal universe quantification. This is essentially because the externally indexed sequence of types still has to live in a single fixed universe. Agda actually *does* allow something like "λ i. Type i". While I view constructions using it more as proof schemes than as single proofs ("book HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found it very useful. Without something like this, I don't see how we could have formalised the statement that "Universe Un is not an n-type in a hierarchy U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would *not* regard the formalisation [3] as a single proof. I see it as an externally indexed family of Nat-many proofs, and it's only a lucky accident (using a feature of Agda that isn't even part of the considered type theory) that it can be implemented. [1] https://arxiv.org/abs/1705.03307 [2] https://arxiv.org/abs/1311.4002 [3] https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html Best wishes, Nicolai On Fri, Jan 27, 2023 at 8:41 PM Jason Gross <jasongross9@gmail.com> wrote: > (Resurrecting this thread because I stumbled upon it while rereading A > Formalized Interpreter > <https://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/>, > and I believe I have something new to add.) > > As I understand it, using `□A` to mean "syntax for A", an infinitary type > theory has rules like `(A → □B) → □(A → B)`. (Note that this is exactly > what HOAS does, which explains why it's so easy to write an interpreter for > HOAS without running into the semisimplicial types coherence issues.) > > > Are there other more serious problems with an infinitary type theory? > I think the answer to this is "it depends". In "An Order-Theoretic > Analysis of Universe Polymorphism" <https://favonia.org/files/mugen.pdf>, > Favonia, Carlo Angiuli, and Reed Mullanix have a consistency proof for a > system with rational-indexed universes (and no explicit universe level > quantification). However, infinitary rules give access to internal > universe quantification (consider the function `λ i. "Type"ᵢ`). I believe > HOAS-like internal-level quantification rules out any "fractal-like" scheme > of universes (such as the rationals), because we can write an interpreter > for "terms using universes i with 0 <= i <= 1" into terms that use > universes between 0 and 2 (because we have enough universes to do that), > and then we can embed terms with universes between 0 and 2 back into terms > with universes between 0 and 1 (divide universe indices by 2), and this > loop gives inconsistency by Gödel / Löb. > > So at the very least, having infinitary limits rules out some of the more > exotic universe level structures. > > Best, > Jason > > > On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> > wrote: > >> Since the problem of defining infinite structures has come up in >> another thread, it may be a good time to bring up this idea, which has >> been kicking around in my head for a while. I know that something >> similar has occurred to others as well. >> >> Logicians study infinitary logics in addition to finitary ones. Why >> can't we have an infinitary type theory? >> >> An infinitary type theory would include type-forming operations which >> take infinitely many inputs ("infinite" in the sense of the >> metatheory). The most obvious would be, say, the cartesian product of >> infinitely many types, e.g. given types A0, A1, A2, ... (with the >> indexing being by external natural numbers), we would have a type >> Prod_i(Ai), and so on. Semantically, this would correspond to a >> category having infinite products. >> >> More useful than this would be a category having limits of towers of >> fibrations. I think this can be represented as a type former in an >> infinitary type theory as well, with a rule like >> >> Gamma |- A0 : Type >> Gamma, a0:A0 |- A1(a0) : Type >> Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type >> Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type >> ... >> ---------------------------------------- >> Gamma |- lim_i A_i : Type >> >> Then we would have a corresponding introduction form, like >> >> Gamma |- x0 : A0 >> Gamma |- x1 : A1(x0) >> Gamma |- x2 : A1(x0,x1) >> ... >> ------------------------------------- >> Gamma |- lam_i xi : lim_i A_i >> >> with elimination and computation rules. We might also need an >> "infinitary extensionality" axiom. >> >> It seems that in such a type theory, we ought to have no trouble >> defining (say) semisimplicial types, as the limit of the appropriate >> externally-defined tower of fibrations. >> >> Has anyone studied infinitary type theories before? Of course, they >> probably won't have all the good properties of finitary ones. For >> instance, I think judgmental equality isn't going to be decidable, >> since there's no way to algorithmically test the infinitely many terms >> that go into a lam_i for equality. But other proposals like HTS are >> also giving up decidability. Are there other more serious problems >> with an infinitary type theory? >> >> Mike >> >> -- >> 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. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.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/CA%2BAZBBqyc%3DyjbeNbcmdWRXnyyBzaUu3G1x2Mp5cdZA8Asg5oLQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 9061 bytes --]

[-- Attachment #1: Type: text/plain, Size: 4725 bytes --] (Resurrecting this thread because I stumbled upon it while rereading A Formalized Interpreter <https://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/>, and I believe I have something new to add.) As I understand it, using `□A` to mean "syntax for A", an infinitary type theory has rules like `(A → □B) → □(A → B)`. (Note that this is exactly what HOAS does, which explains why it's so easy to write an interpreter for HOAS without running into the semisimplicial types coherence issues.) > Are there other more serious problems with an infinitary type theory? I think the answer to this is "it depends". In "An Order-Theoretic Analysis of Universe Polymorphism" <https://favonia.org/files/mugen.pdf>, Favonia, Carlo Angiuli, and Reed Mullanix have a consistency proof for a system with rational-indexed universes (and no explicit universe level quantification). However, infinitary rules give access to internal universe quantification (consider the function `λ i. "Type"ᵢ`). I believe HOAS-like internal-level quantification rules out any "fractal-like" scheme of universes (such as the rationals), because we can write an interpreter for "terms using universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 (because we have enough universes to do that), and then we can embed terms with universes between 0 and 2 back into terms with universes between 0 and 1 (divide universe indices by 2), and this loop gives inconsistency by Gödel / Löb. So at the very least, having infinitary limits rules out some of the more exotic universe level structures. Best, Jason On Sun, Jun 22, 2014 at 2:05 AM Michael Shulman <shulman@sandiego.edu> wrote: > Since the problem of defining infinite structures has come up in > another thread, it may be a good time to bring up this idea, which has > been kicking around in my head for a while. I know that something > similar has occurred to others as well. > > Logicians study infinitary logics in addition to finitary ones. Why > can't we have an infinitary type theory? > > An infinitary type theory would include type-forming operations which > take infinitely many inputs ("infinite" in the sense of the > metatheory). The most obvious would be, say, the cartesian product of > infinitely many types, e.g. given types A0, A1, A2, ... (with the > indexing being by external natural numbers), we would have a type > Prod_i(Ai), and so on. Semantically, this would correspond to a > category having infinite products. > > More useful than this would be a category having limits of towers of > fibrations. I think this can be represented as a type former in an > infinitary type theory as well, with a rule like > > Gamma |- A0 : Type > Gamma, a0:A0 |- A1(a0) : Type > Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type > Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type > ... > ---------------------------------------- > Gamma |- lim_i A_i : Type > > Then we would have a corresponding introduction form, like > > Gamma |- x0 : A0 > Gamma |- x1 : A1(x0) > Gamma |- x2 : A1(x0,x1) > ... > ------------------------------------- > Gamma |- lam_i xi : lim_i A_i > > with elimination and computation rules. We might also need an > "infinitary extensionality" axiom. > > It seems that in such a type theory, we ought to have no trouble > defining (say) semisimplicial types, as the limit of the appropriate > externally-defined tower of fibrations. > > Has anyone studied infinitary type theories before? Of course, they > probably won't have all the good properties of finitary ones. For > instance, I think judgmental equality isn't going to be decidable, > since there's no way to algorithmically test the infinitely many terms > that go into a lam_i for equality. But other proposals like HTS are > also giving up decidability. Are there other more serious problems > with an infinitary type theory? > > Mike > > -- > 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5945 bytes --]

Congratulations Emily! And thanks for making room for HoTT at MLQ. Best wishes, Steve > On Jan 27, 2023, at 02:25, 'EMILY RIEHL' via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> wrote: > > Hi everyone, > > I'm writing to let you all know that I've recently joined the editorial board of Mathematical Logic Quarterly: > > https://onlinelibrary.wiley.com/journal/15213870 > > With the support of the managing editors, I'd be happy to consider homotopy type theory papers for potential publication there. > > Manuscripts should be submitted via the editorial management system linked above. While I'm still learning my way around the journal, I'd be happy to try to answer any questions you might have. > > All best, > Emily Riehl > > -- > Professor of Mathematics (she/her) > Johns Hopkins University > emilyriehl.github.io > > -- > 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/7bd3627a-3d12-13ad-3f94-f62057be0648%40jh.edu. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/FBF3D240-27DF-4266-8D5C-A336AF089502%40cmu.edu.

Hi everyone, I'm writing to let you all know that I've recently joined the editorial board of Mathematical Logic Quarterly: https://onlinelibrary.wiley.com/journal/15213870 With the support of the managing editors, I'd be happy to consider homotopy type theory papers for potential publication there. Manuscripts should be submitted via the editorial management system linked above. While I'm still learning my way around the journal, I'd be happy to try to answer any questions you might have. All best, Emily Riehl -- Professor of Mathematics (she/her) Johns Hopkins University emilyriehl.github.io -- 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/7bd3627a-3d12-13ad-3f94-f62057be0648%40jh.edu.

[-- Attachment #1.1: Type: text/plain, Size: 2135 bytes --] The **second meeting of Working Group 6 of EuroProofNet** will take place in Vienna, Austria, on 24-25 April 2023. <https://europroofnet.github.io/wg6-vienna/> <https://europroofnet.github.io/wg6-vienna/> It is colocated with the Workshop on Homotopy Type Theory/Univalent Foundations (HoTT/UF), which takes place on 22-23 April 2023. <https://hott-uf.github.io/2023/> <https://hott-uf.github.io/2023/> The aim of this meeting series is to bring together researchers working on the topics of WG6. The main focus is thus on the syntax and semantics of type theory. <https://europroofnet.github.io/wg6/> <https://europroofnet.github.io/wg6/> We invite submission of talk proposals (about 1 paragraph). The programme will consists mainly of short talks, and plenty of time for discussion. The meeting will be in person and is open to anyone interested in type theory. Registration will be open soon. To register please follow the link on the event's webpage. A limited amount of funding is available to reimburse expenses. The application for funding will be open together with registration. **Invited speakers** Daniel Gratzer Ambroise Lafont Anders Mörtberg Loïc Pujet **Deadlines** (AoE) Submission of talk proposals: Monday 27 February Author notification: Tuesday 7 March Funding requests: Thursday 19 March Registration: Friday 7 April **Scientific Organisers** Jacopo Emmenegger (University of Genoa) Paige Randall North (Utrecht University) **Local Organiser** Anja Petković Komel (TU Wien) -- Jacopo Emmenegger Postdoctoral research fellow Dipartimento di Matematica (DIMA) Università degli Studi di Genova Genova 16146, Italy -- 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/d5c5864a-1248-48a5-9579-9f844853fac0n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2852 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1398 bytes --] *** 2nd International Conference on Homotopy Type Theory (HoTT 2023) *** Monday 22nd May - Thursday 25th May, 2023 *** Carnegie Mellon University, Pittsburgh (USA) This is the first call for papers for the 2nd International Conference on Homotopy Type Theory (HoTT 2023). Abstracts (no more than 2 pages in A4 format) should be submitted via Easychair, using the following link. https://easychair.org/conferences/?conf=hott2023 <https://easychair.org/conferences/?conf=hott2023> Submissions open on 3rd February 2023 and close on 3rd March 2023. Invited speakers of the conference are: Julie Bergner (University of Virginia, USA) Thierry Coquand (Chalmers University, Sweden) András Kovács (Eötvös Loránd University, Hungary) Anders Mörtberg (Stockholm University) Further information on the conference can be found at the website: https://hott.github.io/HoTT-2023/ <https://hott.github.io/HoTT-2023/> With best regards, Steve Awodey (Chair of the organising committee) -- 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/80C492D2-43F7-446F-8D0E-1A26DBFD726A%40cmu.edu. [-- Attachment #2: Type: text/html, Size: 2737 bytes --]

As usual, we have openings for strong graduate applicants in all areas, and I in particular welcome applicants interested in HoTT, homotopy theory and higher categories. Our department has lots of people working on these topics and many visitors and seminars. Note that the deadline of February 1 is coming soon, but that applications will continue to be reviewed after that. Our standard ad is below. Best, Dan ----- Please distribute to undergraduate and master's students and appropriate counsellors and supervisors. Graduate Student Positions Department of Mathematics University of Western Ontario London, Ontario, Canada The Department of Mathematics at the University of Western Ontario solicits applications for its MSc and PhD programs. We have a large number of fully funded positions available, and applicants from any country are welcome. Our faculty members supervise research in a variety of areas: http://www.math.uwo.ca/graduate/supervisors.html The Department of Mathematics is part of the School of Mathematical Sciences: http://uwo.ca/smss/ More information about our program, including the application procedure, is available at http://www.math.uwo.ca/graduate/ Students normally start in September, in which case applications should be complete (including letters of reference and supplementary material) by February 1. Applications received after this deadline will be reviewed as space permits. Early applications are welcome, and we encourage applicants to apply for external scholarships they are eligible for. Please contact math-grad-program@uwo.ca with any questions you may have. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/874jsprpeh.fsf%40uwo.ca.

[-- Attachment #1.1: Type: text/plain, Size: 5417 bytes --] Congratulations on finishing this textbook, Egbert! This textbook, in its draft format, has been very useful in my learning of homotopy type theory as a foundations of mathematics back a few years ago, and I'm glad to see it finished and hopefully published and available in hardcover format soon. As for the splitting of the textbook in two, I actually agree with the decision to remove the material on using homotopy type theory for synthetic homotopy theory from the textbook, so that this textbook focuses on the foundational aspects of homotopy type theory. However, I do have to agree with Jon that I hope the second half of the textbook gets published as its own textbook; my preferred title would probably be "Synthetic Homotopy Theory" since much of the removed material was specifically about synthetic homotopy theory. Thanks, Madeleine Birchfield On Tuesday, January 3, 2023 at 11:06:11 PM UTC+1 j...@jonmsterling.com wrote: > Hi all, > > I second Urs's congratulations on this great achievement! Just want to > also add that I likewise miss the material on descent & flattening, for > which your old notes provided an excellent reference. Of course, perhaps > this leaves room for an "Advanced Topics in Homotopy Type Theory" followup > ;-) > > Best, > Jon > > > On 3 Jan 2023, at 20:16, 'Urs Schreiber' via Homotopy Type Theory wrote: > > > Hi Egbert, > > > > nice to see your notes now available in a stably referenceable way! > > They could fill quite a few gaps that the existing textbook literature > > leaves open. > > > > On that note, it seems that a fair bit of material has been removed in > > the arXiv version? > > (Maybe to make room for large margins?) > > > > For referencing on the nLab I now find myself pointing mainly to the > > version of your notes from 2018 (these here: > > https://www.andrew.cmu.edu/user/erijke/hott/hott_intro.pdf), which > > have discussion for instance of homotopy pullbacks/pushouts that seem > > to have later been dropped, together with much material depending on > > these notions (if I am seeing this correctly ?) > > > > I can imagine this is at least in large part the publisher's decision, > > but just to say that if there is any wiggle room left, then I would > > think it most worthwhile if these topics could make it into the final > > book version. > > > > All my best wishes for the New Year, > > Urs > > > > On Fri, Dec 23, 2022 at 1:54 PM Egbert Rijke <e.m....@gmail.com> wrote: > >> > >> Dear homotopy type theorists, > >> > >> My textbook Introduction to Homotopy Type Theory is finished and > available on the ArXiv: > >> > >> https://arxiv.org/abs/2212.11082 > >> > >> From the abstract: > >> This is an introductory textbook to univalent mathematics and homotopy > type theory, a mathematical foundation that takes advantage of the > structural nature of mathematical definitions and constructions. It is > common in mathematical practice to consider equivalent objects to be the > same, for example, to identify isomorphic groups. In set theory it is not > possible to make this common practice formal. For example, there are as > many distinct trivial groups in set theory as there are distinct singleton > sets. Type theory, on the other hand, takes a more structural approach to > the foundations of mathematics that accommodates the univalence axiom. > This, however, requires us to rethink what it means for two objects to be > equal. This textbook introduces the reader to Martin-Löf's dependent type > theory, to the central concepts of univalent mathematics, and shows the > reader how to do mathematics from a univalent point of view. Over 200 > exercises are included to train the reader in type theoretic reasoning. The > book is entirely self-contained, and in particular no prior familiarity > with type theory or homotopy theory is assumed. > >> > >> Over Christmas I will write a blog post in which I will go more into > the content of the book. For now: Enjoy! > >> > >> Happy holidays to everyone! > >> 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 HomotopyTypeThe...@googlegroups.com. > >> To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com > . > > > > -- > > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeThe...@googlegroups.com. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%40mail.gmail.com > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/f641a5c8-ea0b-4e82-a2f2-c9c1a8205d94n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 7779 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2919 bytes --] ========================================================== CALL FOR CONTRIBUTIONS AND PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF 2023, co-located with WG6 meeting of the EuroProofNet COST action) ========================================================== ------------------------------------------------------------------------ Workshop on Homotopy Type Theory and Univalent Foundations April 22 - 23, 2023, Vienna, Austria https://hott-uf.github.io/2023/ Co-located with WG6 meeting in Vienna in April 2023 https://europroofnet.github.io/wg6-vienna/ Abstract submission deadline: Feb 17, 2023 ------------------------------------------------------------------------ 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/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. The workshop will be held in person with some support for remote participation. ============================ # Invited speakers * Greta Coraglia (University of Genova, Italy) * Nima Rasekh (Max Planck Institute for Mathematics, Germany) * Egbert Rijke (University of Ljubljana, Slovenia) ================ # Submissions * Abstract submission deadline: February 17, 2023 * Author notification: early March 2023 Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=hottuf2023. 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. ================ # Registration Registration is mandatory. Registration information will be provided shortly. ================ # Organizers * Evan Cavallo, evan.cavallo@math.su.se (Stockholm University) * Anja Petković Komel, anja.komel@tuwien.ac.at (TU Wien) * Taichi Uemura, taichi.uemura@math.su.se (Stockholm University) * Jonathan Weinberger, jweinb20@jhu.edu (Johns Hopkins University) -- 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/CAOOoPfX_xPu%3DSp3YqQQriFRYSYfRehEkT7__a0stgMyiFP0j_g%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3668 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 4015 bytes --] Dear all, this is a reminder that the application window for the Nottingham PhD studentships will close soonish. I wrote in the previous message that the deadline is the 12th of February 2023, but please note that this is the day by which the university needs to receive formal applications. Before a formal application can be submitted, applicants already need to have the confirmed support of their potential future supervisor and discussed the application. If you would like to apply for a studentship in Nottingham, please contact us as soon as possible! I'm always happy to talk about it if you're interested. Best wishes, Nicolai On Monday, November 21, 2022 at 1:20:50 PM UTC Nicolai Kraus wrote: > Dear all, > > The School of Computer Science at the University of Nottingham > in the UK is seeking applications for 10 fully-funded PhD > studentships: https://tinyurl.com/ten-phd-2022 > > Applicants in the area of the Functional Programming Lab > (tinyurl.com/fp-notts) are strongly encouraged! If you are > interested in applying, please contact a potential supervisor > as soon as possible; the application deadline is 12th Feb 2023: > > Thorsten Altenkirch - constructive logic, proof assistants, > homotopy type theory, category theory, lambda calculus. > > Ulrik Buchholtz - homotopy type theory, synthetic homotopy theory, > proof assistants, constructive mathematics, and related topics. > > Graham Hutton - functional programming, haskell, category > theory, program verification, program calculation. > > Nicolai Kraus - homotopy type theory, higher category theory, > constructive mathematics, and related topics. > > Dan Marsden - category theory, logic, finite model theory, > diagrammatic reasoning, foundations of computer science. > > These positions are open to students of any nationality. > > Best wishes, > > The FP Lab > > +-----------------------------------------------------------+ > > 10 Fully-Funded PhD Studentships > > School of Computer Science > University of Nottingham, UK > > https://tinyurl.com/ten-phd-2022 > > Applications are invited from international and home students > for 10 fully-funded PhD studentships offered by the School of > Computer Science, starting on 1st October 2023. > > The topics for the studentships are open, but should relate > to the interests of one the School's research groups: > Computational Optimisation and Learning; Computer Vision; > Cyber Security; Functional Programming; Intelligent Modelling > and Analysis; Mixed Reality; Uncertainty in Data and Decision > Making; Visualisation and Computer Graphics; Cyber-Physical > Health and Assistive Robotics Technologies. > > The studentships are fully funded for 3.5 years and include a > stipend of £17,668 per year and tuition fees. Applicants are > normally expected to have a first-class class bachelors or > masters in Computer Science or another relevant area, and > must obtain the support of a potential supervisor in the > School prior to submitting their application. > > If you are interested in applying, please contact a potential > supervisor as soon as possible, and at least two weeks prior > to the closing date. If the supervisor wishes to support > your application, they will direct you to make an official > application through the MyNottingham system. > > Closing date for applications: Sunday 12th February 2023. > > +-----------------------------------------------------------+ > -- 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/c2b15c21-0f23-4698-8b59-a5359966067dn%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 5464 bytes --]

[-- Attachment #1: Type: text/plain, Size: 995 bytes --] Dear all, The Department of Mathematics of the University of Manchester is advertising a postdoctoral research fellowship to work on the EPSRC-funded project "Monoidal bicategories, linear logic and operads" with me (University of Manchester) and Marcelo Fiore (University of Cambridge). The deadline for applications is 23rd January 2023. For further information, please see the web page: https://www.jobs.manchester.ac.uk/displayjob.aspx?jobid=24337 With best regards, Nicola Dr Nicola Gambino Reader in Pure Mathematics Department of Mathematics, University of Manchester -- 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/5854D71A-747E-4238-9DE4-D8AFF90A68D6%40manchester.ac.uk. [-- Attachment #2: Type: text/html, Size: 2048 bytes --]

Hi all, I second Urs's congratulations on this great achievement! Just want to also add that I likewise miss the material on descent & flattening, for which your old notes provided an excellent reference. Of course, perhaps this leaves room for an "Advanced Topics in Homotopy Type Theory" followup ;-) Best, Jon On 3 Jan 2023, at 20:16, 'Urs Schreiber' via Homotopy Type Theory wrote: > Hi Egbert, > > nice to see your notes now available in a stably referenceable way! > They could fill quite a few gaps that the existing textbook literature > leaves open. > > On that note, it seems that a fair bit of material has been removed in > the arXiv version? > (Maybe to make room for large margins?) > > For referencing on the nLab I now find myself pointing mainly to the > version of your notes from 2018 (these here: > https://www.andrew.cmu.edu/user/erijke/hott/hott_intro.pdf), which > have discussion for instance of homotopy pullbacks/pushouts that seem > to have later been dropped, together with much material depending on > these notions (if I am seeing this correctly ?) > > I can imagine this is at least in large part the publisher's decision, > but just to say that if there is any wiggle room left, then I would > think it most worthwhile if these topics could make it into the final > book version. > > All my best wishes for the New Year, > Urs > > On Fri, Dec 23, 2022 at 1:54 PM Egbert Rijke <e.m.rijke@gmail.com> wrote: >> >> Dear homotopy type theorists, >> >> My textbook Introduction to Homotopy Type Theory is finished and available on the ArXiv: >> >> https://arxiv.org/abs/2212.11082 >> >> From the abstract: >> This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-Löf's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed. >> >> Over Christmas I will write a blog post in which I will go more into the content of the book. For now: Enjoy! >> >> Happy holidays to everyone! >> 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/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/B7706C57-2DE8-4AB6-A50B-89F7E6C1067D%40jonmsterling.com.

Hi Egbert, nice to see your notes now available in a stably referenceable way! They could fill quite a few gaps that the existing textbook literature leaves open. On that note, it seems that a fair bit of material has been removed in the arXiv version? (Maybe to make room for large margins?) For referencing on the nLab I now find myself pointing mainly to the version of your notes from 2018 (these here: https://www.andrew.cmu.edu/user/erijke/hott/hott_intro.pdf), which have discussion for instance of homotopy pullbacks/pushouts that seem to have later been dropped, together with much material depending on these notions (if I am seeing this correctly ?) I can imagine this is at least in large part the publisher's decision, but just to say that if there is any wiggle room left, then I would think it most worthwhile if these topics could make it into the final book version. All my best wishes for the New Year, Urs On Fri, Dec 23, 2022 at 1:54 PM Egbert Rijke <e.m.rijke@gmail.com> wrote: > > Dear homotopy type theorists, > > My textbook Introduction to Homotopy Type Theory is finished and available on the ArXiv: > > https://arxiv.org/abs/2212.11082 > > From the abstract: > This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-Löf's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed. > > Over Christmas I will write a blog post in which I will go more into the content of the book. For now: Enjoy! > > Happy holidays to everyone! > 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/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%40mail.gmail.com.

[-- Attachment #1.1: Type: text/plain, Size: 595 bytes --] Dear friends, Vladimir's paper "C-system of a module over a Jf-relative monad" has been published. You can view the article at https://authors.elsevier.com/a/1gL68_WcdlU5P for the next 49 days. Dan -- 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/96eb41bd-73af-4d5f-9fad-1032eae94590n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 951 bytes --]

Congratulations Egbert! Last fall I taught a topics course on homotopy type theory following this book to an audience of mostly mathematics students. The weekly problem sets were all in Agda, drawing inspiration from Egbert's excellent lists of exercises and extensive formalized library. Course materials are available here: https://github.com/emilyriehl/721 I mention all of this to say that I had an excellent experience teaching using Egbert's book. I had to skip several topics due to time constraints but I never found myself wishing the material were presented in a different order, which is quite remarkable. Kudos Egbert! Emily Professor of Mathematics (she/her) Johns Hopkins University emilyriehl.github.io On 12/23/22 04:54, Egbert Rijke wrote: > Dear homotopy type theorists, > > My textbook Introduction to Homotopy Type Theory is finished and available on the ArXiv: > > https://arxiv.org/abs/2212.11082 <https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Farxiv.org%2Fabs%2F2212.11082&data=05%7C01%7Ceriehl%40jhu.edu%7C0aa33ca5d7df4698161908dae4cbb6a2%7C9fa4f438b1e6473b803f86f8aedf0dec%7C0%7C0%7C638073860853350577%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=aVyJRuhCTZwnztt1H3l2aQMOvn2sfNUVD%2B0obnR%2FC0Y%3D&reserved=0> > > From the abstract: > This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-Löf's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type > theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed. > > Over Christmas I will write a blog post in which I will go more into the content of the book. For now: Enjoy! > > Happy holidays to everyone! > 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 <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com <https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2FHomotopyTypeTheory%2FCAGqv1ODuH3xtsFyFEekjwNH4SUN%252BdU8B1te2ZLX%252BNZsQLeChxg%2540mail.gmail.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=05%7C01%7Ceriehl%40jhu.edu%7C0aa33ca5d7df4698161908dae4cbb6a2%7C9fa4f438b1e6473b803f86f8aedf0dec%7C0%7C0%7C638073860853350577%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=yP5HBchPgpQNsZlwcNVENWmOKZeHdVBHkSneMgvzjCc%3D&reserved=0>. -- 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/7e2fee3c-30e8-a3ec-8941-68c63538240b%40jh.edu.

[-- Attachment #1: Type: text/plain, Size: 2655 bytes --] Thank you! Em sex., 23 de dez. de 2022 06:54, Egbert Rijke <e.m.rijke@gmail.com> escreveu: > Dear homotopy type theorists, > > My textbook Introduction to Homotopy Type Theory is finished and available > on the ArXiv: > > https://arxiv.org/abs/2212.11082 > > From the abstract: > This is an introductory textbook to univalent mathematics and homotopy > type theory, a mathematical foundation that takes advantage of the > structural nature of mathematical definitions and constructions. It is > common in mathematical practice to consider equivalent objects to be the > same, for example, to identify isomorphic groups. In set theory it is not > possible to make this common practice formal. For example, there are as > many distinct trivial groups in set theory as there are distinct singleton > sets. Type theory, on the other hand, takes a more structural approach to > the foundations of mathematics that accommodates the univalence axiom. > This, however, requires us to rethink what it means for two objects to be > equal. This textbook introduces the reader to Martin-Löf's dependent type > theory, to the central concepts of univalent mathematics, and shows the > reader how to do mathematics from a univalent point of view. Over 200 > exercises are included to train the reader in type theoretic reasoning. The > book is entirely self-contained, and in particular no prior familiarity > with type theory or homotopy theory is assumed. > > Over Christmas I will write a blog post in which I will go more into the > content of the book. For now: Enjoy! > > Happy holidays to everyone! > 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/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.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/CABUO1-ihPx2Zugxh9YbWA626Dc4uyQuaCtrxvHTGuLog%2Bza49g%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3459 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1900 bytes --] Dear homotopy type theorists, My textbook Introduction to Homotopy Type Theory is finished and available on the ArXiv: https://arxiv.org/abs/2212.11082 From the abstract: This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-Löf's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed. Over Christmas I will write a blog post in which I will go more into the content of the book. For now: Enjoy! Happy holidays to everyone! 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/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2311 bytes --]