From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.11.203 with SMTP id 69mr6641591oth.22.1508225602995; Tue, 17 Oct 2017 00:33:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.12.144 with SMTP id b16ls228218otb.5.gmail; Tue, 17 Oct 2017 00:33:22 -0700 (PDT) X-Received: by 10.157.90.25 with SMTP id v25mr6205405oth.60.1508225602261; Tue, 17 Oct 2017 00:33:22 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508225602; cv=none; d=google.com; s=arc-20160816; b=e/dvf+rZaiybJR0VqGChBeevmUZh9pDQkFihexhilZI9E/QrCrg11O8ETcAMG/dHW5 jfBwgwG18iOgSMibDZk74iSHtLvQBRiUT7zFWw2+/j29sIMkiwJas0VujfnHL3tnpsc9 EASi8Hn/MPdMmeJ8jO+2GpkbzYHfJNNeU5MnprZoVfDHkNUh5AdB958ImSuRPySzW75r H6ZhTPtR7RSZAwjUgL0NNhQUTxiVKEyJldRijwA2+DdP9Yuzsj9FgG9iUe0llbiooJHY VrvVt2twea75vKGem41yzF47+mauNPFVzPBbAiLTlTUK5LjjAb3py+8XlJEIwZYiaLfP gYEg== 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=S/RO7/Bvrqiq/gIM91prizjzSfrdnOfMDJTH9c054fs=; b=x21QgPeQMTi7vw7sYm+hYWV9ssKjd/VySBHjEFpey9FuRrW5Mgl5ZQvA6a/F8Es2Ut 1g3vw8zJGfOmPEKjJYhlupdoXGitZeYfa26kPtNsDLZ3bMbTfr8b4XQKJpj/Q3kB6O+k l+Oxge1gg/SXJInHdXrRHtNhPq7bcLOPHUILXMAxskBYETR+fgdekvZUBphm1BOGjDx3 sq8fs+/JIr61cS9aWg+Ljbftx2oKy3dZawJrlrCBctnBN/MoNXJTHuhpv2aO+rG9XzWh hvlFK7yu61jqx5x3PchuvZTlAVjbcLApcHx/XnaSQlaipxbUxnsbrq803rc4prbyvfep dJtA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=RCvMMISV; spf=pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c0b::233 as permitted sender) smtp.mailfrom=sanz...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-it0-x233.google.com (mail-it0-x233.google.com. [2607:f8b0:4001:c0b::233]) by gmr-mx.google.com with ESMTPS id q7si393469oih.5.2017.10.17.00.33.22 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 17 Oct 2017 00:33:22 -0700 (PDT) Received-SPF: pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c0b::233 as permitted sender) client-ip=2607:f8b0:4001:c0b::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=RCvMMISV; spf=pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c0b::233 as permitted sender) smtp.mailfrom=sanz...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x233.google.com with SMTP id l196so1255498itl.4 for ; Tue, 17 Oct 2017 00:33:22 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=S/RO7/Bvrqiq/gIM91prizjzSfrdnOfMDJTH9c054fs=; b=RCvMMISVZ+XnkaMC2Pvc5lur42PT/ZOJd5Y4cvgEqom6ok+GkW79G+7923dHvuWBZ8 E9fSNz89kQa1TgcTqWfwKZGKxLBFjh1On/6PBbM7ntGjtEkUGWADJJGpxurfrkmx+l2J 7RpSgrN4+/sWMt6cKX4dHHGpUSb/iL2Ko14/L8flFTrEtb1/nztZPaiKXhqXpuVT+GwA EmX/oRAit57uQqu0G0hkdqo9jWERjWzPIm3R7XsBDK7Ww8F19iSCWPd4LAp2Yjdf+9JK b9B3xzMek/ZM6XFL7uEPOmopqUgq3rUUGxKVQo6tW47b0Z+2td5/bGuM4sel42Ag0HP4 f6Ag== X-Gm-Message-State: AMCzsaXWeGyBj9BqCQQceVWXxVAbQN7JE01CczcZkSccFszWx+hpEAXg aqYBX4VvjCV60dJmdXejhLcJqNxX1flpxogtwk8= X-Received: by 10.36.33.23 with SMTP id e23mr4638923ita.109.1508225601616; Tue, 17 Oct 2017 00:33:21 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.200.79 with HTTP; Tue, 17 Oct 2017 00:33:21 -0700 (PDT) In-Reply-To: References: From: Andrea Vezzosi Date: Tue, 17 Oct 2017 09:33:21 +0200 Message-ID: Subject: Re: [HoTT] Canonical forms for initiality To: Michael Shulman Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" On Mon, Oct 16, 2017 at 7:01 PM, Michael Shulman wrote: > [...] > However, when doing this intrinsically (which is the direct way to get > a useful induction principle) and without h-level restriction, I found > that there seems to be a new problem: you end up needing to substitute > hereditarily not just one term but a whole context morphism, and then > in defining the clauses for the graph of that hereditary substitution > you need to know already that it is associative. So you add another > judgment for the graph of its associativity, but in defining its > clauses you need to know that the associativity is coherent, and so > on. This is interesting but I can't quite see it, what would be the type of the "graph of associativity" judgment? And how would you use it in the term/type judgments? > The result is an inductive-inductive definition with infinite > dependency, which we don't know how to make sense of internally. But > if we can make sense of it (or make it finite by capping the h-level > somewhere), then this tower of dependent inductive-inductive types > ought to present the entire (semi)simplicial nerve of the syntactic > category of the type theory (probably in the form of something like a > "comprehension quasicategory"). > > The induction principle of this inductive-inductive definition should > then let us interpret it into an arbitrary sufficiently structured > quasicategory, or even an internally defined "complete Segal space" if > we do it in a homotopy type theory, such as the canonical universe, > thereby solving the autophagy problem. On the other hand, since it > has no path-constructors, an encode-decode argument should prove that > it actually consists of h-sets, which should then allow us to > interpret untyped syntax into it. > > Of course this is a VERY rough sketch and there are a lot of ways it > could go wrong, plenty of which I expect people will point out. (-: > > Mike > > -- > 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.