From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.53.98 with SMTP id b31mr1859403qte.53.1508439840451; Thu, 19 Oct 2017 12:04:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.200.19.197 with SMTP id i5ls3514864qtj.13.gmail; Thu, 19 Oct 2017 12:03:59 -0700 (PDT) X-Received: by 10.55.31.166 with SMTP id n38mr1811328qkh.57.1508439839845; Thu, 19 Oct 2017 12:03:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508439839; cv=none; d=google.com; s=arc-20160816; b=Cjr06wlXRXOMkDbEu08Jm47xmZOBXwthB3xXib//VbrB3JTIrfbd6ky+gvxCrMrYR6 g9+rYXPz8pmfB8njMGuXZc+92s9eaiMUDQfDXtsbFtTe/11FO/cdlOxGKnAqi/ApjrYk 9oKRBK9B8md/9H8h6qsSn4c1FA/wvDoCXLIxfWPbtldsLK5r/IQinaeLYGiF8k7qEdEJ h5PyIpCYswfO7RAViJRmuxKHJdqy8F53iYW9/8e7lTvo9cj7p3krv8PkA8CND4mcSv49 Euzge68Ts8c2YsJB/xEfsE2bV1ApRxZ86AjTiq9/nkDMWKCw04dhGJuJqeJCBnqO2kqR uNtQ== 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=qG9t6F8zalWZTf+VTvqG/jwf4wEQ6FO4c0Jc6LzGVZ4=; b=v6hYCG2Kr3nD53aETUGTQ8pwHaSvzRKF42+VRyB2rv24XShUjIVJAp+KOa7La7Zw6Y wMA9wh0hQ0GdneYpcuu7YRfGVQbjAe3ENYcLbAfxuNNTTUBxDw1b1J43g2qBwPyyy0MG 3PiXvp8xYDXwhQ+k3Or9dA8FOpYuHZt5VM0nZPAhRJgryXrRSJV/1ge6JT6dYzwKiZAf cn/4tyQow/VWcfnGOWNvgd5XyceUJ6TvJjomvycY5gncs+ylkNBjSja0ajV7xMTErYa7 4FhYCWjYo3SGBFM389B7bCqJp5ulP/LG6rJz9fTCaO7bPHHIMaq9R7tT9Ady2eBhggF5 CMXw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=LhWi7IAk; spf=neutral (google.com: 2607:f8b0:4002:c05::235 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x235.google.com (mail-yw0-x235.google.com. [2607:f8b0:4002:c05::235]) by gmr-mx.google.com with ESMTPS id 5si1042238qki.1.2017.10.19.12.03.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Oct 2017 12:03:59 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::235 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::235; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=LhWi7IAk; spf=neutral (google.com: 2607:f8b0:4002:c05::235 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x235.google.com with SMTP id q126so1477487ywq.10 for ; Thu, 19 Oct 2017 12:03:59 -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=qG9t6F8zalWZTf+VTvqG/jwf4wEQ6FO4c0Jc6LzGVZ4=; b=LhWi7IAk2sd9a08wg84f4CFrhXe/YyV/f5N+zOXkxKoYqmcQfK0/GDDqc2dehtSAqQ d6bKCq124bn0pxYKX9ADW03d3pz6osiMx1bqJ1Tk2gsngJyJOfQHImHZnojazYv1zALr kRyE/J/Q8dNOj3lZkKrqZ9TAf/wRc1NM8dELHR1DPeYDwQzzog8JqHKw9AejRuFyeqL4 moKvHZvst4olIkAqDzAuhtxK2Vb1Ikjayz/AgumCb0xIGoWdORIYSNHE7uTd3si1/w28 Bzzb5EP+T1yCtA/PGb7VTdXmay88qVE8HwbMaIpoFPmBE+2WRuSOEnCU/GIsER3eYmLC DLXw== X-Gm-Message-State: AMCzsaVYCDwPdzQVEFDkPHOu/081Em1rBdv4hzwlpGzs40/w+bxpW1Es Pt8dy3fAWQfqijuAD6+nSuhHrQYL X-Received: by 10.37.214.10 with SMTP id n10mr1582926ybg.115.1508439839308; Thu, 19 Oct 2017 12:03:59 -0700 (PDT) Return-Path: Received: from mail-oi0-f50.google.com (mail-oi0-f50.google.com. [209.85.218.50]) by smtp.gmail.com with ESMTPSA id w199sm8330642yww.10.2017.10.19.12.03.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Oct 2017 12:03:58 -0700 (PDT) Received: by mail-oi0-f50.google.com with SMTP id w197so16562792oif.6 for ; Thu, 19 Oct 2017 12:03:58 -0700 (PDT) X-Received: by 10.202.196.135 with SMTP id u129mr1465645oif.48.1508439838297; Thu, 19 Oct 2017 12:03:58 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Thu, 19 Oct 2017 12:03:37 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Thu, 19 Oct 2017 12:03:37 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Canonical forms for initiality To: Andrea Vezzosi Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Tue, Oct 17, 2017 at 12:33 AM, Andrea Vezzosi wrote: > This is interesting but I can't quite see it, what would be the type > of the "graph of associativity" judgment? So there is a judgment for context morphisms =CF=83 : =CE=93 -> =CE=94 and a judgment for composites thereof (2-simplices) s : =CF=832 =E2=88=98 =CF=831 =3D =CF=833 then one for the graph of hereditary substitution: t=CF=83 : t1 [ =CF=83 ] =3D t2 and then for "associativity", or I suppose better "functoriality" of that, which is a 2-simplex of some (semi-)simplicial set lying over the (semi-)simplicial set of contexts and context morphisms: ts : t=CF=832 =E2=88=98 t=CF=831 =3D( s ) t=CF=833 where t=CF=831 : t1 [ =CF=831 ] =3D t2 t=CF=832 : t2 [ =CF=832 ] =3D t3 t=CF=833 : t1 [ =CF=833 ] =3D t3 s : =CF=832 =E2=88=98 =CF=831 =3D =CF=833 and so on > And how would you use it in the term/type judgments? In an intrinsic presentation of dependent type theory, the rules for variables are kind of forced to be de Bruijn, with something like ------------------------------ (=CE=93 , A) =E2=8A=A2 pop : A [ =CF=80A ] =CE=93 =E2=8A=A2 t : B ------------------------------ (=CE=93 , A) =E2=8A=A2 shift t : B [ =CF=80A ] where =CF=80 : (=CE=93 , A) -> =CE=93 is the weakening context morphism. W= hen you try to define hereditary substitution into these, I think you end up having to compose context morphisms, and then when you try to prove functoriality for substitutions into these, you end up having to talk about 3-simplices, and so on.