From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aca:2c54:: with SMTP id s81-v6mr4975449ois.16.1527888215100; Fri, 01 Jun 2018 14:23:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:4c8c:: with SMTP id m12-v6ls4454055otf.9.gmail; Fri, 01 Jun 2018 14:23:34 -0700 (PDT) X-Received: by 2002:a9d:fda:: with SMTP id m26-v6mr5659271otd.36.1527888214357; Fri, 01 Jun 2018 14:23:34 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527888214; cv=none; d=google.com; s=arc-20160816; b=xEENUneiFzKGB7kcLf1wR+Vq8s1aBTjsshistpZ8hhrNAU469hGkcRT47nlfpLVLTk ZzA5XmGWsXOQVBB2JCNbLsJAugdaxx/FfgFnchBgE93XZ379ofw6wbjAzaAQbdby03oK DBBuin19afTQHJpGjY3r74Dkytuj0MGUuGDpPLAgX5mLLllGSTsxJmVDQ4sIMrhE6dcB 3Z6Vw5OnzzkBxrNQC5dkPgyFQRH/o/9E0wZcaAjLeOHBYSt06M/20nA5Mnp1XYnvwIzH l5hoFpihQn9n4HcNFGu4SEtbBcP4KBDfSqpEmQ20sJlhec/0hQkqNDOfHluGj9Wp0oQY SALQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=x/+7EefJ/GLEPr1H1gM4NYwuCfPkN8z3XsCSuIz94uA=; b=PHGYbJCbM0BSBokH7UhmemZWwueu2kIVFqWLGWUYIii0eCvMW20IORuZugJh+WWJFR FQAzxLp8Y/53FFzclGHEES+pbnny69F2UBohoSfyy0xYr94OmDjPyZYvfhCpRDPgCqgF ROeozgAoDy/SyPYhzEtYwGrGxBYLvunizunSC71e1P/fVI5BMWyWSRyw8baBDe8R30I2 BnFoPF+72CiHLdkXczqdgY1KJolmuk4v14/iCvFQs26QtJXWSIV0LI3JYuG6Awx8cfpP pszR05KpIHLl3Pecp1v9w+E2EIcE6sm7yR+kvue3o7UUSeEl042rEgeebDT8FkKchYrL XeIQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ZbtoFWFC; spf=neutral (google.com: 2607:f8b0:4002:c09::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x236.google.com (mail-yb0-x236.google.com. [2607:f8b0:4002:c09::236]) by gmr-mx.google.com with ESMTPS id s125-v6si118278oih.0.2018.06.01.14.23.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 14:23:34 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::236 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ZbtoFWFC; spf=neutral (google.com: 2607:f8b0:4002:c09::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x236.google.com with SMTP id h141-v6so1993571ybg.4 for ; Fri, 01 Jun 2018 14:23:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=x/+7EefJ/GLEPr1H1gM4NYwuCfPkN8z3XsCSuIz94uA=; b=ZbtoFWFCJQFVqXLapIaNRBf3Ycrh/lnrDRqGANOP/IZEob/pWbJ5MORflFg+yTDdGk yzqxIn83DFvFnPqXIY7kmLp/PnXzdZH1cJPzpejq7TD2Z+JqKRut9tWomfAqujO+evAT p0Yo6uWy+cC+G7meJFFgsG+TH8UcxQIW3WEGI8FujQgEhDbvHLORgsckmpltHzrT6nDE n73EHkccYiueaoOlzNqbEI6GjoPu3f/sv5055Y7HcC7W5/cvBa504ce5vr2m5n57MPmn /PVN5K2mjsTFC9HZ8fMFTPrQsIPBCsEZND/rizhRNAjhFT+7Q3qgOqHPXAjo485kVF99 Ux7Q== X-Gm-Message-State: ALKqPwfYJmRgy+gy0yIi6KAgJM8+Te8Fgxb6T4/xxXZSOurKOKiwpdHO DzlIO+haSaaSwWJwmT4fHszA79r2 X-Received: by 2002:a25:b8b:: with SMTP id 133-v6mr6996103ybl.125.1527888213824; Fri, 01 Jun 2018 14:23:33 -0700 (PDT) Return-Path: Received: from mail-yb0-f175.google.com (mail-yb0-f175.google.com. [209.85.213.175]) by smtp.gmail.com with ESMTPSA id x26-v6sm14532375ywj.95.2018.06.01.14.23.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 14:23:32 -0700 (PDT) Received: by mail-yb0-f175.google.com with SMTP id d123-v6so9200223ybh.9 for ; Fri, 01 Jun 2018 14:23:32 -0700 (PDT) X-Received: by 2002:a25:22d4:: with SMTP id i203-v6mr6750794ybi.505.1527888212486; Fri, 01 Jun 2018 14:23:32 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Fri, 1 Jun 2018 14:23:11 -0700 (PDT) In-Reply-To: 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: Michael Shulman Date: Fri, 1 Jun 2018 14:23:11 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Fri, Jun 1, 2018 at 2:06 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > 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.