From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1f:a182:: with SMTP id k124-v6mr657285vke.27.1528192017571; Tue, 05 Jun 2018 02:46:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:23c8:: with SMTP id c8-v6ls297513uan.3.gmail; Tue, 05 Jun 2018 02:46:56 -0700 (PDT) X-Received: by 2002:ab0:30f4:: with SMTP id d20-v6mr11380877uam.118.1528192016800; Tue, 05 Jun 2018 02:46:56 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1528192016; cv=none; d=google.com; s=arc-20160816; b=M5zAJf1V3VM/vvby50LTNILxGZIrT79LgTSJRcd51vvdu/rvNMlhr1v7h8sj8fETLr p2rP8M8FGcOhrVDfXdsLQivZUFtIIZxEprhDHZ6VU+jrXEr4vfHilRu9/IID4uGXicxp pH8hoJmS+gSbNIRF+qom2iUMDWMqtGUgXt5dUlAsee6UnPUjbYctrMTO9OdQ3rnB5p9Y zxZmwqfhdsw3pPxqkfdEF37bIhpJ/E1dQfZL6DNjfSL00zs38Vw1DMrS3jLPUQ7qCUFv W6eeFDx42TuRwwFBXlmffrw/J73I/P3zCMyW42+CIoUmgWs/mS/axJTZe0D5LMQT+Gft P8IA== 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=zRuR7nEA8xYUAvKDirjE9QgonMSC9dBcXLJP6hnNY0w=; b=znSsAC7KQ6pyfn4YtyXKcgLbKMaKfn21k8QKTzq4Wir0eztNoOVsVw6oUwjBpZVQ8x guTLWlYr/UHWOxfQwkF8qKbzUdP7ZktT3AVL1CIzyTKT6RZ5dcMxrmAU4Jgh9jFYO/PT Iw3oloQ9EdJe8hFuafAQuQBhxUFgZDrBqNjeavtZg8cpppviBl3kz4gReh4sZHyQHpVH IamXQFpOkt16IbbaY8MlsyiUS+m0D/zxI17Z4Kk8DYIoRcBAy9020IXKkcRaU1Zu+wvw kqXv7VtLX2AClziHW3U8ahFHOl+zTFE2mn+eR1CUWeJYtYyqfZkZYWTPaqqLxCYtG9Yv 5pmQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=nLQBK9s5; spf=pass (google.com: domain of gabriel...@gmail.com designates 2607:f8b0:400d:c0d::22b as permitted sender) smtp.mailfrom=gabriel...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt0-x22b.google.com (mail-qt0-x22b.google.com. [2607:f8b0:400d:c0d::22b]) by gmr-mx.google.com with ESMTPS id l142-v6si3227765vke.1.2018.06.05.02.46.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Jun 2018 02:46:56 -0700 (PDT) Received-SPF: pass (google.com: domain of gabriel...@gmail.com designates 2607:f8b0:400d:c0d::22b as permitted sender) client-ip=2607:f8b0:400d:c0d::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=nLQBK9s5; spf=pass (google.com: domain of gabriel...@gmail.com designates 2607:f8b0:400d:c0d::22b as permitted sender) smtp.mailfrom=gabriel...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qt0-x22b.google.com with SMTP id y31-v6so1671974qty.9 for ; Tue, 05 Jun 2018 02:46:56 -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=zRuR7nEA8xYUAvKDirjE9QgonMSC9dBcXLJP6hnNY0w=; b=nLQBK9s5ZciZ0cTGMGgRisXg7HGoEorKVN25xfKSHGvTRd/D4IlYoarlgZ8ozW8ZXJ CvdANQGwwvWw29mWM7zytiQznTIWAhIXMpBfsV5KG5FuYeio94RCUv0pCZz5nb4/PVs0 4m1+YLXTtSjsuX2F7hR2LJgQ/i+CO7IyCWtKpMI5lh0RbQ3z398OakQ9+dG+WhTnz0tq cwNdwrorboPMPNlULbbK+Dchv+/7vCtkvZEijKkEP12Z6+KUxo6a67QKiWBSjCRxPkVA +FBdGqTVIEF5n6dNyyBtfAmsRaNv6dfHGgbjQh52bfM+2Ln+qX5SvQje+Ul1sSZfA+88 BAww== X-Gm-Message-State: APt69E3AIuPJo7NAM+boSlWVv9Z8frCf8Cy4K4H+5VIzn+GBDyJtvXyA Yu0eGjNGSRLYDdXFA7meaT0Q/I6IzsjBEMnL/UE= X-Received: by 2002:ac8:2c37:: with SMTP id d52-v6mr23893819qta.108.1528192016456; Tue, 05 Jun 2018 02:46:56 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a0c:dd02:0:0:0:0:0 with HTTP; Tue, 5 Jun 2018 02:46:15 -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: Gabriel Scherer Date: Tue, 5 Jun 2018 11:46:15 +0200 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: David Roberts Cc: Andrej Bauer , Alexander Kurz , "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Conversely, I think that we could leave the discussion of preterms, typed/untyped representations, etc., out of the present discussion. Instead of trying to argue, a priori, which representations gives the more important initiality statement, we should be able to see, given initiality proofs for each representation (assuming that the proofs are as clean as they can), which ones contain the important, tasty bits, and which ones can be factorized from the others by adding a trivial or heavy-but-already-well-understood (parsing, for example) step. In particular, someone feeling that a given representation is "less important" from an initiality perspective should be able to prove themselves correct by deriving the result, while if they are missing something of mathematical interest it would be apparent in the difficulty to establish the result. (It is not clear that the absolute importance of various representation choices can be assessed solely from their initiality properties; but initiality properties is what is discussed here.) On Tue, Jun 5, 2018 at 10:37 AM, David Roberts wrote= : > 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 wrot= e: >>> >>> It is crucial that informal mathematics is untyped. The untypedness is = what makes it flexible enough for practical purposes. Formalising mathemati= cs 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 casual= ly 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 Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- > 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.