From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a24:7d91:: with SMTP id b139-v6mr5574961itc.6.1527891009472; Fri, 01 Jun 2018 15:10:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:784b:: with SMTP id p72-v6ls8117449itc.9.gmail; Fri, 01 Jun 2018 15:10:08 -0700 (PDT) X-Received: by 2002:a24:28c7:: with SMTP id h190-v6mr4258265ith.20.1527891008684; Fri, 01 Jun 2018 15:10:08 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527891008; cv=none; d=google.com; s=arc-20160816; b=wYspBOe39xaVxuz+LZBKLSRMChZCQXBLudXJsEfXiStONOqVFqxNQExYThVW7hIvbx /V8+kI7TOZ/L1lvmcLoYvdiz1wiNpPIbLcVcRrIJrL82YI2qiXmUC0yQkQnrxsOOBeiZ riXBnl4qN8tRjdHrme/kzRtOH0mtKzMBqxYEawya7Xz4U3ndye4PXzW1JTREz5q9PT3v Zwr5p05JiMHGF/5v+ZIEZeDvKxiorZbCp5G9wgv95hwsP4vgkMfokH7GmjJWUt1xMFaK qbO9Sp5naHGcJpau5p7jCslaaMfkjRvXwUwqrpyfk5MVMqKX++EJ7/wiO1GRUVU39O1Z 1vww== 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=3CofTLnT9moYSzrR1CwsCwxiCJX1JW65NrxQf8LINBE=; b=XlgKOjqzTpfECLSZahAtonTFEte2R7gsy3yEPPEM3c4I/UOsAfTM2iFqfFed0v6SIW G8eYCPFKvrilebUUI8FDQjUzPC9AyUWmGMITxoFKdc724lf763qUrz1yF8tskDdG1swL qQn/UrQJxlHIM+5U77RpX7ht6fRGFovQghpIemMFaeWIHmZuhNucTtpOEA6WpSOTF/s4 Adh90fjLQXdb3/qIf8wo5eVjL8Slf/2MWlV/5voopsawWYdgj8115W2ACi5vH5Ix2Ar4 EdAAQ04f70A7lRbYhEf+rOsSuY+K0Gyd3v7pvmkeaIM1Gqj/ZzspQMGMf1jenlzTIUPU wRKQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=n2sJ4KXK; spf=neutral (google.com: 2607:f8b0:4002:c05::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x236.google.com (mail-yw0-x236.google.com. [2607:f8b0:4002:c05::236]) by gmr-mx.google.com with ESMTPS id u18-v6si103401ita.1.2018.06.01.15.10.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 15:10:08 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::236 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=n2sJ4KXK; spf=neutral (google.com: 2607:f8b0:4002:c05::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x236.google.com with SMTP id 81-v6so5136523ywb.6 for ; Fri, 01 Jun 2018 15:10:08 -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; bh=3CofTLnT9moYSzrR1CwsCwxiCJX1JW65NrxQf8LINBE=; b=n2sJ4KXKJb4cBfwx4nTIwz/np828ahFIkehn26CG3bNBUCnDucPRKEVSdz1ldaoxVe gTfzQbSDLl8eBhwTisWVuNGl8eAoBV/clpqYdf9oOqXbbFb4I9DDOeTMFcfuYCKmMocs gvdS1NdTXRb+JjTsKqAxbSkqB414wM1TA9mnOdxiIDIFIw3Jq+oIqN1Ex50WCYrBr2Ci xOipDUnfPzOnXPc66KWiabVRGcfNv4gk9Hy4gkPqH69jpzfZlsuaH3a1gtWfmkwfLv+a OLXZvIrQFkpizsJfWhHApzE92hECjdGArF8aAKSun9qxvQnBTd9iiwC+cZD44wd9ypjB IcjA== X-Gm-Message-State: ALKqPwcvk7VHx4ByI0pjOVF6Yk8pzHBh7S4ZH9Drwd4jmr8tXWBoNCXC uw2h+6XOl+3q9DZ/4Eof3SR1oArO X-Received: by 2002:a0d:e001:: with SMTP id j1-v6mr4580875ywe.202.1527891008194; Fri, 01 Jun 2018 15:10:08 -0700 (PDT) Return-Path: Received: from mail-yw0-f178.google.com (mail-yw0-f178.google.com. [209.85.161.178]) by smtp.gmail.com with ESMTPSA id l197-v6sm6537462ywe.61.2018.06.01.15.10.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 15:10:07 -0700 (PDT) Received: by mail-yw0-f178.google.com with SMTP id v68-v6so8760058ywd.3 for ; Fri, 01 Jun 2018 15:10:07 -0700 (PDT) X-Received: by 2002:a81:7acb:: with SMTP id v194-v6mr1508881ywc.193.1527891007470; Fri, 01 Jun 2018 15:10:07 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Fri, 1 Jun 2018 15:09:46 -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 15:09:46 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Eric Finster Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" My intuition is that the conjecture should be true for any categorical structure whose corresponding type theory satisfies normalization / cut-elimination. With my suggested approach the idea is that if there is normalization, then you can define the initial 1-structure using *only* the normal forms, so that there is no need to add path-constructors at all. Then instead of a HIIT/QIIT you have just a normal IIT, which will be a set as long as all its parameters are (this being necessary, as Jasper pointed out); and you can nevertheless define maps out of it into higher types using its induction principle. In essence the situation is similar to how the free oo-group on one generator (the integers) happens to be a set, because we can define "normal forms" for integers as positive or negative unary natural numbers. This sort of thing is also known to happen elsewhere in higher category theory; for instance, the free bicategory on a directed graph happens to be a 1-category, because instead of constructing it by throwing in all binary composites, associativity isomorphisms, and so on, we can normalize all bracketed composites to be (say) left-associated. This is essentially cut-elimination for unary simple type theory. So, if we have a type theory for elementary infinity-toposes that has normalization (perhaps some form of cubical type theory), then I would believe the conjecture should hold fo them too. Note that this doesn't mean that the *objects* of the free elementary infinity-topos are *internally* sets -- that would certainly be false since it contains universes. Instead, it means that the free elementary infinity-topos can be *presented* by a structure (e.g. a CwF) that is *externally* a set, just as the model category of simplicial sets is itself a 1-category despite containing objects that are "internally" (in the model-categorical sense) not sets. It seems to me that the question of whether syntax should be decidable seems to be just a question of definition as to where you draw the line separating syntax from semantics. Does a HIIT initial infinity-categorical structure that is not decidable count as "syntax"? Is it "syntax with a heavy flavor of semantics", or is it "semantics with a heavy flavor of syntax"? Whatever we call them, such things are certainly interesting! But I'm dubious that we could use them as a foundation for mathematics unless there is also an untyped extrinsic syntax that can be typechecked into them (which might or might not require them to be decidable). On Fri, Jun 1, 2018 at 2:53 PM, Eric Finster 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. >> > > 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. > > > -- > 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.