From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a37:ad14:: with SMTP id f20-v6mr4091259qkm.35.1527886768281; Fri, 01 Jun 2018 13:59:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:7146:: with SMTP id h6-v6ls1323020qtp.3.gmail; Fri, 01 Jun 2018 13:59:27 -0700 (PDT) X-Received: by 2002:ac8:614d:: with SMTP id d13-v6mr6541130qtm.40.1527886767612; Fri, 01 Jun 2018 13:59:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527886767; cv=none; d=google.com; s=arc-20160816; b=rDQFZ2e/5Gri6z/7UEqxF3MKOwZSE4g/Rhb8D7dT46hDknU4dvg2kKS+JAf23+5wTB sp3B5Z9UnqJDWZxqFd1RHDkwGyRn13AkHICJEDTY0tg+MYL67voW4evhHPzYpUzolETm mE1Sn6HL3/cu4ZePitrX7RA/Cr0qJpfqIzZEiM0W4g7s8+bLwLOL8SxLQ4fmwWglj4qJ 3BMaYBgpParn99J0uddHcmoEWHe9EqgGHrTIIywsOnhhohLhDldi839M8zTcNDgXV8zG ZKtBX4QR+UILYlxDMBPoo/U3DQTPgQkl5QpWnrCi0OIFTGWOvbV7ir7+HdRVLa7Pi/UL GdDw== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=8/MlT44FfPNZkCelefYA5M6HrmK8E+CTTpSC2HzkaxM=; b=xIuAZ0phKHkkbS8rgAhbqIBiwzADDqDRYsjtk/FznOyvvvcTXHu0iqS5RvKm/KaN5n +V+P7ZCWHf6/eB6VFGqylldYAfwvMEmDvRLYGLA/BOAoIq5QTAUfzQL/KWB5NFbkLEQk vZgmKmIj0mZY7j79u/UALrZqR/eN/HmjRg6exoT2FMB096oTqEf78QhCMW4yOTa9RgVn 8OEuCJirCT065mqBnXYLah2tXI3zj6kRBmFj9PWBlLbDSDmcwaVrTTo6iQ2qmR7M882U HBRbJDPZ/CnKtFiZcNukVG1FH77dMSVDojn+6be1ctkKbuHtLbZfnc4WLncTXTZjd1pn UhRQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=G4bllggU; spf=pass (google.com: domain of putta...@gmail.com designates 2607:f8b0:400d:c09::230 as permitted sender) smtp.mailfrom=putta...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qk0-x230.google.com (mail-qk0-x230.google.com. [2607:f8b0:400d:c09::230]) by gmr-mx.google.com with ESMTPS id o3-v6si2540664qtd.5.2018.06.01.13.59.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 13:59:27 -0700 (PDT) Received-SPF: pass (google.com: domain of putta...@gmail.com designates 2607:f8b0:400d:c09::230 as permitted sender) client-ip=2607:f8b0:400d:c09::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=G4bllggU; spf=pass (google.com: domain of putta...@gmail.com designates 2607:f8b0:400d:c09::230 as permitted sender) smtp.mailfrom=putta...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qk0-x230.google.com with SMTP id j12-v6so17566603qkk.4 for ; Fri, 01 Jun 2018 13:59:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=8/MlT44FfPNZkCelefYA5M6HrmK8E+CTTpSC2HzkaxM=; b=G4bllggUtP6NESCv1e4UnNeZJ2lhKwlT0sFeNSXtqAiy2XhVA1Dt/3iYVg16WGttJY RzBdUTOa5TSZSDMcyAwv0tFxDKQ3kzjFdDPd26I24932EUETHtSa3lClasJAjPCtwYeL ehwftXcA0zgpIunlciCQxfI3kczYEl3ep5GfQBNL6Nl5wl0RYok7+tUZOFBPiGZQmL1e Wt7bEwHRizMYXSL8nPgthnGCxHjYUbfm+RiiMwmMk1FIaFZnLXdd0cW39OCIlO5vp+HE iXewgUpCf/99PdnRTGfsgsezkO9jd7JMzz7WISPr39C7/rfuuORB6t6+nRZIUXxne2Ql dUvg== X-Gm-Message-State: APt69E0QkhFYgu8uPCjKFgn8hiV+UkXL/EhjmMNGNzNuIJqb057yoAok WCqQRvUHY5RsiKGaqzisg+z989IcUddqhvQ+J2sLHQ== X-Received: by 2002:a37:16e0:: with SMTP id 93-v6mr12194830qkw.148.1527886767379; Fri, 01 Jun 2018 13:59:27 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:ac8:2d37:0:0:0:0:0 with HTTP; Fri, 1 Jun 2018 13:59:26 -0700 (PDT) In-Reply-To: <1efa5fe9-cdc9-4714-ae2a-953ac59cfdf4@googlegroups.com> 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> <1efa5fe9-cdc9-4714-ae2a-953ac59cfdf4@googlegroups.com> From: =?UTF-8?B?QW5kcsOhcyBLb3bDoWNz?= Date: Fri, 1 Jun 2018 22:59:26 +0200 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000006dbbf056d9adcba" --00000000000006dbbf056d9adcba Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > > I like this question. If the syntax is supposed to be the initial model, > then it can't be a set. Why? The syntax being a set doesn't imply that models also need to be sets. As I understand, the goal of higher models for TT is to get rid of set-truncation but still have a syntax which is a set. 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! > Type checking must be performed in any case, at some level. If we use intrinsic embedded syntaxes, then the implementation of the metalanguage (in a meta-metalanguage) does the type checking. Hence, if we intend to formalize a syntax of type theory which is intended as a metatheoretical setting for mathematics, then I think decidability is quite important. 2018-06-01 21:55 GMT+02:00 Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 : > > > On Friday, 1 June 2018 18:45:42 UTC+1, Eric Finster wrote: >> >> 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 like this question. If the syntax is supposed to be the initial model, > then it can't be a set. > > 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. > --00000000000006dbbf056d9adcba Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I like this question. If the syntax i= s supposed to be the initial model, then it can't be a set.

Why? The syntax being a set doesn't imply= that models also need to be sets. As I understand, the goal of higher mode= ls for TT is to get rid of set-truncation but still have a syntax which is = a set.

But, then, this seems to be a statement about *extrinsic= * syntax.=C2=A0 If,
as Thorsten advocates, we somehow manage to produce = a highly
structured, internal description of the syntax of type theory,<= /div>
then typechecking for this syntax is, by definition, unnecessary!
<= /blockquote>

Type checking must be performed in any ca= se, at some level. If we use intrinsic embedded syntaxes, then the implemen= tation of the metalanguage (in a meta-metalanguage) does the type checking.= Hence, if we intend to formalize a syntax of type theory which is intended= as a metatheoretical setting for mathematics, then I think decidability is= quite important.


2018-06-01 21:55 GMT+02:00 Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 <escardo...@gmail.com>:


On Friday, 1 June 2018 18= :45:42 UTC+1, Eric Finster wrote:
I guess my question is pret= ty simple: why should we insist,
as Thor= sten seems to, that the "intrinsic" syntax of type
theory form a set?

I like this question. If the syntax is supposed to be the i= nitial model, then it can't be a set.

=C2=A0Ma= rtin

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

--00000000000006dbbf056d9adcba--