From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.223.157.198 with SMTP id q6mr380785wre.13.1507978302998; Sat, 14 Oct 2017 03:51:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.223.145.226 with SMTP id 89ls936832wri.10.gmail; Sat, 14 Oct 2017 03:51:42 -0700 (PDT) X-Received: by 10.223.175.196 with SMTP id y4mr379871wrd.30.1507978302086; Sat, 14 Oct 2017 03:51:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507978302; cv=none; d=google.com; s=arc-20160816; b=tytZWfrIa23+kpfP1GLJQiG51hF0A1V1uFkSjBahPp3pNr+bQjMrwIT8dLV5zUdsue pmp2I5pS3PKc2d1rbQoMFZWWXENtEmc1pAmyWlthN0RCRPrLYkTgDNdBCrCUhSBvZSMh 8YVX2iMXzMd8J3GhZVrOhxtC6/pEJm0uiMEZWNtlpGWzZ+iVEh3x70bqVISbXPik5sXy nrbkD6XSpzR9+YVpyAX3IqGaq++QP6WhdMSnbzq/oHt4Gff/05bZ3QqUGbl5rRU7SE5t Q4Qh6dc36LYyCymOO12DvNY/HXRlMFFuwTO7BfVHd64zALys+elRuMF490VmD8a7jjz/ f6OQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:arc-authentication-results; bh=H+gbz9Xjsl84aYKu4j6hh61vfs0nhvQPHcOljyA1v7U=; b=wxCsX5wcXoDa3r/X8wey9sdpvpRG26YFqUwxPeur8Rc/bh0OD2BQb8RSpvWudEj1L+ fOVrBW9pOXFtGKbaip9AhtQlCgE0rRz3ifU68w5PhD+oGyGjP38TCcbNE27mpoehNEks x8bzpaQZHRN3pEwYK1cDUMXq/XgFrUe/VUyxfY2AFh5W5QKc71FJey8KQwUMlsYIcqtF u1Ez9Lw9e68Et5kq9PITci2za8ZJ3ZVFBBWevok15eHzpFVEbQPKfcINMvGsOMohc6z9 1KoGpCERDEKNSQzSkk7fp1gcELm34lEHIbWMouAaOZq1grp/6tt8Ye98t7iZq2OpCE0y 1fgg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of palm...@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) smtp.mailfrom=palm...@math.su.se Return-Path: Received: from mail-prod-route03.it.su.se (mail-prod-route03.it.su.se. [2001:6b0:5:1213:250:56ff:fe94:7fa1]) by gmr-mx.google.com with ESMTPS id b123si170119wme.3.2017.10.14.03.51.41 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 14 Oct 2017 03:51:41 -0700 (PDT) Received-SPF: pass (google.com: domain of palm...@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) client-ip=2001:6b0:5:1213:250:56ff:fe94:7fa1; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of palm...@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) smtp.mailfrom=palm...@math.su.se Received: from e-mailfilter01.sunet.se (e-mailfilter01.sunet.se [IPv6:2001:6b0:8:2::201]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail-prod-route03.it.su.se (Postfix) with ESMTPS id 3yDhGj1875z11Vh; Sat, 14 Oct 2017 12:51:41 +0200 (CEST) Received: from smtp.su.se (mail-prod-smtp01.it.su.se [IPv6:2001:6b0:5:1213:250:56ff:fe94:3d10]) by e-mailfilter01.sunet.se (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id v9EApdWS034600 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO); Sat, 14 Oct 2017 12:51:40 +0200 Received: from ebox-prod-srv09.win.su.se (ebox-prod-srv09.win.su.se [77.238.35.157]) by smtp.su.se (Postfix) with ESMTPS id 3yDhGg312Nzyqp; Sat, 14 Oct 2017 12:51:39 +0200 (CEST) Received: from ebox-prod-srv10.win.su.se (2001:6b0:5:1212:e1ec:c2f0:2866:8f67) by ebox-prod-srv09.win.su.se (2001:6b0:5:1212:50d0:4ddb:ba0a:ef45) with Microsoft SMTP Server (TLS) id 15.0.1263.5; Sat, 14 Oct 2017 12:51:38 +0200 Received: from ebox-prod-srv10.win.su.se ([fe80::f4f1:c810:506:d2e9]) by ebox-prod-srv10.win.su.se ([fe80::f4f1:c810:506:d2e9%16]) with mapi id 15.00.1263.000; Sat, 14 Oct 2017 12:51:38 +0200 From: Erik Palmgren To: Thomas Streicher , Andrej Bauer CC: Homotopy Type Theory , "Univalent Mathematics" Subject: SV: [HoTT] A small observation on cumulativity and the failure of initiality Thread-Topic: [HoTT] A small observation on cumulativity and the failure of initiality Thread-Index: AQHTQ4nwgCLv0+zxHEqBBEoh1ltBnqLhSssAgAACMQCAAYfhAIAAIpGAgAAEU4CAAC4rbg== Date: Sat, 14 Oct 2017 10:51:37 +0000 Message-ID: <1507978297241.98603@math.su.se> References: <20171013081056.GB18718@mathematik.tu-darmstadt.de> ,<20171014095243.GA29903@mathematik.tu-darmstadt.de> In-Reply-To: <20171014095243.GA29903@mathematik.tu-darmstadt.de> Accept-Language: sv-SE, en-US Content-Language: sv-SE X-MS-Has-Attach: X-MS-TNEF-Correlator: x-ms-exchange-transport-fromentityheader: Hosted x-originating-ip: [130.237.154.250] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Bayes-Prob: 0.0001 (Score 0, tokens from: outbound, outbound-su-se:default, su-se:default, base:default, @@RPTN) X-Spam-Score: -0.10 () [Tag at 7.50] T_RP_MATCHES_RCVD:-0.1 X-CanIt-Geo: ip=77.238.35.157; country=SE; region=Stockholm; city=Stockholm; latitude=59.3600; longitude=18.0009; http://maps.google.com/maps?q=59.3600,18.0009&z=6 X-CanItPRO-Stream: outbound-su-se:outbound (inherits from outbound-su-se:default,su-se:default,base:default) X-Canit-Stats-ID: 09UlmPDxc - 6e55274f7afc - 20171014 X-CanIt-Archive-Cluster: PfMRe/vJWMiXwM2YIH5BVExnUnw Received-SPF: neutral (e-mailfilter01.sunet.se: 77.238.35.157 is neither permitted nor denied by domain palm...@math.su.se) receiver=e-mailfilter01.sunet.se; client-ip=77.238.35.157; envelope-from=; helo=smtp.su.se; identity=mailfrom X-Scanned-By: CanIt (www . roaringpenguin . com) A simplistic suggestion for introducing names in contextual categories is to replace the assignment of length to contexts, by an assignment of a string of distinct symbols (variable name). The challenge is then to find a stripping/simplification function that could make the combinators more readable. Some preliminary explorations of this idea is in http://staff.math.su.se/palmgren/Named_variables_in_cwfs_v02.pdf ________________________________________ Fr=E5n: homotopyt...@googlegroups.com f=F6r= Thomas Streicher Skickat: den 14 oktober 2017 11:52 Till: Andrej Bauer Kopia: Homotopy Type Theory; Univalent Mathematics =C4mne: Re: [HoTT] A small observation on cumulativity and the failure of i= nitiality Andrej, you are right in the sense that the free model of a certain type theory T is not trivially isomorphic the syntax modulo. The late Voevodsky suggested this to be an important problem and Peter Lumsdaine has worked on it for some time. It feels a bit like a non-mathematical problem in the sense of being more organizational or CS like. But maybe one should think about ways to introduce variables in a systematic way for making categorical combinator based syntax more palatable. There is more hope this way get something than strating from raw syntax and how to tame it semantically. Thomas -- 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 e= mail to HomotopyTypeThe...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.