From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 22643 invoked from network); 18 Nov 2022 02:36:02 -0000 Received: from mail-pj1-x103a.google.com (2607:f8b0:4864:20::103a) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 02:36:02 -0000 Received: by mail-pj1-x103a.google.com with SMTP id n4-20020a17090a2fc400b002132adb9485sf2205160pjm.0 for ; Thu, 17 Nov 2022 18:36:02 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668738960; cv=pass; d=google.com; s=arc-20160816; b=WPdeZekKfoNEbFBNuSalH2d54mLcnxC0QSDsMgzBuIpkD4Q9cu16JxPGqddkK9sl2E 7ce9+3Gdt30qOyhxpaTpYuXIXXsR8C1q4HBtbFO8xw9ubLNYFuEV59ivl3z4T+uWK36g GlxVdK79aOjs+36xqU8FnO4lz7ubtnAuZS4zgSZVOQWzIU0ZEFuyql0ozSW27Z+tOvJE rfTkzYTQycQyN9PIPXgvvfJLu7z9SCvY0Sm8tbCOfysyOSrOh3HK9a8dl0l37ZsRlF4C msMKboy7n9GQpkxegoRjqr208iRFmC0oTatJayHf0+6DM3gbZDPy8AJcEKOCR5/neYf4 l3lg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=wDSZx81fYvncsS6T617b68IkOfukO85G1eyDBZ/L0jo=; b=TvPSJkE0Xkqcv+eDNUTXP3I3ajJjE12co1yFjl/xr2kuhiZZ1QJQCsAs+54udLtO1z sidNbEHPP+IDlTe/y2QOqxKCaXkFh5V808yQ2r+da5Z2SRWtsRg/poCc4oN7KiK4PBg+ L6clG+iIviuJ26mip/Nkji48Z5Ksj1HO5BPqoRDuHX+zQM/d5AvQNBlcXwxiG/tOZc1f 6Aqa+QKsX4ZPU8XWW5Z6UCRuTwtWy0xW4P+xoAwbqLiyaMtHRYxFTipYGbsQuFuo1NHr fM9r4V9CBSoYJq4xrH9Lwe0rW12IZIuviUfvlfiSAh/tdVpOUlVrtVS8U4+ujywIAzU1 o17Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=AFTtQx7l; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112f as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=wDSZx81fYvncsS6T617b68IkOfukO85G1eyDBZ/L0jo=; b=b6/R5H9Hz4N39uK09+hCnBF43x7m0XJ33RKN0NrsdsH5kkgA/cI6y+AYnGYHKDUmDI KwmhnspnzDMRIzPiDPR/R6exNQd05CwUcBg8aKaTINZYxIN1cK6wr3nrO1SUc/nTqWku q6gvmexPVk9HqUa8rCzi+RVW5o6aakBC6YKTDGy68/S0TX+QdDDQ5CrtKzxu37G4pyoH 424idplL7XjZMEV0xu1WsYwlPSzb2yL2svamvTWBtCHkXECmbaysVITQEkE7vVoNgXo7 GlU/PeEZM4zEd4KFQuBklwfnRBZAi+m2Egzv1icgBfsVCSRrFOzrw+sD8jLrnjkzr0Ry ObQg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=wDSZx81fYvncsS6T617b68IkOfukO85G1eyDBZ/L0jo=; b=5abQukfZC2+P1PtQJ2C0xzoV68QCYWc+k/cyhGwztRR9AAQLoBueKjSmm6dUfxMD4a GwOr11RbZAAYzJlZEVRK3Wabz8tEoKKbAsfV4ELcI/zegIw7S+UostWB8UVuovbfwTph R6OaqqRi4vspvjxZG4wJQ7L0pePY84sOEmKUX93d8rw34IShQ7TPOC0yMyTkdF8TuHf5 XpjrObygGDQTZ80irnKX3rR50UmY1565PTszDYzDePa/XCokpkOAq/YaGcWxdQ9O3kil aia5MDow3Lt/T3suPongLUbBMixChvHCexp2EIi726tcnAkbYTmcovsPAwV4QwFDRw37 3sUg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pnb1djchQQgj4Yl5kwaRnYynzT80eS1BbH/QgTXEwEASEul7qAA lTfkyDlUnyxi5XA6QdfMkBw= X-Google-Smtp-Source: AA0mqf7rEa44jXfPR2XBl1IJGqqPC5VW/GhUz8ql4pqOYxAKMXxoFZcgA2ehko1XhWe0SFo8ANgZpg== X-Received: by 2002:a17:903:4111:b0:188:6300:640f with SMTP id r17-20020a170903411100b001886300640fmr5523704pld.124.1668738959079; Thu, 17 Nov 2022 18:35:59 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6a00:788:b0:56c:78e9:352e with SMTP id g8-20020a056a00078800b0056c78e9352els1871784pfu.7.-pod-prod-gmail; Thu, 17 Nov 2022 18:35:57 -0800 (PST) X-Received: by 2002:a63:4804:0:b0:464:8d6:8dc7 with SMTP id v4-20020a634804000000b0046408d68dc7mr4764568pga.594.1668738956922; Thu, 17 Nov 2022 18:35:56 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668738956; cv=none; d=google.com; s=arc-20160816; b=jtxinv5WczKJBda27SHlY/rB47qdEqvdXAAAr8oxqNLZwVcpUQA3VERr1DpXp3rzhO YneZgn6DhO+YqbV+Iobce4078mK0SR1Dd7ANo6T/HjYpveFvA0JYo5oj5kdopavl0K9+ WC9z8F5apQ6Z953TK/YvvUVbc6dpWc8Ajgqh+c34yRY3bDBVJESj7UwhiO8HaYNdWFsf NPnTA/6w34R5pWtR7CId0CISngKMXGRuvrpJ+zWvTE2ZC/QXstJRAXeevuLpc3Bwz/oX Knz685JdO8/jvgWBwaGMnzYrY4sCN/s8OWo62/trLdCMYBNaPVuyHXag+vXG3PGJkjfr KLMw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=O4vtXTSV7MZ4MlKe7H2nGAGGa8NH1wtV/DLePXT4ErU=; b=0ksk09f874mGrGgcpxdO6RywDxctrWiOd4T7/WKD8wpEBqBrKRS2mkj69OZBIhT4kP 2r1NEdPR2wbEqaheMS5qbvVHh74o3m2h61GgHMPNW8/jnY4rbzFNrlhjEDiwIufqXEjk qPvg+1+hVnYwQZQbOqoYWYvUrhdchKJBGSSYFYOtJLSipL9BL/oi/0jl+ya6HKmYR26J aVtdTCJI/gEmCcuhWqvUE2cLtjUVxmOlE/MmP24wJj0/XhPFATOcBAlYSHhpS16IX28U vcuz5U2OYxHlbsLg0eUiEMnmZ1EdoK5mC3yI4N5OZGV9q9p8oE2rAlLA2/zjJJbrD7Zw oWIg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=AFTtQx7l; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112f as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yw1-x112f.google.com (mail-yw1-x112f.google.com. [2607:f8b0:4864:20::112f]) by gmr-mx.google.com with ESMTPS id d4-20020a170903230400b00174ea015ef2si150938plh.5.2022.11.17.18.35.56 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 17 Nov 2022 18:35:56 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112f as permitted sender) client-ip=2607:f8b0:4864:20::112f; Received: by mail-yw1-x112f.google.com with SMTP id 00721157ae682-37063f855e5so37477347b3.3 for ; Thu, 17 Nov 2022 18:35:56 -0800 (PST) X-Received: by 2002:a05:690c:c01:b0:36d:1162:5dd with SMTP id cl1-20020a05690c0c0100b0036d116205ddmr4686638ywb.462.1668738956098; Thu, 17 Nov 2022 18:35:56 -0800 (PST) MIME-Version: 1.0 References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> In-Reply-To: <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> From: Michael Shulman Date: Thu, 17 Nov 2022 18:35:44 -0800 Message-ID: Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory To: Jon Sterling Cc: Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000b3e63d05edb59033" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=AFTtQx7l; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112f as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , --000000000000b3e63d05edb59033 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable As far as the mathematical study of type theories and their models goes, that may be true. But I believe that when talking about the way type theories are used in practice, either on paper or in a proof assistant, there is still a difference. Suppose I am teaching a calculus class, and I define f(x) =3D x^2 + 1 and I want to evaluate f(3). I don't write f(3) =3D (x^2+1)[3/x] =3D (x^2)[3/x] + 1[3/x] =3D 3^2 + 1 =3D 9 + 1 =3D 10. Instead, I jump right to f(3) =3D 3^2+1, because substitution is an operati= on that happens immediately in my head, not a computational step analogous to 3^2 =3D 9. Similarly, the user of a proof assistant never types or sees substitution as part of the syntax; it is an operation *on* syntax that happens behind the scenes. Yes, this is a property of a particular *presentation* of a free structure rather than a property of the structure itself, but that doesn't intrinsically make it unimportant. Groups and group presentations are both important. Maybe you want to say that "a type theory" refers to the free structure rather than its presentation, but choosing to use words in that way doesn't by itself make "presentations of type theories" (or whatever you call them) less important. Maybe you want to define an "admissible rule" to be a property that holds in the syntax but fails in some actual models; but that doesn't make "rules that hold in all models and can be made to hold in a particular presentation of the free model without being given explicitly as generating operations/equalities" (or whatever you call them) less important. I do agree that Andrej's formulation sounds backwards. In practice (in my experience) one doesn't write the rules down first and then try to figure out what kind of substitution is admissible. Instead one decides what the substitution rule should be, and *then* (hopefully) works out a way of presenting the syntax to make that substitution rule admissible. This is particularly tricky for modal type theories, where the categorically "obvious" rules do not admit substitution, and leads to the introduction of split contexts as used in the BFP paper. I have trouble imagining how I could have written that paper if I had been forced to write explicit substitutions everywhere. Thorsten and Jon, do you maintain that all the work that's gone into figuring out ways to present modal type theories with "admissible substitution" is meaningless? On Thu, Nov 17, 2022 at 5:37 AM Jon Sterling wrote: > Indeed, I echo Thorsten's comment =E2=80=94 to put it another way, even b= eing able > to tell whether these rules are derivable or only admissible is like > knowing what an angel's favorite TV show is (in other words, a form of > knowledge that cannot be applied toward anything by human beings). At lea= st > for structural type theory, there is nothing worth saying that cannot be > phrased in a way that does not depend on whether structural rules are > admissible or derivable. It may be that admissiblity of structural rules > starts to play a role in substructural type theory, however, but this is > not my area of expertise. > > It is revealing that nobody has proposed a notion of **model** of type > theory in which the admissible structural rules do not hold; this would b= e > the necessary form taken by any evidence for the thesis that it is > important for structural rules to not be derivable. Absent such a notion = of > model and evidence that it is at all compelling/useful, we would have to > conclude that worrying about admissibility vs. derivability of structural > rules in the official presentation of type theory is fundementally > misguided. > > On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory > wrote: > > That depends on what presentation of Type Theory you are using. Your > remarks apply to the extrinsic approach from the last millennium. More > recent presentation of Type Theory built in substitution and weakening an= d > use an intrinsic approach which avoids talking about preterms you don=E2= =80=99t > really care about. > > > > https://dl.acm.org/doi/10.1145/2837614.2837638 > > > > Cheers, > > Thorsten > > > > *From:* homotopytypetheory@googlegroups.com < > homotopytypetheory@googlegroups.com> on behalf of andrej.bauer@andrej.com > > *Date:* Tuesday, 15 November 2022 at 22:39 > *To:* Homotopy Type Theory > *Subject:* Re: [HoTT] Question about the formal rules of cohesive > homotopy type theory > > > Does this also include the structural rules of type theory such as the > substitution and weakening rules? > > I would just like to point out that substutition and weakening typically > are not part of the rules. They are shown to be admissible. In this spiri= t, > the question should have been: what is the precise version of substitutio= n > and weakening (which is a special case of substitution) that is admissibl= e > in cohesive type theory? > > 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/D66F4584-A005-4F69-8= E75-E976E0FF9957%40andrej.com > . > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > -- > 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/PAXPR06MB786979CA945= 19BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.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/41C2FBD7-7C3B-4D6D-A= 444-13FA43EDD1CF%40jonmsterling.com > > . > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CADYavpxcTpvy6%2BBS%2B-5yjOjVFkdXFHdmCX0U3Qre2J6t8Lfh_g%= 40mail.gmail.com. --000000000000b3e63d05edb59033 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
As far as the mathematical study of type theories and= their models goes, that may be true.=C2=A0 But I believe that when talking= about the way type theories are used in practice, either on paper or in a = proof assistant, there is still a difference.

Supp= ose I am teaching a calculus class, and I define f(x) =3D x^2 + 1 and I wan= t to evaluate f(3).=C2=A0 I don't write

f(3) = =3D (x^2+1)[3/x] =3D (x^2)[3/x] + 1[3/x] =3D 3^2 + 1 =3D 9=C2=A0+ 1 =3D 10.=

Instead, I jump right to f(3) =3D 3^2+1, because = substitution is an operation that happens immediately in my head, not a com= putational step analogous to 3^2 =3D 9.=C2=A0 Similarly, the user of a proo= f assistant never types or sees substitution as part of the syntax; it is a= n operation *on* syntax that happens behind the scenes.

<= /div>
Yes, this is a property of a particular *presentation* of a free = structure rather than a property of the structure itself, but that doesn= 9;t intrinsically make it unimportant.=C2=A0 Groups and group presentations= are both important.=C2=A0 Maybe you want to say that "a type theory&q= uot; refers to the free structure rather than its presentation, but choosin= g to use words in that way doesn't by itself make "presentations o= f type theories" (or whatever you call them) less important.=C2=A0 May= be you want to define an "admissible rule" to be a property that = holds in the syntax but fails in some actual models; but that doesn't m= ake "rules that hold in all models and can be made to hold in a partic= ular presentation of the free model without being given explicitly as gener= ating operations/equalities" (or whatever you call them) less importan= t.

I do agree that Andrej's formulation so= unds backwards.=C2=A0 In practice (in my experience) one doesn't write = the rules down first and then try to figure out what kind of substitution i= s admissible.=C2=A0 Instead one decides what the substitution rule should b= e, and *then* (hopefully) works out a way of presenting the syntax to make = that substitution rule admissible.=C2=A0 This is particularly tricky for mo= dal type theories, where the categorically "obvious" rules do not= admit substitution, and leads to the introduction of split contexts as use= d in the BFP paper.=C2=A0 I have trouble imagining how I could have written= that paper if I had been forced to write explicit substitutions everywhere= .=C2=A0 Thorsten and Jon, do you maintain that all the work that's gone= into figuring out ways to present modal type theories with "admissibl= e substitution" is meaningless?

On Thu, Nov 17, 2022 at 5:37 = AM Jon Sterling <jon@jonmsterlin= g.com> wrote:

Indeed, I echo Thorsten's comment =E2=80=94 to put it= another way, even being able to tell whether these rules are derivable or = only admissible is like knowing what an angel's favorite TV show is (in= other words, a form of knowledge that cannot be applied toward anything by= human beings). At least for structural type theory, there is nothing worth= saying that cannot be phrased in a way that does not depend on whether str= uctural rules are admissible or derivable. It may be that admissiblity of s= tructural rules starts to play a role in substructural type theory, however= , but this is not my area of expertise.

It is revealing that nobody has proposed a notion of **mode= l** of type theory in which the admissible structural rules do not hold; th= is would be the necessary form taken by any evidence for the thesis that it= is important for structural rules to not be derivable. Absent such a notio= n of model and evidence that it is at all compelling/useful, we would have = to conclude that worrying about admissibility vs. derivability of structura= l rules in the official presentation of type theory is fundementally misgui= ded.


On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' = via Homotopy Type Theory wrote:

That depends on what presentation of Type Theo= ry you are using. Your remarks apply to the extrinsic approach from the las= t millennium. More recent presentation of Type Theory built in substitution= and weakening and use an intrinsic approach which avoids talking about pre= terms you don=E2=80=99t really care about.

=C2=A0

https://dl.acm.org/doi/10.1145/2837614.28376= 38

=C2=A0

Cheers,

Thorsten

=C2=A0

From: <= span style=3D"font-size:12pt;color:black">homotopytypetheory@googlegroups.com= <homotopytypetheory@googlegroups.com> on behalf of andrej.bauer@andrej.com <andrej.= bauer@andrej.com>
Date: Tuesday, 15 November 2022 at 22:39
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com&g= t;
Subject: Re: [HoTT] Question about the formal rules of cohesive homo= topy type theory

>=C2=A0 Does this also= include the structural rules of type theory such as the substitution and w= eakening rules?

I would just like to point out that substutition and weakening typically ar= e not part of the rules. They are shown to be admissible. In this spirit, t= he question should have been: what is the precise version of substitution a= nd weakening (which is a special case of substitution) that is admissible i= n cohesive type theory?

With kind regards,

Andrej

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheor= y/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.
--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory= /PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlo= ok.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-= 13FA43EDD1CF%40jonmsterling.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https:/= /groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxcTpvy6%2BBS%2B-5yjOjV= FkdXFHdmCX0U3Qre2J6t8Lfh_g%40mail.gmail.com.
--000000000000b3e63d05edb59033--