From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.176.73.44 with SMTP id z41mr4367049uac.43.1508110976381; Sun, 15 Oct 2017 16:42:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.176.22.18 with SMTP id k18ls3054520uae.15.gmail; Sun, 15 Oct 2017 16:42:55 -0700 (PDT) X-Received: by 10.31.92.132 with SMTP id q126mr4303332vkb.52.1508110975502; Sun, 15 Oct 2017 16:42:55 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508110975; cv=none; d=google.com; s=arc-20160816; b=z7o2IapJVeGu3o1HPrnKOjL210ZT/mTvcBDJ4SD64WAPPzt4CbK8hOFP9hUVtFd7U/ QfvCyGnFQ/I+x71ejtYOHLisobmo7w9asBC/Fq6o5ijUPF/nk7v+KINLAa45fzpsAonP 1YwFlWQ6bJFv5V1PtsAgq3+okUO9ldqJq0w8ppNB+3KScsDldtEA+1dTmjO1L7nEOZOV FW+q/At10QnUcEvhz5JFNodS2mA8+5sBU9AwO451kv3rY4GL26FmPhyMUbu/PW2V7q7C biXe6yg6lrP6OyzLKPOMqejhdlnsxm2w3NKTbA1JbknBl0Pb5z6o6EeWItKh6Yhc2a0F Dmww== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=SQ5FcKdA+HkVkWjMfZPcxnyYmAgksHf2Ygl2oFy+rx0=; b=Kjyd5JRADfbi5StNj3IrancDpl6FfgxP0p2Ed+cJajvbTh+8Cvs1hcwTb/Eixv4rLJ QOqdIkPDbo8gFUs/hHr97e0K+k4O0lizfbuaOwCgnJruS7JT3b1x/BersnAtHO1KUSzj Qo+qOCnzc9QEdA1gWFHXQvBlJPc+9fFcZO/Tz3oJ1COihz6SwpXcmaYBYGAiH7AIDjGg u/fdp+BpogFlINqBXywe2NKu7M2v3pXO0bbodFFLcNnT8DHSW6iHInAt0/nAJ5PcnQxJ q+bNxbAfjZzbomRNJFQBRPmHcL5bYlnc9NeRk15FhWSVcJ1nREJnvGRO2Y/hN30raTtz 0Zdg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=aiFx7IR+; spf=neutral (google.com: 2607:f8b0:400d:c0d::244 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-x244.google.com (mail-qt0-x244.google.com. [2607:f8b0:400d:c0d::244]) by gmr-mx.google.com with ESMTPS id h54si369865uaa.4.2017.10.15.16.42.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 16:42:55 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::244 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c0d::244; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=aiFx7IR+; spf=neutral (google.com: 2607:f8b0:400d:c0d::244 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-qt0-x244.google.com with SMTP id p54so1730150qtc.4 for ; Sun, 15 Oct 2017 16:42:55 -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:cc; bh=SQ5FcKdA+HkVkWjMfZPcxnyYmAgksHf2Ygl2oFy+rx0=; b=aiFx7IR+e+oVxe5JAE4fIfwJXplZ2z3CbKB5nViBbM3tPuqbe2NPjKrBsknuKKRgp7 NCPgEyWMW1VuaC6M1BsnwPDJHfrUuiG4Mgv6Pw4zgEmlEBo7PgE9wRz3jjGUfJ3ZxfIR FhvTrVikRVKS30Ij0HDSAfwd+ITPyNq6YUsJCLTQ+/F/H8f4k8p0yLGxVWc7C3n0AaKH K8NyUJkIjdltqbw4quTWq9OQwvLA98GkEMpkfnmM/ijMAoxKEAn9/yR6ZV/+f03bffRV 0FpIkpZIU7QIAgjveA5CnggPcGEd/lQcpaCM7HeHGiB+B0FhUCK7w/sb7Lifs0b1zkDO 8Q2g== X-Gm-Message-State: AMCzsaVsmjZu3rWfvIgrPji4Uzo+AhPHX7foRwgpABGrc0uqTYj5Snun XhN70cdwO6Nj42ZdjNHvm4/xQUc35yqjLowLfuZXfQ== X-Received: by 10.37.230.210 with SMTP id d201mt5190078ybh.118.1508110974776; Sun, 15 Oct 2017 16:42:54 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.17.130 with HTTP; Sun, 15 Oct 2017 16:42:54 -0700 (PDT) X-Originating-IP: [193.77.148.136] In-Reply-To: <20171014095243.GA29903@mathematik.tu-darmstadt.de> References: <20171013081056.GB18718@mathematik.tu-darmstadt.de> <20171014095243.GA29903@mathematik.tu-darmstadt.de> From: Andrej Bauer Date: Mon, 16 Oct 2017 01:42:54 +0200 Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Cc: Homotopy Type Theory , Univalent Mathematics Content-Type: text/plain; charset="UTF-8" > 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. I absolutely agree with Vladimir's insisting that actually proving good, robust, and general theorems about initiality of syntactic models is not only important, but also an open problem. We have *instances* of such theorems (with many thanks to you, Thomas), but no general theory. I would warn against repeating or spreading the opinion that such general theorems either exist, or are somehow not worth proving, or worse, that they are easy. And the reason for this is that I am working with Peter on them, and it's really not as easy or as boring as many would seem to presume. > It feels a bit like a non-mathematical problem in the sense of being > more organizational or CS like. Call it what you like. Isn't all of logic organizational? With kind regards, Andrej P.S. Why are we cross-posting everything between HoTT and Univalent mathematics lists?