From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:ac8:2a58:: with SMTP id l24-v6mr248951qtl.29.1527719757456; Wed, 30 May 2018 15:35:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aed:278d:: with SMTP id a13-v6ls18361395qtd.4.gmail; Wed, 30 May 2018 15:35:56 -0700 (PDT) X-Received: by 2002:ac8:748:: with SMTP id k8-v6mr2482464qth.12.1527719756737; Wed, 30 May 2018 15:35:56 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527719756; cv=none; d=google.com; s=arc-20160816; b=PQBF2SZIkFRyIP96MUcPHPMMVF2lu2eNhfRtAEReauz7+K2m8+MflEvMro98Zk2CbL rEtytbQh7pSmT9EifgN5YxtWZ3h6noVVb6BzXS3BtKTuPrLqDY7IvwOS7BeDYAiRuBKU GiGld8cjc7OGPMLIVpHdBx1qQwWxmbUvMRRowiXYYKkce5ViXWch9uSVfn6lLKN0HyL8 pn4ZW8QT4rvYqahe79Eg/6NZ1CYTQXUMzfa+bn/LG+h77X0yDz/ZfsD/0vi9m+EiAYfk 8VHhqI24T8OPdb/BKsjBJuDvm5F602jK0FYKBcw8Q/pQYU3Ti+Qh/DC1RYW3aKbh9TKc FNYg== 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=aCrUfe7njIeUGonCIYEGnSS+PGVLNnEbjVkI4/w7Pyg=; b=diuCO59OFd5JEoxoL1PaHLgJX1hteu/qjT6qYeLMccixeSo/mWBueXQzR2f0WJuwWo KHzUektob6FVYkZlB/w89FfEhuYDfEqydoocrh95x1KOMqiYQ8a+n6m+rAr8aZyTgbDP rF4VJSZBoDBLFXhXNSmmiWTtbZKdAKAMm6sMoitJTLH/+bForheIn5u2S+ycIsIefY9u +HTsBevFqpKoF1B3suUD0yZfX2K3a4rWwoZk8Fxx+fHhUaEAPyLJVUE4vMZZAKOhv6Af r36XrOF39RdyfJsU8xbxSoCkZc+Q1ipmgUB752m3lnId2p6JUp84m1UGnNCnvI0GuYsc o2UQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=04vcqbQW; spf=neutral (google.com: 2607:f8b0:4002:c09::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x232.google.com (mail-yb0-x232.google.com. [2607:f8b0:4002:c09::232]) by gmr-mx.google.com with ESMTPS id j1-v6si1086892qkk.2.2018.05.30.15.35.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 30 May 2018 15:35:56 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::232 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=04vcqbQW; spf=neutral (google.com: 2607:f8b0:4002:c09::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x232.google.com with SMTP id i1-v6so6939318ybe.1 for ; Wed, 30 May 2018 15:35:56 -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=aCrUfe7njIeUGonCIYEGnSS+PGVLNnEbjVkI4/w7Pyg=; b=04vcqbQW2tLptgop19WvbZahwfpKk+4zij1PixKMooVa0vClHseh10zamtbfvg7gZE LgcyzotiTNlK4JBCr+/QzvGm7SL3CztoBGQ90PUV/1OQVrSlHz6HnmyDlSgq9b/0y7lh Zb0dx/K1XUc/CyOW+7XIJC/qwk8mnKC6bQ/3j4jIFL9zWr7s83u0dtBkYV17UhhhETHo 3C9zq5tVLcw/4KAeEXs86gum22sXKPiZ4/L8b6LyVSCrRc/0X11GqzpP2KuXe0v/hL/D 3G2wt0he1a/DJ4L9hKqNCVwj/A8V4HrI6JWc/KyZJw6C1U7vSsmRWsGm1Yb/1m9N4hRL CW+w== X-Gm-Message-State: ALKqPwdb92fXKkC6UPRUZpArJXsoAQO1+tN84/hhO/+YV4o4jahH4DDN UL6jnY2Emb3udq+r5Vzf4CuPa3ew X-Received: by 2002:a25:7cc5:: with SMTP id x188-v6mr2648543ybc.164.1527719756183; Wed, 30 May 2018 15:35:56 -0700 (PDT) Return-Path: Received: from mail-yb0-f174.google.com (mail-yb0-f174.google.com. [209.85.213.174]) by smtp.gmail.com with ESMTPSA id n187-v6sm7423982ywe.66.2018.05.30.15.35.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 30 May 2018 15:35:55 -0700 (PDT) Received: by mail-yb0-f174.google.com with SMTP id i1-v6so6939304ybe.1 for ; Wed, 30 May 2018 15:35:55 -0700 (PDT) X-Received: by 2002:a25:2bc1:: with SMTP id r184-v6mr2656401ybr.120.1527719755241; Wed, 30 May 2018 15:35:55 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Wed, 30 May 2018 15:35:34 -0700 (PDT) In-Reply-To: <1527602447.1037774.1389070656.2CE32C72@webmail.messagingengine.com> References: <1527602447.1037774.1389070656.2CE32C72@webmail.messagingengine.com> From: Michael Shulman Date: Wed, 30 May 2018 15:35:34 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Jon Sterling Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks, Jon, for that very detailed and thoughtful response. I agree that there are significant differences between the Homotopy Hypothesis spectrum and the Initiality Hypothesis spectrum -- how could there not be? But I don't think those differences invalidate the analogy. The gap in the homotopy hypothesis is not uniform either: for instance, in addition to algebraic vs nonalgebraic, it comprises cell shape (globular vs simplicial), and there are other dimensions too such as whether a definition can be phrased in an ambient homotopy theory or whether it has to be built out of sets. In other words, the "spectrum" is actually multidimensional in both cases. And non-algebraic notions of higher category were not alien to category theorists either; indeed, the very first proposed general definition of omega-category (due to Ross Street) was non-algebraic! I'm grateful to you, Thorsten, and others, for trying to help me get over my hangups about explicit substitution. I guess that fundamentally what matters is the existence of normal forms and of a terminating normalization algorithm, and that applies to beta-reduction as well as to substitution-reduction. I personally find it more elegant to regard the normal forms as the "fundamental" objects with things like application and substitution as defined operations on them, rather than regarding application and substitution as term constructors and then having to quotient by beta-reduction and substitution reduction -- why introduce flab only to quotient it out later? And I have an easier time with explicit applications than with explicit substitutions, because I see the former but not the latter all the time in everyday mathematics. But I can see that the other approach has advantages as well. On Tue, May 29, 2018 at 7:00 AM, Jon Sterling wrote= : > Far from being a result which might hold or fail about "type theories" (w= hat are those, specifically?), I take it that your parenthetical refers to the lack of a general definition of "type theory". But to me, such a lack is itself a gap in the literature -- how can we really consider "type theory" a respectable mathematical subject if we don't even have definitions of the things it studies? The lack of such a definition is not a reason not to study type theories in general, rather the opposite -- studying type theories in general will help move us towards being able to formulate such definitions (note the plural -- I don't necessarily expect there to ever be *one* definition encompassing *all* type theories). > I think that initiality is a purely definitive principle by which we can = measure any attempt at formulating an algebraic notion of type theory (and = there is no reason a priori to expect this to explain type theory as it exi= sts in the wild, because the latter kind of type theory was never intended = to be algebraic). I don't think the fact that "wild type theories" (interesting associativity there with the biological notion of "wild type") were "never intended to be algebraic" is a reason not to study their algebraicity. In fact it's *more* exciting when something that wasn't *intended* to be algebraic turns out nevertheless to be (equivalent to) something algebraic! Such unintended coincidences are what mathematics thrives on; indeed HoTT itself arose from a gigantic unintended coincidence between intensional type theory and homotopy theory. > The gap between algebraic type theory and the pre-term-presented version = of type theory which still has unique types etc. is a purely bureaucratic g= ap I don't think that's a fair characterization, because it seems (likely) to depend on fundamental features of a particular type theory. In his talk Thorsten mentioned that the proof of decidability of equality for QIIT syntax uses a normalization, and the alternative argument I proposed using hereditary substitution also depends on the existence of the latter, which is essentially a normalization property. I wouldn't call something "bureaucratic" if it depends on essential features of a particular situation and doesn't generalize to slightly modified situations. > I believe that the interesting gap that we should study (using tools from= the study of elaboration, coercions, coherence, etc.) is the one between "= wild" type theory (where you you have subtyping, implicit coercion, etc.) a= nd algebraic type theory. I agree that elaboration is an important problem that we should study, but I don't think it is "the" problem we should study -- other problems can also be interesting and important! Thanks again for the interesting discussion! Best, Mike