[-- Attachment #1.1: Type: text/plain, Size: 765 bytes --] Dear all, The Institute for Logic, Language and Computation (part of the University of Amsterdam) will be hiring an assistant professor in Theoretical Computer Science. The official add is available here: https://ivi.uva.nl/shared/uva/en/vacancies/2020/10/20-647-assistant-professor-theoretical-computer-science.html?origin=dXb5vvhxSni9fe05dSz4fA Best wishes, Benno -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/fd89dad4-f27f-4d87-93a0-a85d4713ea92n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1153 bytes --]

It is my pleasure to announce the next talk in the Every proof assistant on-line seminar series. We are starting the Fall season with Anders Mörtberg who will talk about Cubical Agda. With kind regards, Andrej CUBICAL AGDA: A DEPENDENTLY TYPED PROGRAMMING LANGUAGE WITH UNIVALENCE AND HIGHER INDUCTIVE TYPES Anders Mörtberg Stockholm University Thursday, September 17, 2020 15:00 to 16:00 (Central European Summer Time, UTC+2) Location: online at Zoom ID 989 0478 8985, https://zoom.us/j/98904788985 Proof assistant: Cubical Agda, https://github.com/agda/cubical Abstract: The dependently typed programming language Agda has recently been extended with a cubical mode which provides extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically to proof assistants based on dependent type theory which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. In the talk I will discuss how Agda was extended to a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. I will also show a variety of examples of how to use Cubical Agda in practice to reason about mathematics and computer science. -- 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/CAB0nkh1qFFEtkb90aj7RBy%2Bf407nJRwjLdWcu8BvMC1N6Z3c7A%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 2256 bytes --] The Institute of Philosophy of the Czech Academy of Sciences welcomes applications for two full-time postdoc positions. The two postdocs will work within a project led by Ansten Klev on type theory and the philosophy of mathematics. The main aim of the project is to develop a philosophy of mathematics for Martin-Löf type theory. The postdocs will pursue research programmes of their own that in some way contribute to this overall aim. Both positions last for 30 months and will start in January 2021. In the first part of this 5-year project emphasis will be placed on developing an inferentialist meaning theory for mathematical language. We are especially looking for researchers who fit at least one of these two descriptions: 1. You are well acquainted with inferentialism in at least one of its incarnations (proof-theoretic semantics, the Brandom tradition), and you are interested in extending the programme to the language of mathematics. If you are not already familiar with Martin-Löf type theory, you are willing to learn the basics of the system after arriving in Prague. 2. You are well acquainted with the technical aspects of Martin-Löf type theory and are familiar with Martin-Löf's meaning explanations. You might even know some homotopy type theory and have thought about how the meaning explanations fare within that or other extensions of Martin-Löf type theory. A more detailed description of the project is available upon request from Ansten Klev, who will also attend to any questions applicants may have: klev@flu.cas.cz. The deadline for applying is October 15. Applications should be sent to Olga Bažantová: bazantova@flu.cas.cz. The application should consist of a CV and a brief (1-2 pages) description of the research the applicant plans to carry out while in Prague. -- 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/CAJHZuqZGaZcfb7d8xFpR9Fju_DoRZCxY9EVHNHGUGcve90V_sA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2932 bytes --]

Dear all, The Homotopy Type Theory Electronic Seminar Talks (HoTTEST) are returning in Fall 2020. The speakers are: September 10: Guillaume Brunerie and Peter LeFanu Lumsdaine September 24: Jakob von Raumer October 8: Yuki Maehara October 22: Ambrus Kaposi November 5: Nima Rasekh November 19: Pierre Cagne December 3: Jamie Vicary The seminar will meet on alternating Thursdays at 11:30 Eastern. The seminar is open to all, but some prior familiarity with HoTT will be assumed. For updates and instructions how to attend, please see https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html We know you have a choice when it comes to electronic seminars and we thank you for choosing HoTTEST. Best wishes, Dan Christensen Chris Kapulkin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3N6wK8Ywx8gAW6x%3DuvBtvD_JXHw7REtScTTY2DRH3%2BnUw%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 5646 bytes --] Dear all, the panel discussion below is on the future of conferences and the publication model of computer science, especially compared to maths and other disciplines. This seems very relevant for us, i.e. the HoTT community. Nicolai -------- Forwarded Message -------- Subject: Panel Debate, Wednesday 2 September @ 3pm UTC: "Evolution or Revolution? The Future of Conferences in Theoretical Computer Science" Date: Mon, 17 Aug 2020 22:54:13 +0100 From: Jamie Vicary <jamie.vicary@cl.cam.ac.uk> [TLDR: Panel Debate on the Future of Conferences in TCS -- panel Fong, Kesner, Pierce, Vardi -- join at 3pm UTC on Weds 2 Sep -- zoom.us/j/177472153 -- reply now from academic email address to propose a question -- please circulate this message widely] Dear all, The entire community is invited to participate in a debate on the future of the conference system in theoretical computer science. Organized as a special event as part of the Online Worldwide Seminar on Logic and Semantics (OWLS), this will provide a rare community-wide opportunity for us to consider the strengths and weaknesses of our current system, and consider if we can do better. The scope of the debate is all aspects of our publishing and community traditions, characterised by prestige earned mostly through publication in competitive conferences, and frequent local and international travel. Possible topics for discussion include the need to publish in conferences for career progression, which usually involves burning carbon; wasted author and reviewer effort when good papers are rejected from highly competitive conferences; the extent of our responsibility as a community to respond to climate change; alternative publishing models, like the journal-focussed system used in mathematics; high costs of conference travel and registration; virtual conference advantages, disadvantages and best practice; improving equality, diversity and access; consequences and response to COVID-19; and the role of professional bodies. These topics have many close relationships, and need to be discussed together to gain a full understanding of the issues involved, and how we can move forward. OUR PANEL To discuss these issues, we have an excellent panel with a wide range of relevant experience: - Dr Brendan Fong, MIT (brendanfong.com) is a postdoctoral researcher with considerable experience organizing virtual conferences and seminars (act2020.mit.edu), and an Executive Editor of the new open-access journal Compositionality. - Professor Delia Kesner, University of Paris (irif.fr/~kesner) has served on the Steering Committee of six conferences and workshops, and is currently the SC Chair of FSCD, the most recent iteration of which was organized at short notice as a virtual event (fscd2020.org). - Professor Benjamin Pierce, University of Pennsylvania (cis.upenn.edu/~bcpierce) has served as PC chair of a range of events including POPL and ICFP, and has written powerfully on the need for the computer science community to adapt to the reality of climate change. - Professor Moshe Vardi, Rice University (cs.rice.edu/~vardi) is Senior Editor of the journal Communications of the ACM, and founded the Federated Logic Conference (FLOC). He has long been a vocal commentator on structural problems with computer science publishing. PROPOSE A QUESTION Questions will be asked by members of the community. That means you! Please reply to this email to propose your question, which could raise any issue in scope. **Why not do it right now?** Make sure to use an academic email address. We'll let you know if your question is accepted, and you'll then have the opportunity to ask it during the debate, and to respond to the panel's comments. WHEN AND WHERE The debate will take place on Wednesday 2 September at 3pm UTC, which corresponds to the following times in a range of cities around the world: 8am San Francisco / 10am Houston / 11am Philadelphia / 4pm London / 5pm Paris / 9pm Mumbai / 11pm Beijing / midnight Tokyo / 1am Sydney The event will take place on Zoom at the following address, with no password or registration required: - zoom.us/j/177472153 The debate will be followed by an opportunity to discuss informally with other members of the community in small groups. WEBPAGE This event is organized as part of the OWLS seminar series. For more information, a calendar you can embed into your own, and to sign up for reminder emails, visit the webpage: - https://www.cs.bham.ac.uk/~vicaryjo/owls/ READING Members of the community may enjoy the following articles, related to the topic of the debate. - Lance Fortnow (2009), "Time for Computer Science to Grow Up", https://cacm.acm.org/magazines/2009/8/34492-viewpoint-time-for-computer-science-to-grow-up - Benjamin Pierce, Michael Hicks, Crista Lopes and Jens Palsberg (2020), "Conferences in an Era of Expensive Carbon", https://cacm.acm.org/magazines/2020/3/243024-conferences-in-an-era-of-expensive-carbon - Moshe Vardi (2020), "Publish and Perish", https://cacm.acm.org/magazines/2020/1/241717-publish-and-perish We hope you will join us for the debate. Please forward this message to members of your research group, and others who may be interested to participate. Best wishes, Jamie -- 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/bc16b3e1-08e0-3152-65bd-595bf42faead%40gmail.com. [-- Attachment #2: Type: text/html, Size: 8736 bytes --]

[-- Attachment #1: Type: text/plain, Size: 6884 bytes --] Hi Alex, Thanks, that is all really cool stuff! It's neat that you can do a similar thing for equality, I hadn't thought that was possible, though it seems obvious to me when spelled out. I actually started off learning Coq trying to formalize an undergraduate group theory class, and got sidetracked by various ways of making associativity less annoying. I was exploring reflexive decision procedures, but it's wonderful to see other approaches to this problem. With regards to your proposed definition of A involutiveBiEquiv B, I don't believe that it is a true definition of equivalence, since biEquiv is not a mere proposition. The definitions with strictly involutive inversion I have seen generally introduce a type in the middle, so A involutiveEquiv B = (C : Type) x (C equiv A) x (C equiv B), which under univalence is equivalent to equiv but can only strictly satisfy one of the two unit equations for composition. Sincerely, - Jasper Hugunin On Mon, Aug 17, 2020 at 6:48 AM alexr...@gmail.com <alexrice73@gmail.com> wrote: > Hi Jasper, > > I have also thought about these sort of structures a bit, and in fact this > sort of "trick" of decomposing something of passing in an equality also > works in a variety of situations where composition involves transitivity of > equality. For example, you might be interested in Martin Escardo's > version of this for equality > <https://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html> which contains a fair > bit of discussion on the topic. I have also done some work on this sort of > idea related to groups which can be found here > <https://alexarice.github.io/posts/sgtuf/Strict-Group-Theory-UF.html> and > submitted a pull request to agda standard library with a similar idea to > this for quasi-inverses <https://github.com/agda/agda-stdlib/pull/1156>. > > With respect to the questions at the end, I'm afraid I am not aware of any > definition for which inverses are strict and I expect that (2) (at least in > it's full generality) is not possible as this would imply that > \infty-groupoids are equivalent to strict \infty-groupoids. For involution > you could perhaps do a similar trick that is done in category theory > libraries like agda-categories where you store the data for both > directions. More precisely, if we let your definition be called biEquiv > then you could let > > A involutiveBiEquiv B = A biEquiv B x B biEquiv A > > and then let inverting be given by swapping the order of the product. I > believe this should maintain the nice compositional properties of biEquiv > and adds involutive inverses for "free". > > Hope some of this was useful/interesting. > Alex > > On Sunday, 16 August 2020 at 20:08:47 UTC+1 jas...@cs.washington.edu > wrote: > >> I was thinking about various definitions of equivalence, and the various >> equations we could ask them to satisfy up to definitional equality. (They >> are of course all the same when looking at propositional equality.) >> >> Looking at composition, all the definitions of equivalence I have seen >> before satisfy at most one of the two equations id o p = p or p o id = p >> (for p : A equiv B and _o_ composition). >> >> By adapting the definition by bi-invertible maps, we can get a definition >> of equivalence where both the above equations hold, and additionally we get >> definitional associativity (p o q) o r = p o (q o r). >> >> ----- >> >> Recall the bi-invertible map definition of equivalence is >> A equiv B = >> (f : A -> B) x >> (gl : B -> A) x >> (gr : B -> A) x >> (linv : forall a, gl(f(a)) = a) x >> (rinv : forall b, f(gr(b)) = b) >> Then the identity is (id, id, id, refl, refl). >> >> When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2, >> rinv2), >> we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and >> rinv require path induction (essentially to compose instantiations of linv1 >> and linv2). Since path composition in an arbitrary type only satisfies one >> of the two unit equations definitionally, I don't believe it is possible to >> satisfy both id o p and p o id for this definition. >> >> However, we can modify the definitions of linv and rinv inspired by the >> symmetric coinductive definition of equivalence (that A equiv B = (f : A -> >> B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)). >> >> So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, >> a = gr b -> f a = b. >> >> (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are >> contractible, so this definition is equivalent to the bi-invertible map >> definition, and thus a real definition of equivalence.) >> >> Then for the identity, we take linv = rinv = id. >> Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o >> rinv2, and exploit the fact that the identity function is definitionally a >> two-sided unit for function composition. >> >> Q.E.D. >> >> ----- >> >> Has anyone seen this definition or other definitions with this property >> used before? >> >> This definition does not behave particularly nicely with respect to >> inversion. I know a few definitions with definitional involutive inversion, >> and most definitions seem to satisfy id^-1 = id, but I don't think I know >> any definitions where p^-1 o p = id or p o p^-1 = id. >> >> There is such a wide variety of possible choices with respect to the >> definition of equivalence, I am interested in what additional properties we >> can ask of it to narrow down the scope of a "good" definition, and what >> unavoidable trade offs exist. >> Some good properties I am thinking about are: >> 1) Decomposition into (f : A -> B) x isEquiv f >> 2) Definitional groupoid equations. >> Currently (1) seems to be incompatible with involutive inversion, but as >> shown here we can have both (1) and definitional equations for everything >> except inversion. Can we be more greedy? >> >> Sincerely, >> - Jasper Hugunin >> > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8Ev95e9eop-DSPgDD6e_tCbQJyxfG-qUt15HYgpZ-hgA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 8604 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 5184 bytes --] Hi Jasper, I have also thought about these sort of structures a bit, and in fact this sort of "trick" of decomposing something of passing in an equality also works in a variety of situations where composition involves transitivity of equality. For example, you might be interested in Martin Escardo's version of this for equality <https://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html> which contains a fair bit of discussion on the topic. I have also done some work on this sort of idea related to groups which can be found here <https://alexarice.github.io/posts/sgtuf/Strict-Group-Theory-UF.html> and submitted a pull request to agda standard library with a similar idea to this for quasi-inverses <https://github.com/agda/agda-stdlib/pull/1156>. With respect to the questions at the end, I'm afraid I am not aware of any definition for which inverses are strict and I expect that (2) (at least in it's full generality) is not possible as this would imply that \infty-groupoids are equivalent to strict \infty-groupoids. For involution you could perhaps do a similar trick that is done in category theory libraries like agda-categories where you store the data for both directions. More precisely, if we let your definition be called biEquiv then you could let A involutiveBiEquiv B = A biEquiv B x B biEquiv A and then let inverting be given by swapping the order of the product. I believe this should maintain the nice compositional properties of biEquiv and adds involutive inverses for "free". Hope some of this was useful/interesting. Alex On Sunday, 16 August 2020 at 20:08:47 UTC+1 jas...@cs.washington.edu wrote: > I was thinking about various definitions of equivalence, and the various > equations we could ask them to satisfy up to definitional equality. (They > are of course all the same when looking at propositional equality.) > > Looking at composition, all the definitions of equivalence I have seen > before satisfy at most one of the two equations id o p = p or p o id = p > (for p : A equiv B and _o_ composition). > > By adapting the definition by bi-invertible maps, we can get a definition > of equivalence where both the above equations hold, and additionally we get > definitional associativity (p o q) o r = p o (q o r). > > ----- > > Recall the bi-invertible map definition of equivalence is > A equiv B = > (f : A -> B) x > (gl : B -> A) x > (gr : B -> A) x > (linv : forall a, gl(f(a)) = a) x > (rinv : forall b, f(gr(b)) = b) > Then the identity is (id, id, id, refl, refl). > > When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2, > rinv2), > we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and > rinv require path induction (essentially to compose instantiations of linv1 > and linv2). Since path composition in an arbitrary type only satisfies one > of the two unit equations definitionally, I don't believe it is possible to > satisfy both id o p and p o id for this definition. > > However, we can modify the definitions of linv and rinv inspired by the > symmetric coinductive definition of equivalence (that A equiv B = (f : A -> > B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)). > > So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, > a = gr b -> f a = b. > > (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are > contractible, so this definition is equivalent to the bi-invertible map > definition, and thus a real definition of equivalence.) > > Then for the identity, we take linv = rinv = id. > Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o > rinv2, and exploit the fact that the identity function is definitionally a > two-sided unit for function composition. > > Q.E.D. > > ----- > > Has anyone seen this definition or other definitions with this property > used before? > > This definition does not behave particularly nicely with respect to > inversion. I know a few definitions with definitional involutive inversion, > and most definitions seem to satisfy id^-1 = id, but I don't think I know > any definitions where p^-1 o p = id or p o p^-1 = id. > > There is such a wide variety of possible choices with respect to the > definition of equivalence, I am interested in what additional properties we > can ask of it to narrow down the scope of a "good" definition, and what > unavoidable trade offs exist. > Some good properties I am thinking about are: > 1) Decomposition into (f : A -> B) x isEquiv f > 2) Definitional groupoid equations. > Currently (1) seems to be incompatible with involutive inversion, but as > shown here we can have both (1) and definitional equations for everything > except inversion. Can we be more greedy? > > Sincerely, > - Jasper Hugunin > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 6273 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3394 bytes --] I was thinking about various definitions of equivalence, and the various equations we could ask them to satisfy up to definitional equality. (They are of course all the same when looking at propositional equality.) Looking at composition, all the definitions of equivalence I have seen before satisfy at most one of the two equations id o p = p or p o id = p (for p : A equiv B and _o_ composition). By adapting the definition by bi-invertible maps, we can get a definition of equivalence where both the above equations hold, and additionally we get definitional associativity (p o q) o r = p o (q o r). ----- Recall the bi-invertible map definition of equivalence is A equiv B = (f : A -> B) x (gl : B -> A) x (gr : B -> A) x (linv : forall a, gl(f(a)) = a) x (rinv : forall b, f(gr(b)) = b) Then the identity is (id, id, id, refl, refl). When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2, rinv2), we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and rinv require path induction (essentially to compose instantiations of linv1 and linv2). Since path composition in an arbitrary type only satisfies one of the two unit equations definitionally, I don't believe it is possible to satisfy both id o p and p o id for this definition. However, we can modify the definitions of linv and rinv inspired by the symmetric coinductive definition of equivalence (that A equiv B = (f : A -> B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)). So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, a = gr b -> f a = b. (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are contractible, so this definition is equivalent to the bi-invertible map definition, and thus a real definition of equivalence.) Then for the identity, we take linv = rinv = id. Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o rinv2, and exploit the fact that the identity function is definitionally a two-sided unit for function composition. Q.E.D. ----- Has anyone seen this definition or other definitions with this property used before? This definition does not behave particularly nicely with respect to inversion. I know a few definitions with definitional involutive inversion, and most definitions seem to satisfy id^-1 = id, but I don't think I know any definitions where p^-1 o p = id or p o p^-1 = id. There is such a wide variety of possible choices with respect to the definition of equivalence, I am interested in what additional properties we can ask of it to narrow down the scope of a "good" definition, and what unavoidable trade offs exist. Some good properties I am thinking about are: 1) Decomposition into (f : A -> B) x isEquiv f 2) Definitional groupoid equations. Currently (1) seems to be incompatible with involutive inversion, but as shown here we can have both (1) and definitional equations for everything except inversion. Can we be more greedy? Sincerely, - Jasper Hugunin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9Qo5jTP7bMsHkQGgBp9y46icJ1m1bB0qiSiHUS%2BJxQGw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4273 bytes --]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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