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 22736 invoked from network); 18 Nov 2022 16:26:00 -0000 Received: from mail-pj1-x103c.google.com (2607:f8b0:4864:20::103c) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 16:26:00 -0000 Received: by mail-pj1-x103c.google.com with SMTP id ch21-20020a17090af41500b0021879d85859sf2611179pjb.8 for ; Fri, 18 Nov 2022 08:25:59 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668788758; cv=pass; d=google.com; s=arc-20160816; b=yEOg1GCXvTh9mSYOQkS4peA0WHo4LCpr7XPAOW0iI8XtziRPM9Bkj5Ly/kg6mV6hhN t/rQiB6Sgmkf8uDigBoeBRSdOY4S6Z7Kqckhjf8mXuiN/+FcBBSW7TJjQ/ll5++JuKBe 3eJnBPqYg9WNzR8+e0/upDJV0ImJWX7NSLz/faJwIelzZHbIzPPW3uk/gpFaR493hbj7 CFx/w+1Zr0d0Pi1OaJ9Y0dRt4txqqKaRTn2v81Z2sGecA+9z56JJKSO+oZiWp09nsw9d I5XK0m2mB+6eDekMMvxl3XCPHVtIJcVb3BPM4/drJmZY2H7saGUUdZFBs4NfZj03yqUg jZBA== 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=EPebvrI8QTHJ0JQnxhnR3TLNUSIMUti/XInB/e/9iag=; b=KX4Nr1eYpVaGqxW8mgoH5RzwHAWhJAZ5u0UFoqTkegjfm1XJF5I8uAp87sfEV4QbHR PAb6pjJ5Bj9dVf6iqttbd16t8BKG16efJmZWhMLyb53LsP3ZP/5B3dA0OAoBEiQ+4LGn ubOF2dx4ytdkodyr89HJ8WwIY3dkTWJjLAddwY154w1Y+MZ2Zt3Pjp5IyqnUL9gtpdLI MDZAPnXP9edQ+GDBRwkag/LUewHAVR+wDwXzvvEcrLlGtXJTBNwXm+RD6MwwKyBbqk6/ MEzy/CdhXorEseEJpelw7OY6sbHQQCc2YWGV6Gwf2coC0MBaPzjt7776yo46L2LMvNZX jrwg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=c2GKuaBm; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 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=EPebvrI8QTHJ0JQnxhnR3TLNUSIMUti/XInB/e/9iag=; b=s1zjYsP7gj01JtuTSI5zlkq2Ia6Obqn+vuAj9EJ8bvwZ3sdOVYa3fjhfS5mPsxpsCQ 6COXD86qRU69x7tPODCuZugKMFGDa30uL/gRygW3kQ7Y8tO/vlw0CLWREfboOFwfJ7eO JDazxTdtjnWErYt96ZWtKilPO99auldq5kkxeBfj8Fn4ULrXUOK3VmxO7TkHoGlKfA1C zdl4+bXzLLuUM32TTNTwTNvgVtfi4yMWUJ1BxrcuqoEe2xZLk0W/lG74jCK3fRj0IRro HFiXivnFaYpCX8JBdCQifNedKn4zd3IL5mqL4avnF+XWBDGyJlBRppZs/r5oNed8SiFI O7pw== 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=EPebvrI8QTHJ0JQnxhnR3TLNUSIMUti/XInB/e/9iag=; b=mo4/rdd8y21XGoZV0iubgrXxeN0+zjQ5lClCk/EWW+rThjdY4YuaJLnv6mhu0YJwRX q2K2XFe7UO/BG2qTlrCHghkcekt5Ep4I5VeVHiSWl1dPgqNHSeGoAqNS+pbBLQoEAKWv kk3HG3dFXkZXpJUP85bR94xKSxQ1qQj5FqC2A8B7ryMJpxGDaGDrysjqdkRa1DDASkTY 2raPBPUZUJfhLhX8oE/o2Nla/fOqtls/zm2ZlYY9JpyBr9omm1A5Fb5NT1orveAQ49J6 jLfL1VTqUmhHSPId9WnaP2QbRG8T2zRvEyBttqnm4SM1N26BlBQBsGxPqVnkkWr6AfJa QO7w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pn+2k79tv+4OZTU74i4lz3ypA0Aeb34gE+Z1zOsy5+OQ/SfOjdh qzvLazxaFQmZD5X+G3vsYdE= X-Google-Smtp-Source: AA0mqf5nzU1Kpq++7m4/ZvFU9fGBCRaB9wrULYTNRqEYNXXhG6+rB+5wdF/QOPQkVi7bhVglNKD+Ag== X-Received: by 2002:a17:90a:fa46:b0:200:1df3:a7a9 with SMTP id dt6-20020a17090afa4600b002001df3a7a9mr14198838pjb.202.1668788758501; Fri, 18 Nov 2022 08:25:58 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:903:441:b0:187:3028:5d29 with SMTP id iw1-20020a170903044100b0018730285d29ls4295694plb.8.-pod-prod-gmail; Fri, 18 Nov 2022 08:25:57 -0800 (PST) X-Received: by 2002:a17:90b:128b:b0:20a:f469:7307 with SMTP id fw11-20020a17090b128b00b0020af4697307mr14632861pjb.213.1668788757013; Fri, 18 Nov 2022 08:25:57 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668788757; cv=none; d=google.com; s=arc-20160816; b=DG2iXlZ7oSKrrIgmWpFS1/aIW6REwy+NZOte49sgut28oLZj3p8XkzBJEuKNMWr5sS o54EfQXRYTS4PkdKM2rgbkqDvyrcudFA63WeF2PtWMnCQAvWHykl30w6VpkzDvePwVEZ t9Eb9B6GjGTmsdmMK0P8j6oAQJccZjOw0ZmuRLMNlMQR/NfNVcWUO1OBVWTo+/n3y+aY uErT/iJ6FhkQd+hYFCWeApl7rWjiJNYfNHJy9/5an5Fprm4gzr6Tuq13Pv+LLDM0IDkp euE6QAOgP1LyrzoNO7brE3GrBZp790TwrkEO0u+meZZQzTTIlrxJ/xDLGwnA+Az4zdbK oeCw== 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=JM05i2W42zudrOuIjLePdJ3NSRQCjdXM5PvPeTUEvnI=; b=e6uvgYdJihtgIPcHDMfOipfROJSze5y/6ryfpIDe/qjjTK2OkNnWsl0tBVW3esKuBH VtDzeAx3IjpSvfD0rnhB1CAH00h/RxD6MoweU7fsJwi11I1NKlgYAvyBfo7pF1Fbc2Rh mED3+xE+QvIp7hfB+qpqT78giMcdmYdHSVFmOgJSf4mPLYbIaU16T+pr/gLsv5BFgb6A ggBp1KhCtH/ujRd5x5gsnoeKk4HgJj6zoaXIIDKuJi4Gpdy9iqkONlP96D0rj+wZZgqF WbH24OkiVeneL40G8DK8fVUkUACVpjKJARPaugT8BfCmmanQo3cs0jYEdqTrLEzTTR8n 0mxA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=c2GKuaBm; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yb1-xb35.google.com (mail-yb1-xb35.google.com. [2607:f8b0:4864:20::b35]) by gmr-mx.google.com with ESMTPS id bu3-20020a632943000000b004772bae20ebsi114080pgb.5.2022.11.18.08.25.56 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 18 Nov 2022 08:25:56 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 as permitted sender) client-ip=2607:f8b0:4864:20::b35; Received: by mail-yb1-xb35.google.com with SMTP id 7so6187912ybp.13 for ; Fri, 18 Nov 2022 08:25:56 -0800 (PST) X-Received: by 2002:a25:c788:0:b0:6bc:7c5:df05 with SMTP id w130-20020a25c788000000b006bc07c5df05mr7576715ybe.138.1668788756267; Fri, 18 Nov 2022 08:25:56 -0800 (PST) MIME-Version: 1.0 References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> <9B3B568C-452A-4919-A149-CF7C1E91CDAE@jonmsterling.com> <21B50B02-4107-4854-8015-99EA4B14EBA5@jonmsterling.com> In-Reply-To: <21B50B02-4107-4854-8015-99EA4B14EBA5@jonmsterling.com> From: Michael Shulman Date: Fri, 18 Nov 2022 08:25: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="00000000000005db7805edc129c0" 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=c2GKuaBm; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 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: , --00000000000005db7805edc129c0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable In general, I feel like we are still talking past each other. Maybe the problem is that I still haven't found the words that will communicate my point to you. I was trying to say that it isn't the word "admissible" that matters, but there are real mathematical questions going on whatever words you use to talk about them. Last summer when I was explaining something about HOTT to a group that I think included you, I used the phrase "admissible" for a certain equality, and we got into a bit of this discussion. But I felt like we agreed in the end that what I meant was "a rule that doesn't have to get used explicitly by the conversion-checker", and that it was useful to distinguish such things whatever we call them. That's what I was trying to get at with "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". Similarly, I don't think the implicitness or explicitness of substitutions in the syntax is what's crucial. If you formulate substitutions implicitly, then the statement you want is that substitution can be defined as an "admissible" operation on the syntax. If you formulate substitutions explicitly, then the statement you want is that substitutions can be eliminated by a computation. Isn't this what you mean by "The equational theory of substitution in this situation (particularly, how to commute substitutions past the modal forms) is the hard part"? You don't just want an equational theory for substitution -- the equations in an equational theory are undirected -- but some kind of rewriting system that tells you how to push a substitution inside the modal forms. Whether the substitutions are part of the syntax or not isn't the point. On Fri, Nov 18, 2022 at 5:06 AM Jon Sterling wrote: > Maybe just to put a finer point on it, re: the calculus example (and then > I'll try to shut up, I have alreadyspoken too much): > > I subscribe to the viewpoint of the HoTT book regarding the practice of > informal mathematics (or at least, I subscribe to a version of the > viewpoint of the HoTT book which I think at least some of its authors hel= d, > including Steve Awodey with whom I have discussed this topic at length in > the past). Things like terms, variables, and substitution do not actually > arise in informal mathematics: instead, we work *directly* with things th= at > are functions of other things. Thus when doing informal mathematics, if w= e > say "term" we usually mean something that someone might more precisely > refer to as an "element". (But let me not open that can of worms!) > > In that sense, it would be completely incorrect to say that when doing > mathematics and we have a function `f(x) =3D x^2 + 1`, to evaluate f at 3= we > must apply a syntactical operation that recursively walks a syntax tree a= nd > replaces a placeholder with 3. The function `f` has the same ontological > status as a tree or as a friend or as a piece of stone: it is not a piece > of code that tracks a function, rather it is *actually* a function --- in > the same way that a stone is not a representation of an object, but an > actual object. Thus to evaluate `f(3)`, we use what we know about `f`: > namely that it is the function associated to the law that relates any > number to the successor of its square. > > So in ordinary math, "substitution" tends to be a fa=C3=A7on de parler fo= r an > operation that is not really syntactical at all but is instead > intrinsically constitutive of the informal notion of a "mapping", which > exists long before any logicians could attempt to intervene with their > syntactical gesticulations... (By the way: truly syntactic substitution > also arises *separately* in mathematics, by the way, when thinking about > free extensions of algebraic objects (like rings of the form R[x]). But > this is a very specialized usage, and if we are being precise we will > always distinguish between an element of R[x] and the function it encodes= .) > > It is true that it is possible to put aside this ontology, and think of > mathematical objects in terms of their encodings and then make sure to on= ly > speak of syntactical operations that track mathematical operations (e.g. > well-typed substitutions, but not ill-typed substitutions). But this is t= he > way of logicians, and it is not really pertinent to the practice of > everyday mathematics. Mathematics abstracts over these things, and we try > to work "directly" with the objects we are concerned with, regardless of > where we fall on the ancient debate of the "real-ness" of these objects. > > I fear we have veered off topic from the original question! But I think i= t > would be great if we could put this debate to rest once and for all --- I > am constantly amazed to be the syntactician in the room, but having > semanticists insist to me that the study of syntax needs raw terms and > variables and admissible substitution, etc. If it were needed, then I wou= ld > certainly have noticed it by now! The world of syntax is far richer than > can be described with mere trees or strings, and many of us who study > syntax for a living have moved on from that viewpoint. ;-) > > Best, > Jon > > > On 18 Nov 2022, at 7:47, Jon Sterling wrote: > > > On 17 Nov 2022, at 21:35, Michael Shulman wrote: > > > >> As far as the mathematical study of type theories and their models goe= s, > >> 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 > operation > >> that happens immediately in my head, not a computational step analogou= s > to > >> 3^2 =3D 9. Similarly, the user of a proof assistant never types or se= es > >> substitution as part of the syntax; it is an operation *on* syntax tha= t > >> happens behind the scenes. > > > > By the way, I find this calculus example to be supremely uncompelling > --- not because I am hung up on the fact that it pertains to a > presentation, but because mathematics is full of equations that we > basically agree not to mention at various times. > > > > It is also not particularly helpful to your point to bring up > implementation, where it is extremely common to eschew implicit > substitution for explicit substitutions --- or to use a mix of the two... > In neither case are the details of this presented to the user, however, > because the gender of an angel is not useful information to mere humans w= ho > use proof assistants. > > > > Best, > > Jon > --=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/CADYavpxMB%3D1kSPQM-OmSV_a9EauGmz7Gr-U3L%3DqfLCqsgzOnZQ%= 40mail.gmail.com. --00000000000005db7805edc129c0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
In general, I feel like we are still talking past eac= h other.=C2=A0 Maybe the problem is that I still haven't found the word= s that will communicate my point to you.=C2=A0 I was trying to say that it = isn't the word "admissible" that matters, but there are real = mathematical questions going on whatever words you use to talk about them.<= br>

Last summer when I was explaining something ab= out HOTT to a group that I think included you, I used the phrase "admi= ssible" for a certain equality, and we got into a bit of this discussi= on.=C2=A0 But I felt like we agreed in the end that what I meant was "= a rule that doesn't have to get used explicitly by the conversion-check= er", and that it was useful to distinguish such things whatever we cal= l them.=C2=A0 That's what I was trying to get at with "rules that = hold in all models and can be made to hold in a particular=20 presentation of the free model without being given explicitly as=20 generating operations/equalities".

Similarly,= I don't think the implicitness or explicitness of substitutions in the= syntax is what's crucial.=C2=A0 If you formulate substitutions implici= tly, then the statement you want is that substitution can be defined as an = "admissible" operation on the syntax.=C2=A0 If you formulate subs= titutions explicitly, then the statement you want is that substitutions can= be eliminated by a computation.=C2=A0 Isn't this what you mean by &quo= t;The equational theory of substitution in this situation (particularly,=20 how to commute substitutions past the modal forms) is the hard part"?= =C2=A0 You don't just want an equational theory for substitution -- the= equations in an equational theory are undirected -- but some kind of rewri= ting system that tells you how to push a substitution inside the modal form= s.=C2=A0 Whether the substitutions are part of the syntax or not isn't = the point.



On Fri, Nov 18, 2022 at 5= :06 AM Jon Sterling <jon@jonmste= rling.com> wrote:
Maybe just to put a finer point on it, re: the calculus example = (and then I'll try to shut up, I have alreadyspoken too much):

I subscribe to the viewpoint of the HoTT book regarding the practice of inf= ormal mathematics (or at least, I subscribe to a version of the viewpoint o= f the HoTT book which I think at least some of its authors held, including = Steve Awodey with whom I have discussed this topic at length in the past). = Things like terms, variables, and substitution do not actually arise in inf= ormal mathematics: instead, we work *directly* with things that are functio= ns of other things. Thus when doing informal mathematics, if we say "t= erm" we usually mean something that someone might more precisely refer= to as an "element". (But let me not open that can of worms!)

In that sense, it would be completely incorrect to say that when doing math= ematics and we have a function `f(x) =3D x^2 + 1`, to evaluate f at 3 we mu= st apply a syntactical operation that recursively walks a syntax tree and r= eplaces a placeholder with 3. The function `f` has the same ontological sta= tus as a tree or as a friend or as a piece of stone: it is not a piece of c= ode that tracks a function, rather it is *actually* a function --- in the s= ame way that a stone is not a representation of an object, but an actual ob= ject. Thus to evaluate `f(3)`, we use what we know about `f`: namely that i= t is the function associated to the law that relates any number to the succ= essor of its square.

So in ordinary math, "substitution" tends to be a fa=C3=A7on de p= arler for an operation that is not really syntactical at all but is instead= intrinsically constitutive of the informal notion of a "mapping"= , which exists long before any logicians could attempt to intervene with th= eir syntactical gesticulations... (By the way: truly syntactic substitution= also arises *separately* in mathematics, by the way, when thinking about f= ree extensions of algebraic objects (like rings of the form R[x]). But this= is a very specialized usage, and if we are being precise we will always di= stinguish between an element of R[x] and the function it encodes.)

It is true that it is possible to put aside this ontology, and think of mat= hematical objects in terms of their encodings and then make sure to only sp= eak of syntactical operations that track mathematical operations (e.g. well= -typed substitutions, but not ill-typed substitutions). But this is the way= of logicians, and it is not really pertinent to the practice of everyday m= athematics. Mathematics abstracts over these things, and we try to work &qu= ot;directly" with the objects we are concerned with, regardless of whe= re we fall on the ancient debate of the "real-ness" of these obje= cts.

I fear we have veered off topic from the original question! But I think it = would be great if we could put this debate to rest once and for all --- I a= m constantly amazed to be the syntactician in the room, but having semantic= ists insist to me that the study of syntax needs raw terms and variables an= d admissible substitution, etc. If it were needed, then I would certainly h= ave noticed it by now! The world of syntax is far richer than can be descri= bed with mere trees or strings, and many of us who study syntax for a livin= g have moved on from that viewpoint. ;-)

Best,
Jon


On 18 Nov 2022, at 7:47, Jon Sterling wrote:

> On 17 Nov 2022, at 21:35, Michael Shulman wrote:
>
>> 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 assis= tant,
>> 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).=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 + = 1 =3D 10.
>>
>> Instead, I jump right to f(3) =3D 3^2+1, because substitution is a= n operation
>> that happens immediately in my head, not a computational step anal= ogous to
>> 3^2 =3D 9.=C2=A0 Similarly, the user of a proof assistant never ty= pes or sees
>> substitution as part of the syntax; it is an operation *on* syntax= that
>> happens behind the scenes.
>
> By the way, I find this calculus example to be supremely uncompelling = --- not because I am hung up on the fact that it pertains to a presentation= , but because mathematics is full of equations that we basically agree not = to mention at various times.
>
> It is also not particularly helpful to your point to bring up implemen= tation, where it is extremely common to eschew implicit substitution for ex= plicit substitutions --- or to use a mix of the two... In neither case are = the details of this presented to the user, however, because the gender of a= n angel is not useful information to mere humans who use proof assistants.<= br> >
> Best,
> Jon

--
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/CADYavpxMB%3D1kSPQM-OmSV_a9Ea= uGmz7Gr-U3L%3DqfLCqsgzOnZQ%40mail.gmail.com.
--00000000000005db7805edc129c0--