From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a81:314e:: with SMTP id x75-v6mr4946750ywx.136.1528187861888; Tue, 05 Jun 2018 01:37:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0d:ddd7:: with SMTP id g206-v6ls3131813ywe.28.gmail; Tue, 05 Jun 2018 01:37:41 -0700 (PDT) X-Received: by 2002:a81:9f49:: with SMTP id w70-v6mr7942039ywg.146.1528187861133; Tue, 05 Jun 2018 01:37:41 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528187861; cv=none; d=google.com; s=arc-20160816; b=iKgdTEhwoRdYDYCHocI9qhM9cw6yjpc02w8vWo8HMxRg40O2wQYvQvl4HoxMqqul7l Bi61KYPCG+oUe7Hvv/KWeax80Q1u7ft7jny0eYRLIwbdfjPanXUTZbe7ImMCp+9Ixr25 gjaVbuI44VXIE6LVcXK5SyNoUHupJOLCqU6iVdWaFv9zxhmXDP3GS4wOOvKJCojqO5+X c/sagM82n7YeVO3NaOI5EkPBBCslvO513w+l0cqk7Gkj0Ch0A5Ah1TuUBULOg50DaTEl 7JFvlJz1otDIdnwNxgwZmIJDZjsG8C17FGfK7D1QvwbGR7hFYtnYf8qAtSeVCgWmqngk Zr7A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=i5c1n+/+3pt2ZK0WLtagYQY1Tnb1CBAtGyH+AxPQDsQ=; b=lfCeChcNY86tEk30Jg3fF79/+bgLl/VD9m95BLZyNcyMBPCx8IIEybV5axKdCQG6ze T7GowpJdrrTFDHMKVTdn+suwLyWwi12OjAuXFwGrMkkHbxuzbZfv3+LGqX1i2i4kmAV9 7rsAatq8Ee/BPloO0Mpoy71APVr7a6TYjjrWl5H23bLqD1RBQolu9/QwNgxxjEGAUA7i z1V3TOJGS33JbQHOqi7aBOWV0QkuKc0YvDHVomtN81RDMWX5wMhiQjbMK1H+48qKk2Yt Yp+4O2UAKCMyYmOk1Cey2QcTzwiLH4yjytUQare6Gcwgy3lvv3GdWg4shSOcjoKYaavW gH3g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=uq/bX9b7; spf=pass (google.com: domain of drobert...@gmail.com designates 2607:f8b0:400c:c08::22e as permitted sender) smtp.mailfrom=drobert...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ua0-x22e.google.com (mail-ua0-x22e.google.com. [2607:f8b0:400c:c08::22e]) by gmr-mx.google.com with ESMTPS id x4-v6si111560ybk.2.2018.06.05.01.37.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Jun 2018 01:37:41 -0700 (PDT) Received-SPF: pass (google.com: domain of drobert...@gmail.com designates 2607:f8b0:400c:c08::22e as permitted sender) client-ip=2607:f8b0:400c:c08::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=uq/bX9b7; spf=pass (google.com: domain of drobert...@gmail.com designates 2607:f8b0:400c:c08::22e as permitted sender) smtp.mailfrom=drobert...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-ua0-x22e.google.com with SMTP id f30-v6so1040783uab.11 for ; Tue, 05 Jun 2018 01:37:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=i5c1n+/+3pt2ZK0WLtagYQY1Tnb1CBAtGyH+AxPQDsQ=; b=uq/bX9b7pAGVux4TQrRZJVZY8lgVLWYltyxuxAH3tPVL/bFrKXSIRA5yxqdCgNUlOE ojd9FFH/3N3SqUn8Rx4DHOZ0dWTOU4qsBw+iIlXkk6BPSt7zPZyAe/696IMgFLz7xsL/ gw5xIjmQxT27VQuOcK3UNoW7OnYRuJrJLdozevHSdjfWWDHXvwF0QsUkcp9wM3eEmGuh MnzDLi/xGQ/trWGen7EfB3gOhFi3wHv1fFo0o+ZOlpMzpuSI3Hy47m+mOUej3qzuSMk4 gPT/wqrFG7NGhmYJZnePv+2b1FenkdCRQYGA66SC8UjEXmY3XcmgFJpB7bkAd1lZXBnO VyZA== X-Gm-Message-State: APt69E2sANiyOIfW3sSh5CMEbkjXuyVKo7AxDZsT9rNBAYr9pHMwaOyE V2ZJd588a6x+kYzUXzLAbc3GVT4DNu34R+uSH/A= X-Received: by 2002:ab0:d94:: with SMTP id i20-v6mr295414uak.67.1528187860761; Tue, 05 Jun 2018 01:37:40 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a1f:ac0e:0:0:0:0:0 with HTTP; Tue, 5 Jun 2018 01:37:39 -0700 (PDT) In-Reply-To: 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: David Roberts Date: Tue, 5 Jun 2018 18:07:39 +0930 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Andrej Bauer Cc: Alexander Kurz , "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable There is an... "interesting" discussion going on at the fom mailing list at present, the usual suspects included, about set theory-based proof assistants, which might provide either a source of entertainment or frustration. It is enlightening when considering what people think about typed vs untyped. Univalent foundations gets a mention here: https://cs.nyu.edu/pipermail/fom/2018-May/021012.html The 'ideal proof assistant' is described as being based on ZFC here: https://cs.nyu.edu/pipermail/fom/2018-May/021026.html Friedman proclaims he is completely ignorant of the issues and that he has never gotten close to getting dirty with details, but is happy to weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/021023.html The discussion continues this month here: https://cs.nyu.edu/pipermail/fom/2018-June/021030.html David David Roberts http://ncatlab.org/nlab/show/David+Roberts On 5 June 2018 at 17:22, 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 w= hat makes it flexible enough for practical purposes. Formalising mathematic= s in a proof assistant is hard work. And to a large extent this is due to t= he fact that everything has to be typed. >> >> If we ever want to get mathematicians to use proof assistants as casuall= y as they use latex, the problem of untyped vs typed mathematics needs to b= e 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.