From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a25:e89:: with SMTP id 131-v6mr6712581ybo.17.1528183808156; Tue, 05 Jun 2018 00:30:08 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:9b90:: with SMTP id s138-v6ls62000ywg.8.gmail; Tue, 05 Jun 2018 00:30:07 -0700 (PDT) X-Received: by 2002:a81:2f08:: with SMTP id v8-v6mr6654173ywv.140.1528183807479; Tue, 05 Jun 2018 00:30:07 -0700 (PDT) Received: by 2002:a0d:cb4b:0:0:0:0:0 with SMTP id n72-v6msywd; Fri, 1 Jun 2018 02:55:47 -0700 (PDT) X-Received: by 2002:a25:507:: with SMTP id 7-v6mr3039752ybf.46.1527846947338; Fri, 01 Jun 2018 02:55:47 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527846947; cv=none; d=google.com; s=arc-20160816; b=H/mP+iNTDzd31MnWxe5XKpQMkm99s8ixUeHCaFHp/ZULjz3KD4DTRFbKyq+Mpu0jd4 GBt2+vyW4KPQaF+z+d9/zXxtqNRAee78iuTErOQndRisF2fkwJkAV8g0dshSTMgATmpF 0vktOxpz0lYr/w+uh3ICOdGYEWWxwc9dYZpxHol0og/lLfQBsRQF0seCCmwBWc2qzlBX TkzbBKIFIeToc/oHFvTrzp2sESR2zpUk3Bxii0hYYC8KtpalZuH0wHOLFvXyKeT52fqx MxWLOAWupDzzRtLSPyQmfC9mxwQs3vKyHmVszyG/g1EwifHBbNQYmfcB7CzWDwQHE3Z+ HQJA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:cc:to:subject :arc-authentication-results; bh=BN9bhGzHoEDsalu6XztjhQnjLjZCGNaHtlqOrvgwQtg=; b=hN0L0tfx0LVal6Bl/bMIiQVWiD4qNXNMkD8O2B7fcQlzwKVv8xoqFX6X3iDy8D1MtA /i5HLO1Hh2/EAnMzoae5LXP19cmOg1+o9oYMqNB6DaykYQ6V2s2vVz6PUkH+3j9strbp vl9zNqqUDBGjiD4Bd8Ybt6m6mWPsq3qj/cxnvG77YLCiwAJSENnfRPoc0l1GmC1Lpc93 Jne+S7dhwZ67V2Lv37K3u6w7xYlEuQuMjaBC0ajFo8i6hSmQgyzs7LZ3BJ3+8vWalE0P B+5EvVEHvgDjYLL+9h6X3EJxwS1Hh8W/YA9MjsfnRSaaNv5L5YjYbPSeBnB1nXvlha7g IotA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id v185-v6si441687ywe.0.2018.06.01.02.55.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 02:55:47 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun61.bham.ac.uk with esmtps (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256) (Exim 4.90_1) (envelope-from ) id 1fOgme-00080s-Nv; Fri, 01 Jun 2018 10:55:44 +0100 Received: from dynamic200-250.cs.bham.ac.uk ([147.188.200.250]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128) (Exim 4.90_1) id 1fOgme-0002ZY-Du using interface auth-smtp.bham.ac.uk; Fri, 01 Jun 2018 10:55:44 +0100 Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Alexander Kurz , Michael Shulman Cc: Thorsten Altenkirch , Thomas Streicher , "homotopyt...@googlegroups.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> <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk> <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com> From: Martin Escardo Message-ID: Date: Fri, 1 Jun 2018 10:55:43 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.8.0 MIME-Version: 1.0 In-Reply-To: <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128 via 147.188.128.21:465 (escardom) On 31/05/18 20:02, Alexander Kurz wrote: > I am interested in this question of translating the untyped stuff we write on the page into type theory. > > To give a concrete example of what I am thinking of as untyped, but nevertheless conceptual and structural mathematics, I would point at Tom Leinster’s elegant description of the solution to the problem of Buffon’s needle, see the first paragraphs of the section “What is category theory?” at https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html > > I call this argument type free because I see no obvious or canonical way to make the types precise enough in order to implement the proof in, say, Agda. Even if this can be done, it is still important that mathematicians can discuss this argument first without having to make the types precise. So there will always be mathematics outside of type theory. I don't understand why you call this argument untyped. Do you feel that a formalization in set theory, which is untyped, would be easier than a formalization in type theory? How is untypedness helping with this argument? Martin