From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:147:: with SMTP id 65-v6mr2666840plb.41.1527890132180; Fri, 01 Jun 2018 14:55:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:968a:: with SMTP id n10-v6ls16190260plp.13.gmail; Fri, 01 Jun 2018 14:55:31 -0700 (PDT) X-Received: by 2002:a17:902:424:: with SMTP id 33-v6mr2692502ple.31.1527890131418; Fri, 01 Jun 2018 14:55:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527890131; cv=none; d=google.com; s=arc-20160816; b=xlU/N0emvfJ7bW2XpIWIDbD86igLaGopoQ8GcFvtjv4E3/dj0iGymOs+JjFYnnFnSu DOKHdbDDvRKlfR/Sjv+Dizhazl3cNgfkwLn4RcT/rs5NyL1q/JU3oUsT3dGBgX9HcUvp uSVTOR/p1mDblSc99Gg00io72LNLrzfLbqxjTVNZUoDMl2NMxwYb+55nOj+Y592xGqrZ 1Xek5HJsQn2HEdCtBezXTh6hO7BVirhr6SpX5vEGfwMqASsfgBSM/V3jl2s2u4JopDIH ReWOO4ucAfQhkcV1spd00zRmvoVBBYNUqzlTQNMXoCxir1ejlqwEjGCE91DW05qC2BY2 l/jg== 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=5L3TyEfpdmuRWvm6c4l+oY8wGsqAAAOdZv1QCtQ/LXk=; b=IuOPTmX2LOe0mJsixCqyWwXxNUBmLkH97Bngv0r/ZFIfb4pH80fqYiNARdyytjVIXl S6SHogrgY8EWbg3bPNCEvoyeY70NtQtlel5pT5RBtIeZDhPHlqRJwNRY5xR9VOoyEusM v56BYDshlJUXfoOGv3m7tmhc7eTmIq2tB3V5Iwu4B3Saa02VHF6iE77hUZeTtr16jjA8 i2QIZo6TCaFLeCupRSKgbPuz+BbG0qr4Un8X0m/cSvo2bCoRe3je6TEkjP1iVcv07EvX D/i0bKor2345ruRk32mb/ubgm6rStfW5z/Qo+lzaxI9pQ1dmZGJW1yZPwd1eCkm/HFrL VV4A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=XT4UnUu2; spf=pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::233 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-x233.google.com (mail-vk0-x233.google.com. [2607:f8b0:400c:c05::233]) by gmr-mx.google.com with ESMTPS id g9-v6si436477pfh.2.2018.06.01.14.55.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 14:55:31 -0700 (PDT) Received-SPF: pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::233 as permitted sender) client-ip=2607:f8b0:400c:c05::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=XT4UnUu2; spf=pass (google.com: domain of ericf...@gmail.com designates 2607:f8b0:400c:c05::233 as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-vk0-x233.google.com with SMTP id o138-v6so6337410vkd.3 for ; Fri, 01 Jun 2018 14:55:31 -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=5L3TyEfpdmuRWvm6c4l+oY8wGsqAAAOdZv1QCtQ/LXk=; b=XT4UnUu2qXiS2mRcTHqsAbicN/dlLL7h9gYC5BS02fMyZvNm6+nUsn7anMxGPFAedU MTTvgyVMmfjRDsUstQF7Y3rBX9VXbde14iBzBwfs9LMlkjA9qtPcOtVqA5OY4qNSsgQm qZfaCfwzTnYrqm1FxJyB6qwWuDx4JVfSX0UmsKsDvH9gMl1gnFDVxSwovAOnEj9Xi2AW 8dGmZn/DbVFgkaBDEdNgWbyiUXXZj79OrhD3ciY2o0HPYLstigkUe36sHk5D1BIhFM2r oVH1nwwgTmXINlUJJwZuPNXX/f9YqTX747dLiUjtloEyDenepN9EIT6j4CQ47F4I4yl0 AaJg== X-Gm-Message-State: ALKqPwdcHGFF5ujcr66rk4rX0kYn8GknDE2MS4qzVcyCjB2R0AcB9Etg FCBPNHZ1/Dxn25xAuCkFitirug9fAooKUhkv7vE= X-Received: by 2002:a1f:31b:: with SMTP id 27-v6mr7650653vkd.114.1527890130995; Fri, 01 Jun 2018 14:55:30 -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: Fri, 1 Jun 2018 23:53:39 +0200 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Michael Shulman Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000838de1056d9ba46e" --000000000000838de1056d9ba46e Content-Type: text/plain; charset="UTF-8" > > I don't think the initial model is a set. Is it? > > This is the big conjecture that Thorsten and I actually agree on: that > the initial infinity-CwF in fact happens to be a 1-CwF. Thorsten > wants to prove this by explicitly constructing the initial > infinity-CwF and then proving that it is a 1-CwF; my preference would > be to construct the initial 1-CwF in a careful way (e.g. with only > normal forms and hereditary substitution) so that one can prove that > it is in fact the initial infinity-CwF as well. But in both cases the > conjectured result is the same, and even the important ingredient in > the expected proof is roughly the same: the existence of normal forms > and normalization. > > Right, and I think I'm more or less on board with the conjecture. Although as you start adding more structure to your CwF, things get a bit murkier... Is it still okay with dependent products ... umm ... and what about if I add a class of HIT's? To take things really far: if there is such a thing as the free elementary infty-topos, is it a 1-category? This somehow seems dubious, no? So it seems to me at some point, something has to break in our notion of what syntax for higher algebraic objects *is* in the first place. Which is why I would not want to make the assumption from the outset that syntax must necessarily be decidable. --000000000000838de1056d9ba46e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
=C2=A0
> I don't think the initial model is a set. Is it?

This is the big conjecture that Thorsten and I actually agree on: that
the initial infinity-CwF in fact happens to be a 1-CwF.=C2=A0 Thorsten
wants to prove this by explicitly constructing the initial
infinity-CwF and then proving that it is a 1-CwF; my preference would
be to construct the initial 1-CwF in a careful way (e.g. with only
normal forms and hereditary substitution) so that one can prove that
it is in fact the initial infinity-CwF as well.=C2=A0 But in both cases the=
conjectured result is the same, and even the important ingredient in
the expected proof is roughly the same: the existence of normal forms
and normalization.


Right, and I think I'm more or les= s on board with the conjecture.
Although as you start adding more= structure to your CwF, things get a bit murkier...
Is it still o= kay with dependent products ... umm ... and what about if I add a class of = HIT's?=C2=A0=C2=A0
To take things really far: if there is suc= h a thing as the free elementary infty-topos, is it a 1-category?=C2=A0=C2= =A0
This somehow seems dubious, no?
=C2=A0
So= it seems to me at some point, something has to break in our notion of what= syntax for higher algebraic objects *is* in the first place.
Whi= ch is why I would not want to make the assumption from the outset that synt= ax must necessarily be decidable.


=
--000000000000838de1056d9ba46e--