From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a6b:1e90:: with SMTP id e138-v6mr2290370ioe.79.1528185148153; Tue, 05 Jun 2018 00:52:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:eb15:: with SMTP id h21-v6ls518803itj.4.canary-gmail; Tue, 05 Jun 2018 00:52:27 -0700 (PDT) X-Received: by 2002:a24:62ca:: with SMTP id d193-v6mr4083480itc.21.1528185147401; Tue, 05 Jun 2018 00:52:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528185147; cv=none; d=google.com; s=arc-20160816; b=zlwJd7P+/0EHmWE/5VmoC7PwTheCDMNffCesZRjl9gqMdOeRUMDJPmaxs2x5nNQWg+ olrIOi6kRUCpIo61TB2CorP/WKhtmd8linvqc2VIXOi0RepQzUuOO4oMdy5A0l5d/Rx+ 9JxcZK9odwWqmYHGFYJ0bKDTv1Ojp8p56iDpzSEcyFFPElGngshzsowUznDul163uXYd VVuyt1734ihXotvMRV1WG/pg7lkPS9a/C5HTiJxz0aaQK//oYbeAaioakaPr7UH2A/p+ CIczCgf7wCyVauVbt9i0PUv35LEwoCgY64bB62vIAc8joOYfh5LuZoL4ngNWuwy33JLM TQfQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=7dU4S6RmxaFQ/FrOxqmlMWBmLaMk5iOXZyHDTm485pY=; b=PGOSFoAJwcETrD4GI1HcNkOgTc1XJ0X3kXLVjBPJWM0cWmG+Yu8G/JpEah9t2+LTnM mNLLtXUqeXW1M74Z5gVx8A1UxD27J0islT3IhSodohGczF1iFWeZrArj8+DFwN2Gah+G xYOarRI9vdQRyMxBqR1gQ0xlU61NMTZ3Xjq/434q+kieGQrxrk8sxT2US/eDwzLZkhgR kxmb7fFnAmI9ybuC8xgh0kKuyc2oHoDOXZXlgnOX8+ls+GHtRZNudyg3FavGnkteNKxN HoCCZYJMj0wo/biw9daUOwne/6cf/xM09D/fopN1c/Ut7yifkqxcCe2Tl+GFXQn9+MSr q9xw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=JhpyaiOu; spf=neutral (google.com: 2607:f8b0:4001:c06::235 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-io0-x235.google.com (mail-io0-x235.google.com. [2607:f8b0:4001:c06::235]) by gmr-mx.google.com with ESMTPS id r1-v6si1451571ioa.5.2018.06.05.00.52.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Jun 2018 00:52:27 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4001:c06::235 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4001:c06::235; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=JhpyaiOu; spf=neutral (google.com: 2607:f8b0:4001:c06::235 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-io0-x235.google.com with SMTP id g22-v6so2225221iob.7 for ; Tue, 05 Jun 2018 00:52:27 -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 :content-transfer-encoding; bh=7dU4S6RmxaFQ/FrOxqmlMWBmLaMk5iOXZyHDTm485pY=; b=JhpyaiOu6+qI3n5ycND8EkPjvIMsjFq7A4cqniq+eiky5v9vVFlVEc82rKrwi41CPe Cheb01uTosavqr4IVQrhrNLD4nQbTfPfjw4As58GE2sWrz4TyPeddPRuhnDtuROPkwqo aMrhtn7rp/QCwwkKVgifErKG1IH/wkhF3o5tqNt1p/4TBo3++MBGYewgVeRG2c7B/AD7 aJMZQUJQSSwQbxQpSR4kTbhxvnINxw0qihLIdPe5CKlpahckpl/zrMi0PTXYuk3xpKOX E5iTdqwV69rRT7wUiWYtK961Hm9Rtir78P4PsZcOGut5Bk9rmxhqJEsNuMKGkZio6t9v YORQ== X-Gm-Message-State: APt69E3E7V1PHXnippH4eUxP2RsEpYrCtxAYotBhf0AddrGkk0yTnOU9 e79fK/u7mH6DxUu1Rnb1JdxDhVrjqntbZLHNFECk3q+d X-Received: by 2002:a6b:106:: with SMTP id 6-v6mr24236903iob.175.1528185146865; Tue, 05 Jun 2018 00:52:26 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:ac0:acd3:0:0:0:0:0 with HTTP; Tue, 5 Jun 2018 00:52:26 -0700 (PDT) X-Originating-IP: [131.220.249.211] In-Reply-To: <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> References: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk> <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> From: Andrej Bauer Date: Tue, 5 Jun 2018 09:52:26 +0200 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Alexander Kurz , "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear Alexander, On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz wrote: > > It is crucial that informal mathematics is untyped. The untypedness is wh= at makes it flexible enough for practical purposes. Formalising mathematics= in a proof assistant is hard work. And to a large extent this is due to th= e fact that everything has to be typed. > > If we ever want to get mathematicians to use proof assistants as casually= as they use latex, the problem of untyped vs typed mathematics needs to be= solved. I think you made there a coiple of intellectual jumps. In order for your statements to have some weight, you need to consider the following questions: (a) What if formalization of mathematics in existing proof assistants is hard for some reason other than typedness? (b) Most proof assistants that have a large user base are typed. Is this is a big conspiracy on part of the designers, or could it be understood as evidence that typed proof assistants have a certain advantage over the untyped ones? (c) You offer LaTeX as an example of good design. I beg to differ. (d) Informal mathematics is very obviously typed, as witnessed by the fact that authors are always carefully explain the types of various symbols they use (or rely on the culturally accepted notations). The Buffon needle example presents absolutely no obstacle to typing. Perhaps you are mixing up *informal* nature of human mathematics with untypedness? Formalizing Buffon's needle requires a great amount of precision (what is a curve? what does it mean to "throw a needle"? how do we cuunt crossings when there are infinitely many?) which is unavoidable so long as we subbscribe to the mathematical method. Typedness has nothing to do with this fact. With kind regards, Andrej