From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:9a0b:: with SMTP id v11-v6mr2488118plp.51.1527875142780; Fri, 01 Jun 2018 10:45:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:418c:: with SMTP id g12-v6ls5344181pfd.7.gmail; Fri, 01 Jun 2018 10:45:41 -0700 (PDT) X-Received: by 2002:a63:6a88:: with SMTP id f130-v6mr2142462pgc.43.1527875141776; Fri, 01 Jun 2018 10:45:41 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527875141; cv=none; d=google.com; s=arc-20160816; b=wn2OGc5opXpp/QMSiVPDABW+788cYBczc7rKp5qX+KFxwhiH8U9YNaCLsnLWVjvlhQ 8dmoWwo6iUpS9Gyd7drWQUeeKdMsIK10E3tTN0/Dyzhwecy1dHucJ9K2wk6qYsZEvUA+ c7xtV4RQtegKgCg1i7z2aDyrbEnsXfEUV+W37PXKwcVopYftFY/owsq6KGmZC+Zu/3C5 tfHLC5hfESlR52EF+t/SnT2En6pCq9XMfZsTugdeX28a1yFgacU+rCtUbR5BBBjiK33v MhSJSWhES0TBTVT2VKfZmuB9WpUjUx9Y9KlQvg4hcTDf64ycyW8tEzYR13U4kLDBafZc sGTQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature:arc-authentication-results; bh=ivSZNeBvbwJaDxMHlZWdbng1UKndbxJ90+wWXaoHAMs=; b=GiXgau8GQhNI5lARFM7tmaAhCKDivnglxm3HJSo5JJywmdsZ8WbsSeMmoFaOZxTSvp 5H7JU2iblOv0R/obbQgsqZzEWFy7F1iYPPwKHLT1g2kFJ8Gviw4vr2qtBcGDDWrH/B+m jWA+l2rI0JpZKwfUC6fDKDCl3M2yfBvOC+ytaT55gaWvtYVSYtWqPI1jxSvN2+aDh893 fN4rlYy6e6m3w26kGGbXwvQpz70mN11QpiMkvdbvJ5tSJKcRuLXJfpj3i+h8W5xL8vno fLS80N7sf+djU6d5wpyzZBBIJmo/hPhpV181dknNEthGx+IhxEjsvoP6T1RqHy9r2ZwR MsJQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ve8aAY5c; spf=pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::22b as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x22b.google.com (mail-vk0-x22b.google.com. [2607:f8b0:400c:c05::22b]) by gmr-mx.google.com with ESMTPS id s13-v6si461824plp.1.2018.06.01.10.45.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 10:45:41 -0700 (PDT) Received-SPF: pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::22b as permitted sender) client-ip=2607:f8b0:400c:c05::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=ve8aAY5c; spf=pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::22b as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-vk0-x22b.google.com with SMTP id 200-v6so13948727vkc.0 for ; Fri, 01 Jun 2018 10:45:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to; bh=ivSZNeBvbwJaDxMHlZWdbng1UKndbxJ90+wWXaoHAMs=; b=ve8aAY5cGXQegMRiZgEJNvPB9dwrGC38i+0TJKYI34UDze8iRKyyYQ76fxm85IJAUm hixh3YhpQ/DTH5DLfKhY0BEqdDz2rl/bMcTDPWIird+MFeV4MgLu0DdoGSah7WnP0xj3 Kh23jfXelxkDYKA5pj0H1WgND148jOvuyABqMAFpimH+KEI3cA5ITYZn0PddApUK3Tt4 JmrW0S469CtTGsGhjRV7xvHLIT0mkoKgXbQLMxrsg8A9cpPUDw81/LBjt0rbnIV0BPxP Z1Z+xtWp/TnZ+TC8r1XSocMt8laNte28UyEEjkrkpTXc65uMEuZWfyIDUAOWpTfpRNgJ 21VA== X-Gm-Message-State: ALKqPwdz4IwNzYqzMgR8GjyACKFBWc3MCzK/6kQu4mNRGRUXSkdWzcWq ZDUxxgUbRcs7vp2I3pr796lCE3kNRaVQR80qEAc= X-Received: by 2002:a1f:aa58:: with SMTP id t85-v6mr7505030vke.118.1527875140501; Fri, 01 Jun 2018 10:45:40 -0700 (PDT) MIME-Version: 1.0 References: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk> <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk> <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com> <2b190a31-7985-4e6b-9f69-ed244ea64d7d@googlegroups.com> In-Reply-To: <2b190a31-7985-4e6b-9f69-ed244ea64d7d@googlegroups.com> From: Eric Finster Date: Fri, 1 Jun 2018 19:43:49 +0200 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000002d8a3056d9827be" --00000000000002d8a3056d9827be Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi All, I just had a chance to catch up and watch the video which prompted this disucussion last night. I'm a huge fan of the idea of trying to understand and make precise the notion of "higher category with families" and what that might say about the syntax of type theory. So my question is probably mostly directed at Thorsten, but I am curious to hear other people's responses as well. I guess my question is pretty simple: why should we insist, as Thorsten seems to, that the "intrinsic" syntax of type theory form a set? I can, I think, anticipate the first response: well, we want to have a type-checking algorithm. And, in light of the conversion rule, this typically means that we will have to reduce type expressions to a normal form and check if they are equal. Hence, if we don't have decidability of the syntax, we cannot have decidability of typechecking. Am I right that this is the principle motivation for having decidable syntax? But, then, this seems to be a statement about *extrinsic* syntax. If, as Thorsten advocates, we somehow manage to produce a highly structured, internal description of the syntax of type theory, then typechecking for this syntax is, by definition, unnecessary! After all, the whole point is that in such a setup, only the well-typed terms even make sense (i.e., are typeable in the meta-language). So from an internal perspective, I cannot think of any reason to insist on decidability. And consequently, insisting that an internal higher category with families be univalent does not seem in any way strange to me. But maybe there is some other objection that I'm not seeing? Eric On Fri, Jun 1, 2018 at 7:07 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < escardo...@gmail.com> wrote: > > > On Thursday, 31 May 2018 20:02:51 UTC+1, Alexander Kurz wrote: > >> >> > On 31 May 2018, at 12:05, Michael Shulman wrote: >> > >> > It sounds like Thorsten and are both starting to repeat ourselves, so >> > we should probably spare the patience of everyone else on the list >> > pretty soon. I'll just make my own hopefully-final point by saying >> > that if "properties of the typed algebraic syntax" can imply that the >> > untyped stuff we write on the page has a *unique* typed denotation, >> > independent of a particular typechecking algorithm, as mentioned in my >> > last email, then I'll (probably) be satisfied. >> >> I am interested in this question of translating the untyped stuff we >> write on the page into type theory. >> >> To give a concrete example of what I am thinking of as untyped, but >> nevertheless conceptual and structural mathematics, I would point at Tom >> Leinster=E2=80=99s elegant description of the solution to the problem of= Buffon=E2=80=99s >> needle, see the first paragraphs of the section =E2=80=9CWhat is categor= y theory?=E2=80=9D >> at >> https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_cat= ego.html >> >> I call this argument type free because I see no obvious or canonical way >> to make the types precise enough in order to implement the proof in, say= , >> Agda. Even if this can be done, it is still important that mathematician= s >> can discuss this argument first without having to make the types precise= . >> So there will always be mathematics outside of type theory. >> > > I don't understand why you call this argument untyped. Do you feel that = a > formalization in set theory, which is untyped, would be easier than a > formalization in type theory? How is untypedness helping with this > argument? > > Martin > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --00000000000002d8a3056d9827be Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi All,

I just had a chance = to catch up and watch the video which
pr= ompted this disucussion last night.=C2=A0 I'm a huge fan of the idea
of trying to understand and make precise t= he notion of "higher
category with = families" and what that might say about the syntax
of type theory.=C2=A0 So my question is probably mostly dir= ected at
Thorsten, but I am curious to h= ear other people's responses as
well= .

I guess my question is pretty simple: why should we insist,
as Thorsten seems to, that the "intrinsic" = syntax of type
theory form a set?
<= div style=3D"font-size:13px">
I can,= I think, anticipate the first response: well, we want to
have a type-checking algorithm.=C2=A0 And, in light of = the conversion
rule, this typically mean= s that we will have to reduce type
expre= ssions to a normal form and check if they are equal.=C2=A0 Hence,
if we don't have decidability of the syntax, = we cannot have
decidability of typecheck= ing.=C2=A0 Am I right that this is the principle=C2=A0
motivation for having decidable syntax?

But, then, this seem= s to be a statement about *extrinsic* syntax.=C2=A0 If,
as Thorsten advocates, we somehow manage to produce a highl= y
structured, internal description of th= e syntax of type theory,
then typechecki= ng for this syntax is, by definition, unnecessary!=C2=A0 After all,=C2=A0
the whole point is that in such a setup, = only the well-typed terms=C2=A0
even mak= e sense (i.e., are typeable in the meta-language).

So from an internal pers= pective, I cannot think of any reason to
insist on decidability.=C2=A0 And consequently, insisting that an
internal higher category with families be unival= ent does not seem
in any way strange to = me.

But maybe there is some other objection that I'm not seeing?
<= div style=3D"font-size:13px">
Eric
On Fri, Jun 1, 2018 at = 7:07 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 <escardo...@gmail.com> wrote:


On Thursday, 31 May 2018 20:02:51 U= TC+1, Alexander Kurz wrote:

> On 31 May 2018, at 12:05, Michael Shulman <= shu...@sandiego.edu> wrote:
>=20
> It sounds like Thorsten and are both starting to repeat ourselves,= so
> we should probably spare the patience of everyone else on the list
> pretty soon.=C2=A0 I'll just make my own hopefully-final point= by saying
> that if "properties of the typed algebraic syntax" can i= mply that the
> untyped stuff we write on the page has a *unique* typed denotation= ,
> independent of a particular typechecking algorithm, as mentioned i= n my
> last email, then I'll (probably) be satisfied. =C2=A0

I am interested in this question of translating the untyped stuff we wr= ite on the page into type theory.=20

To give a concrete example of what I am thinking of as untyped, but nev= ertheless conceptual and structural mathematics, I would point at Tom Leins= ter=E2=80=99s elegant description of the solution to the problem of Buffon= =E2=80=99s needle, see the first paragraphs of the section =E2=80=9CWhat is= category theory?=E2=80=9D at https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_highe= r_catego.html

I call this argument type free because I see no obvious or canonical wa= y to make the types precise enough in order to implement the proof in, say,= Agda. Even if this can be done, it is still important that mathematicians = can discuss this argument first without having to make the types precise. S= o there will always be mathematics outside of type theory.

=C2=A0I don'= ;t understand why you call this argument untyped. Do you feel that=20 a formalization in set theory, which is untyped, would be easier than a=20 formalization in type theory? How is untypedness helping with this argument= ?=C2=A0

Martin=C2=A0

--
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 HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--00000000000002d8a3056d9827be--