From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a9f:25b6:: with SMTP id 51-v6mr5389912uaf.47.1527889938904; Fri, 01 Jun 2018 14:52:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:ab4f:: with SMTP id u76-v6ls11859161vke.2.gmail; Fri, 01 Jun 2018 14:52:18 -0700 (PDT) X-Received: by 2002:a1f:2fd3:: with SMTP id v202-v6mr5304052vkv.53.1527889938141; Fri, 01 Jun 2018 14:52:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527889938; cv=none; d=google.com; s=arc-20160816; b=yh+yqDYQTO4TMFTwRtXxJPDI8UVAd7HgNi+WzaTzag9HWSeXri+mXLSA6Dwj+fGvjI b/7cc4HZMEJ5shTbPwnD1UJRhAyeZDrgdd4HGABndPOBmc+5ag/LW17dN7F9ldUdEKPY L9y6AuxNJYHq221/SyJiTZ6/mP8eUMyAott/ekYHeeffT3H/zNYiQRU/YiHDJsipXLPn hMYL2jMhBC0UioC1IkLv/Q6C1WsGonWgprOA4IdGMmpq3ofYSDEyKqEKVfA2IzVtE0MN 7sTXu/wI/Jb1uBlq+4GYZixow/2+naMCaVgaCXaaOaOTPfdJ+H2ho57fTHZ3hMeruLj4 cekQ== 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=GypcarpFmcofg9w0yS55PHyEn5260nO5iMhlSCibGMI=; b=kUCfoH3q5Rzjlx7qCvCow4sgxpVANpsOyB2ohfdNv6J/Az9K0MW7fsFuBPmMh0rhy5 SbMYym2w0Skw4RlqNbtTcBZubR5YdW6K7weXAGU27bfiJUSJxGDjoDxGYxCxgx1Kg2D1 RDhTSukvMWy4K7uxd4KZGWsm5B/ulrJT2Stz1IlF/IZfxFwucbxQrUsUGoVdMhzreO77 tJxRQ1tp1L1M9dYn2bSzJAfRV4apS4KiwZquDJlldr736JJn6dGmnhaiRRyeX/7m4Kta NxcuYq02AXm+po/rm9hd+CdQQjduU+ZM5Ee9jgRxTlYIL64xtyQQt1sUz5HfwBy7Yspb hc/A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cs.washington.edu header.s=goo201206 header.b=U6iDqLys; spf=neutral (google.com: 2607:f8b0:4003:c0f::241 is neither permitted nor denied by best guess record for domain of jas...@cs.washington.edu) smtp.mailfrom=jas...@cs.washington.edu Return-Path: Received: from mail-ot0-x241.google.com (mail-ot0-x241.google.com. [2607:f8b0:4003:c0f::241]) by gmr-mx.google.com with ESMTPS id q12-v6si1484897ual.5.2018.06.01.14.52.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 14:52:18 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4003:c0f::241 is neither permitted nor denied by best guess record for domain of jas...@cs.washington.edu) client-ip=2607:f8b0:4003:c0f::241; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cs.washington.edu header.s=goo201206 header.b=U6iDqLys; spf=neutral (google.com: 2607:f8b0:4003:c0f::241 is neither permitted nor denied by best guess record for domain of jas...@cs.washington.edu) smtp.mailfrom=jas...@cs.washington.edu Received: by mail-ot0-x241.google.com with SMTP id l13-v6so30967025otk.9 for ; Fri, 01 Jun 2018 14:52:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs.washington.edu; s=goo201206; h=mime-version:references:in-reply-to:from:date:message-id:subject:to; bh=GypcarpFmcofg9w0yS55PHyEn5260nO5iMhlSCibGMI=; b=U6iDqLys9nFci6+5sQTh6UyKNfLyB8zPtDY9HKm5Vp+MvHI43BM9hHdtz2W9FUcZoh MUOlrSStP+Dsgsd5nvZD5xyKOmJHuYFxsbdfgVciBodHfKvIFwv/qF1uVcer0D3A8ker XJNOkIS6zZ6w07Q72Vdn1DWt+l9oW96QNbmps= X-Gm-Message-State: ALKqPwdvcXL3QJd+q7xd1OPyEP+5uajf6xET40hnT0noX7BSX0/RZqJP LCgqf5V1ftbAZi0tdlRGa1XWqJK7dr7o1FdRnJhfNWaB X-Received: by 2002:a9d:444a:: with SMTP id f10-v6mr8157138otj.400.1527889937383; Fri, 01 Jun 2018 14:52:17 -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> <1efa5fe9-cdc9-4714-ae2a-953ac59cfdf4@googlegroups.com> In-Reply-To: From: Jasper Hugunin Date: Fri, 1 Jun 2018 14:52:09 -0700 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000f9575d056d9b989d" --000000000000f9575d056d9b989d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Friday, 1 June 2018 18:45:42 UTC+1, Eric Finster wrote: > 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! On Fri, Jun 1, 2018 at 1:59 PM Andr=C3=A1s Kov=C3=A1cs = wrote: > 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. > If we don't intend our type theory to be used as a metatheoretical setting for mathematics, it seems interesting to consider for example a type theory with a family of base types indexed by the circle, the syntax of which I think would not form a set. That is, if we have a way to represent dependent type theory in Coq, what happens if we add a constructor `a_circle_of_types : circle -> type` to our syntax (for a postulated circle, or HIT)? This should be consistent, to add a family of uninterpreted types, but I believe equality is no longer decidable (since equality of circle is not decidable). - Jasper Hugunin --000000000000f9575d056d9b989d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Friday, 1 June 2018 18:45:42 UTC= +1, Eric Finster wrote:
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,
then typechecking for this syntax is, by = definition, unnecessary!

On Fri, Jun 1, 2018 at 1:59 PM Andr=C3=A1s Kov=C3=A1cs= <putta...@gmail.com> wrote= :
Type checking must b= e performed in any case, at some level. If we use intrinsic embedded syntax= es, then the implementation of the metalanguage (in a meta-metalanguage) do= es the type checking. Hence, if we intend to formalize a syntax of type the= ory which is intended as a metatheoretical setting for mathematics, then I = think decidability is quite important.

=C2=A0If we don't intend our type theory to be used as a metath= eoretical setting for mathematics, it seems interesting to consider for exa= mple a type theory with a family of base types indexed by the circle, the s= yntax of which I think would not form a set.
That is, if we have = a way to represent dependent type theory in Coq, what happens if we add a c= onstructor `a_circle_of_types : circle -> type` to our syntax (for a pos= tulated circle, or HIT)? This should be consistent, to add a family of unin= terpreted types, but I believe equality is no longer decidable (since equal= ity of circle is not decidable).

- Jasper Hugu= nin
--000000000000f9575d056d9b989d--