From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a19:ee0d:: with SMTP id g13-v6mr30993lfb.1.1528236747434; Tue, 05 Jun 2018 15:12:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:7e0b:: with SMTP id z11-v6ls5942516ljc.0.gmail; Tue, 05 Jun 2018 15:12:26 -0700 (PDT) X-Received: by 2002:a2e:7e05:: with SMTP id z5-v6mr33516ljc.9.1528236746525; Tue, 05 Jun 2018 15:12:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528236746; cv=none; d=google.com; s=arc-20160816; b=Kk9pR8QolIklVpktpe7exJLiNxHk4CeUmPQ8fBfQqUxW2LGWtJSDjZzeRF23yRIPlL 9G7xrcJyeIQaxIPI/I0JLrbZKzChg8LrlS9fMxt/LOknJhCjNQurb/Qg6Dgf4tFdxx+w QLtxYqSB1EPJii/Wj1BJqZs3qZKvMReZ8KRmd8wJflrNCawhJXWNy1+3aXficKmNAh+I jcbP1RyNUwQQbhVDPkMdeodzjyk1xaC/ZmcG3FgWrY294PSXrWXqPcMrihQ/UsLnhRV7 aG/jLb9LBfnhXOKGt9VvDRnClXe/ROOgB4ra74f1/14DW83oFYzFGHVei/MMdNzk7AWr M1jA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date:dkim-signature :arc-authentication-results; bh=q75C8O3FZW06AuudlCNL0AZMmtWq1x5o6eXvmlc+7gw=; b=Yw0eTugEHOo3duYF8bBo8VNXbQys1Tb4ZRY/xzH2ktAgH1lAF36lRSl/+AAbdHHkKN pGlScFinOp6WL2ec+44fCEYGCWGxzuXKgJtTUF7ADG56XSE+6Gl2RWMIM/QdFOtAlpkb Y7n8J14MBmEi0QT5fVsHvZzBip4ezOsfaVp8xLfFAEwhaYfkvsDpHt0xtdihLBTEiwAz sYjano359BBHmJo2Phiw3JKO2OKsM/SxuuNZqQI8w/+7Mp8UmOdXA3TKfHVpf4ItI+cc zgpDDQqOTNuhqR2toA1oD4JVkpqD14ErLn+o2eXEkZRhe3D3ELz6TULMVi4iiXqP+Y6s keKQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=jiRxOVf+; spf=pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::22f as permitted sender) smtp.mailfrom=rwilli...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-lf0-x22f.google.com (mail-lf0-x22f.google.com. [2a00:1450:4010:c07::22f]) by gmr-mx.google.com with ESMTPS id j127-v6si1950175lfe.4.2018.06.05.15.12.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Jun 2018 15:12:26 -0700 (PDT) Received-SPF: pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::22f as permitted sender) client-ip=2a00:1450:4010:c07::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=jiRxOVf+; spf=pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::22f as permitted sender) smtp.mailfrom=rwilli...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-lf0-x22f.google.com with SMTP id n15-v6so5972096lfn.10 for ; Tue, 05 Jun 2018 15:12:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent; bh=q75C8O3FZW06AuudlCNL0AZMmtWq1x5o6eXvmlc+7gw=; b=jiRxOVf+aoEWRySP97SvWFSgj7O1tugCIFwiqWMAmG88eLVoebeloRIZiLOWn7eLri hc8z/54y6flgt1FFDEVuz9vfW5Z0XAJOjRaqgpOonm2DDNbG4kF/Ck9bwH02IeEWsSgE 7xLZ8gn7wPygA6xFJFy6Bo7unr17OnyoxjU7yQqjDQXvqh28rUhMOsYbVrvvZdcO+PWm zz9wOTdJ0gBuLu3M7ccuYJC5oMA/uNiGR57yP7bkWiivOD7v/jfhyJNgWDzwiucwsV0B ImGIXJ5t6fzQwVm0VQT0Ud2PhquYZtTVlK3epOCTf3iryUEK2u8SmVsQFSqCX+ADFMj6 Gvng== X-Gm-Message-State: APt69E2TJFlvpcVxh5jOiwR3tYu9gKtRXaVe6QbKyo88uldXhgCnd2tj bFXNJCENsEnYoxXaidQD7b/GJQ== X-Received: by 2002:a2e:43db:: with SMTP id z88-v6mr272416lje.24.1528236746281; Tue, 05 Jun 2018 15:12:26 -0700 (PDT) Return-Path: Received: from localhost (109.247.202.84.customer.cdi.no. [84.202.247.109]) by smtp.gmail.com with ESMTPSA id o9-v6sm5313074lfk.2.2018.06.05.15.12.24 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Tue, 05 Jun 2018 15:12:25 -0700 (PDT) Date: Wed, 6 Jun 2018 00:12:23 +0200 From: Richard Williamson To: Andrej Bauer Cc: Alexander Kurz , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] Re: Where is the problem with initiality? Message-ID: <20180605221223.GA3309@richard.richard> 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> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.9.5 (2018-04-13) Alexander is getting a fair bit of stick! I just wanted to add a note of support to one aspect of the point I think he is making: there is a reason that languages such as Python are widely used by perfectly competent programmers who fully understand the benefits of typing. I share the view that there has to be something rather more Python-like in syntax than the currently available syntaxes if one is to have any hope of having something usable in practise by people who just want to get on with the mathematics. I am not convinced that this is a purely engineering problem as opposed to a theoretical one. (Yes, Python is not untyped either, but I think the point stands). On Tue, Jun 05, 2018 at 09:52:26AM +0200, Andrej Bauer wrote: > 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 what 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 the 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 > > -- > 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 email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.