From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a19:98d3:: with SMTP id a202-v6mr88744lfe.32.1527677606820; Wed, 30 May 2018 03:53:26 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:d7db:: with SMTP id q88-v6ls3802060lfi.10.gmail; Wed, 30 May 2018 03:53:25 -0700 (PDT) X-Received: by 2002:a19:20ce:: with SMTP id g197-v6mr90572lfg.34.1527677605880; Wed, 30 May 2018 03:53:25 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527677605; cv=none; d=google.com; s=arc-20160816; b=y8Mptlqxt8xZOVkBe30cRZhn4O6ITzEF2OFT76Hmotv4bORxqZe3kRvXHTzYeW8yf3 XjBGYB57shhANN+22WOrgShWGWz4JtsgdXjVFrjjJp58T+UuzbW0ftpCDqFBxT1ySnGF W1gl6NueAtJbeey9bblS5OcOuimPfHOs9F7Yx5nBq4WZYrSf/zOTh3gCzuggq9BRSboR fytiwAJovx98af0NKCh1wwF7V2dJGW9jxvJm0YnA5nE1xq8u63/Iqn1HY+I0JZpu6JEp wE1hpV/fuDaBf9T1bHLOibRL8gN0+h8QoBIfAqH1NWMTP4BqltoazSe3eO/NxvFdSDjg ZWgw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature :arc-authentication-results; bh=96Ha1hM1TG/isVBzbZa/QLRDRhFopaSep6FLALtLmVI=; b=ecSNmZnA1KuuLW5cbqkG1R8c4zLjmOAaAhBTwzc4SCCwxyUhAJgMDcfx8R2BHOgZt1 rngDrxRlK2HUy9+TFAV0hzP0QCvCSenyy2QlCQu83mfHUOpl/1ePNGAGT3JX3CV9Mn2U i1NmIJbW1YyG7wBu3l2nXH63V096jH/Mpth3FZMW/uL8/vod0PQkflMKs6QLVmgKeAy7 97UKrVr2nzA3YmkXd3zrScX9TkEA5hygD19hfBb4ZSSykramQRXKD2wan5K7KxKNzS2s nXR/ZiGTKN0ojFl25VV88mTiaTDXNq9dkqcS/k8MVgadVu+wnHYMzVd+eyA2gBzQsJwA 1pgQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=vfUMEhkc; spf=pass (google.com: domain of axh...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) smtp.mailfrom=axh...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm0-x243.google.com (mail-wm0-x243.google.com. [2a00:1450:400c:c09::243]) by gmr-mx.google.com with ESMTPS id i26-v6si1656913ljj.2.2018.05.30.03.53.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 30 May 2018 03:53:25 -0700 (PDT) Received-SPF: pass (google.com: domain of axh...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) client-ip=2a00:1450:400c:c09::243; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=vfUMEhkc; spf=pass (google.com: domain of axh...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) smtp.mailfrom=axh...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wm0-x243.google.com with SMTP id a8-v6so46960886wmg.5 for ; Wed, 30 May 2018 03:53:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=96Ha1hM1TG/isVBzbZa/QLRDRhFopaSep6FLALtLmVI=; b=vfUMEhkcfNhx3rJAw1gG/sY8XjOm7WwcdAzrwLgP76CzzDH43BmaQULxcmruZ1qTHz IoEzX7TFo/MYGZVlF678Wd9QDZi1kYeceyv7Zv3Q2Jb+5j8j/E3MvqPKsd/sMdJOMlUd 8ImGsSn0TuEaGfoYW1xcXJLcJGHhGLxD/7pziswQ1gJaQE6cRIput+fNQDrThxIEx70v jtHbB04dc3CT5N6kbPFHEbi0dpkFMpiZkAVoRgTfAiguGxg4JEMfNuFbBdEpduXjFiXi nOYSGbdiIYNLwUUS5f7bTPWZwF+f+j1yNju4MSXn3Ev5mkqZFRkTNJMdTpiWruBGQ0fL ucDA== X-Gm-Message-State: ALKqPwdT3v1SwbuAW2Yox6cYy4Nh5tupO8O8r90QyAbtHC6ZnBKzaaoK 75XUSkECwZTznAdUu2dWALg= X-Received: by 2002:a1c:800e:: with SMTP id b14-v6mr1064197wmd.83.1527677605506; Wed, 30 May 2018 03:53:25 -0700 (PDT) Return-Path: Received: from [192.168.0.21] (cpc86287-nfds17-2-0-cust224.8-2.cable.virginm.net. [86.8.41.225]) by smtp.gmail.com with ESMTPSA id l10-v6sm15069875wrm.29.2018.05.30.03.53.24 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 30 May 2018 03:53:24 -0700 (PDT) Content-Type: text/plain; charset=us-ascii Mime-Version: 1.0 (Mac OS X Mail 11.2 \(3445.5.20\)) Subject: Re: [HoTT] Re: Where is the problem with initiality? From: Alexander Kurz In-Reply-To: <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> Date: Wed, 30 May 2018 11:53:23 +0100 Cc: Thomas Streicher , Michael Shulman , "homotopyt...@googlegroups.com" Content-Transfer-Encoding: quoted-printable Message-Id: <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> To: Thorsten Altenkirch X-Mailer: Apple Mail (2.3445.5.20) > On 30 May 2018, at 10:37, Thorsten Altenkirch wrote: >=20 > On 30/05/2018, 10:33, "Thomas Streicher" wrote: >=20 > That categorical syntax and ordinary syntax are isomorphic is just a > purely syntactic result allowing one to replace correct algebraic > syntax by one more accessible for the human mind. >=20 > For the human mind accustomed to the separation of collections and predic= ates as present in conventional Mathematics. I think the problem is not just one of being accustomed or not.=20 It is crucial that informal mathematics is untyped. The untypedness is what= makes it flexible enough for practical purposes. Formalising mathematics i= n a proof assistant is hard work. And to a large extent this is due to the = fact that everything has to be typed.=20 If we ever want to get mathematicians to use proof assistants as casually a= s they use latex, the problem of untyped vs typed mathematics needs to be s= olved.=20 Alexander >=20 >=20 >=20 >=20 >=20 >=20 > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment.=20 >=20 > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored=20 > where permitted by law. >=20 >=20 >=20 >=20 > --=20 > 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.