From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:ac8:708d:: with SMTP id y13-v6mr4250713qto.11.1527890549745; Fri, 01 Jun 2018 15:02:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:4417:: with SMTP id j23-v6ls21637642qtn.13.gmail; Fri, 01 Jun 2018 15:02:28 -0700 (PDT) X-Received: by 2002:aed:21e5:: with SMTP id m34-v6mr6665078qtc.16.1527890548407; Fri, 01 Jun 2018 15:02:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527890548; cv=none; d=google.com; s=arc-20160816; b=g42HYpAuO0t8EnKEt48bCYEvHpfhg7tEtVIKvsbHU9L7rHT87RHCCyNi2VMwz/ifHj sBdCbonH5BASEIGeObn6prEN5O2kyFOGNOw4P5NthLqQI8ONZHor8uZH7xNvXQy0B8Bu mWXEECxv1g/tdKi+AJmbA55BNr7DRbxGdEi/P2voPW92+s7WGE6Pws/EAoDr/fK+FB0Z hFYkCeo+3skArGIbLp8uBSKmy0VR459C2ofI3CMcC5tt/I9GEDL7FIbm+yDhaLto6CQ7 2j/4FgCf+6cNTksxrOt7vxBNyauQNij/tuxkJB2DfxQnnXiezCjBb1KWmXLVrv7oBbR4 LEUg== 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:arc-authentication-results; bh=F57VZA3pNb3u5S8IBm5KdR80OuyzKssp7KJYoJ5ZsVE=; b=aAsgbPRsTdawWGRXzXo81Yc49cFZNgaFDzPpkh4qEZa26xzp/OVUHB8u5qd2xBw0jR Ts8TX7NqgSAfMuFgFShthiLNnV9rMkbH/bzKv69EIyaPZjnfLXZfFH4I8XS49fpSfZpR EhvgCHuWakAKqAD3eHFYfS+AgnE10wBJ1nC4Sv5RAPkDPUkVG0cDiHVc5Z8PDR+/hjyO gw+wjJ59pcMNb5gqmJyM+xo02tXweK7t1dFGKvfP0SG6BYZ2FpI29KQ6qrLPz8VX8k/5 WdY/Aj1gmhlw+cKAiAijgTJLGXHT9aay+9xQ/lfKMjdc7Z1rO6cVd24ccTFTZ4gHPS46 zAQg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=DyPvtKsd; spf=pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c08::231 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-ua0-x231.google.com (mail-ua0-x231.google.com. [2607:f8b0:400c:c08::231]) by gmr-mx.google.com with ESMTPS id y21-v6si293496qka.3.2018.06.01.15.02.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 15:02:28 -0700 (PDT) Received-SPF: pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) client-ip=2607:f8b0:400c:c08::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=DyPvtKsd; spf=pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-ua0-x231.google.com with SMTP id v17-v6so18325905uak.6 for ; Fri, 01 Jun 2018 15:02:28 -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 :cc; bh=F57VZA3pNb3u5S8IBm5KdR80OuyzKssp7KJYoJ5ZsVE=; b=DyPvtKsdRUaZKKJSkdRveFFa9rUQGUwmUKj+poYvXks0kApGLUNc2HfMPvNtcAZFAu qZP79lat7z8gs0cgdT1dPvaEe4hpgOfoK0NSDQqfvSpz4ce4BPRcN08ddaus323nFHCm 1d1gduBNk7BajHLWnz2/IHmWTrUyb16x049jdTLsD5sy6IiQVHtw/xEMxnOBQPXEWM31 gONsuOMtuVf/QJI137LE4In/j+XV7MRnLNfnuNLt631Wzg/2heKz9hbSWnUhzFWxh6CX l7jlBk9BULS25ZfmF7Ncmt1OxxS2PmbZ4fjP1yhTZZ8QRgdf6SwIM8/yroZIknqRcPWS AWXw== X-Gm-Message-State: ALKqPwcFscciFueMVYc8IZr9JegbIuOmTTvzTIXMf6uZwZ20Iy34TVRT /aqKwvt+OvynIpnHLj3eSI8lQWwxSEU3YTDPMlE= X-Received: by 2002:ab0:5922:: with SMTP id n31-v6mr8908936uad.197.1527890547923; Fri, 01 Jun 2018 15:02:27 -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: Eric Finster Date: Sat, 2 Jun 2018 00:00:36 +0200 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Jasper Hugunin Cc: HomotopyT...@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000005d6103056d9bbd92" --0000000000005d6103056d9bbd92 Content-Type: text/plain; charset="UTF-8" > 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). > > Yes, exactly, I have the same objection. Even if the conjecture Mike alluded to is true, that the free higher category with families is equivalent to a 1-category, I can certainly *force* it to be false by considering the "free higher category with families with some random extra 2-cell". Don't we expect this thing to *also* have some kind of "syntax" presenting it? > - Jasper Hugunin > > -- > 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. > --0000000000005d6103056d9bbd92 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
=C2=A0
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.

=C2=A0If we don't inten= d 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 fo= rm a set.
That is, if we have a way to represent dependent type t= heory in Coq, what happens if we add a constructor `a_circle_of_types : cir= cle -> type` to our syntax (for a postulated circle, or HIT)? This shoul= d be consistent, to add a family of uninterpreted types, but I believe equa= lity is no longer decidable (since equality of circle is not decidable).
<= div>

Yes, exact= ly, I have the same objection.=C2=A0=C2=A0
Even if the conjecture= Mike alluded to is true, that the free higher category with families is eq= uivalent to a 1-category, I can certainly *force* it to be false by conside= ring the "free higher category with families with some random extra 2-= cell".
Don't we expect this thing to *also* have some ki= nd of "syntax" presenting it?

=C2=A0
- Jasper Hugunin

--
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.
--0000000000005d6103056d9bbd92--