From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.123.69 with SMTP id w66mr2245015ywc.143.1507973837218; Sat, 14 Oct 2017 02:37:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.129.88.214 with SMTP id m205ls659532ywb.29.gmail; Sat, 14 Oct 2017 02:37:16 -0700 (PDT) X-Received: by 10.37.114.134 with SMTP id n128mr2213973ybc.44.1507973836489; Sat, 14 Oct 2017 02:37:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507973836; cv=none; d=google.com; s=arc-20160816; b=mCk/KAQ4RVlfAoRpWjMPdQZveJkDpRIdgZKgbH1Kl/m/WbZXYYWeTefJyVU2kMdcBz nzadFAIeBfN87/Mgrfww/XEtR2GZ4y1S2Yav98MT1DzMcB7BSr2zS9RMZaTrZTyUilU/ gDx/b0+LLI5lzOFsNXGim+DR8X9s2s05HxeIgOfoanHxENhJy8cJXBOx9dYHeO8k8M/o w87sKRxycQrxBQ3dUMk4t5fyurv4e/q7z/AHeHhsdt/1u080/NfcRn0SxXtf0TV6NTKF XwVFSJlEo62SdX3FBIQngbALjEax5m6Zq4VIe2a4AvNlvBH0JO9LtEo3V4wLrRWLEXc6 kyBw== 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=SwgNgHboop4WYtqr7a7tDc3RDXflCLZKEgt4oe4+DGc=; b=UHh6eRn6zc0v/DAK36oTVNAW8pfiL9+ombK4Unz3eqvbT2AmPfdSVvseEQLeSE/fbu n27rBWp7hcKkX3vGZaVCVMLLW+k7gtaaMydbvSVDzqXiQrqFmtqhBqVPnKof5Z0DrxeD 2fH0YxI5zTCiGe1S465refcYU5mNxg7Ltg+qClrOOce4fTAxq4WBfoE7hyWRMOBpWJS5 yRR3Fx9+22Di6cqgbxhtxhjwhAvf/hsGRuzx92szRUSgbAKhMm15PG0Ln7Ox5p3Wwr48 rMz1eTJS4/yCX5mQQ9Hv+ILr5oeeAO9kbHojCHBvd4UCShq2g1Xor1x7bSnAKVCb30GH S0Fw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=oBDAOjiA; spf=neutral (google.com: 2607:f8b0:400d:c0d::232 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Return-Path: Received: from mail-qt0-x232.google.com (mail-qt0-x232.google.com. [2607:f8b0:400d:c0d::232]) by gmr-mx.google.com with ESMTPS id d62si135021ybc.4.2017.10.14.02.37.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 14 Oct 2017 02:37:16 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::232 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c0d::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=oBDAOjiA; spf=neutral (google.com: 2607:f8b0:400d:c0d::232 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-qt0-x232.google.com with SMTP id n61so23658225qte.10 for ; Sat, 14 Oct 2017 02:37:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=SwgNgHboop4WYtqr7a7tDc3RDXflCLZKEgt4oe4+DGc=; b=oBDAOjiAhy8HmHv9vHTh88ERM9Bk/WDUJGscVzzVqHEgJ7VNgHsYEkm0dmxIZyKUNm maophDqlo2ztBf8ijLTpwGBIATAXqAriSPVITSQFC+OskR+4gf7BeiFoClGzPox2PB2e Ug8QI8iEAVrfOBaSN/ESgrEfDltaicBrc8hWTpOZD8pO4oNckrpyu8aZDe11bxZl4Rjx LhQXW2NgPlAklJlUXpr06ZBDftElU+MbPKq8cXyAhcqp3AL1FL5hokSDj/lQ9IR05bzu cWK5TZB1aPXkUCJBvqYhrFgVDnjI36YGw++rjc6nDnlql2LR/LtFv3Z6wB9CY2lcI9Eg S+Aw== X-Gm-Message-State: AMCzsaXekyfmCtXknNo65T4HD9D9H/yVEx/N+KuwfFzCOm/Ypq/c0/9t Q/3WWFzSMgO4CDov5Pm6lywYg+eQSkKPR5YMyd1nRw== X-Received: by 10.129.106.133 with SMTP id f127mr2482262ywc.217.1507973835694; Sat, 14 Oct 2017 02:37:15 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.130.3 with HTTP; Sat, 14 Oct 2017 02:37:15 -0700 (PDT) X-Originating-IP: [193.77.148.136] In-Reply-To: References: <20171013081056.GB18718@mathematik.tu-darmstadt.de> From: Andrej Bauer Date: Sat, 14 Oct 2017 11:37:15 +0200 Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Homotopy Type Theory Cc: Univalent Mathematics Content-Type: text/plain; charset="UTF-8" > In our recent work on intrinsic > syntax of Type Theory we present a typed syntax that never refers to > preterms. In this framework theories with coercions cannot be expressed > and the syntax is the initial algebra of the corresponding notion of > algebras. This is quite cool, but I'd just like to point out that there are levels of abstraction, some of which cannot be ignored. At a very banal level, we need to know how to convert concrete syntax into abstract syntax. At a slightly less banal level, we have to admit that preterms (expressed as abstract syntax) are unavoidable. An important aspect of type theory revolves around making sure that the thing written down makes sense. The "thing written down" is a preterm (something that survived parsing but has yet to be type checked). There is also the question of breaking the vicious circle: we express type theory inside type theory, but where did the original type theory come from? I think it is quite reasonable to take the possition that type theory is primitive, but it is also equally reasonable to take the position that one should analyse how type theory arises from a more concrete setup, for instance, there is some value in knowing that the syntactic models based on concrete syntax are initial for type theory. With kind regards, Andrej