From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x239.google.com (mail-oi1-x239.google.com [IPv6:2607:f8b0:4864:20::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 97596633 for ; Mon, 27 May 2019 02:33:48 +0000 (UTC) Received: by mail-oi1-x239.google.com with SMTP id k63sf3202640oih.15 for ; Sun, 26 May 2019 19:33:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=4PKhAl6yOG8RqVQSc+pEbIJqCZR+JLCjllmmgaHwCCg=; b=QTYTazDxLSkrQxPBBikU7m3Au+yOA8/JuwOBI7G3P+m6StTS5Qxnt0zs7lDnlqgVLi ax1AI4iUrBWk9OzgDR4NHOc5iYrLaoMHQavTmK/2h2tBfwNhmXbkME8FbNkK/hDHahJk PVNxwOhFneiBgMMklDETtE05y+1OCS2IRZk7+JJzStRtreAOx6QDx8DWHfuIPc54YW92 NN+WDwyEsioXnbWT9Kh1BEWIghPmA9JYltfoeYrtCyYGTHeBeA8xmYhh8LiMmDMuE1El IJBcUNGt3Nak/N8wEfGZP51wCTluOi7C+/Owb+wbz7vCXE462X3dJXmU4cPS/05/1hNz KjJg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=4PKhAl6yOG8RqVQSc+pEbIJqCZR+JLCjllmmgaHwCCg=; b=oSP6dmsZBwULbDSJbJAvlFTmEwIsUOszpqNj0+sg1pJjGxUSldXY52o/In5CC3cTuH GLB8QaJQTBpJkua1z2siF2OV7kdiAxhEGkO/hu0OZ8qBvUwNZNUCrMsnU5lGAeix9Ms3 3xe6ZDTdeMNDPIqbxW1/cyM0iTzEMswOH/bXayRViD5d1/FGsBfgX8gZxqr8Alcdf5EP ABzOwhVI4pJP5x3RRvZFqIfJ7bwDv5Gth9nckgxiGYFT62zbfLyeJA/VdBW6Cr1H47B9 kZrk0oeEfWMdyPtKUqaPEklBXZ1v2zhfgv5utN5QB1yjsphBkZXNKVAMHLXjAfmY4vgW 6xcg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=4PKhAl6yOG8RqVQSc+pEbIJqCZR+JLCjllmmgaHwCCg=; b=UMFYPuvowxbCxqWqlsiJ7l47xCLL3fzAd1yPs4nReV2zpn5PmHmG3MLygv3CzKBPp+ wvSGLlwoysPDcrYM0MztNLLIwy1LUpfo/F0MLbwD978bz+GmSLbOHSglYrFuWgI531Yd 3+93YdD4zkxa7rCjFLOe7F64fjs1FaoVgQw5JSLLOTnBc8fFP7GKfx3acEf/oL3hTtNs pAzSmbCz0b05026ws/T9gJGGbCTnzq4peoQFt5LeqwXnTT0paE270o4HS3Mm9EGP2DR0 hfPBBvakM7MjNCEG/JPQe2ttUFlx3k5bjQvL/DnjL10VkGTifcvUMiZ72pf0Sy0hz0Me VEVA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWPJ9eJ86saa+WikrYJTQeXHVe2aPy6hd2+zgY6BCo13y+GN6Ht /gwS7dx6hL4/jUDyhDPcncE= X-Google-Smtp-Source: APXvYqxAoZzIQsXOHtdUyfkWeSEu07bVq7JCmrMECxzbBNms+WD2Vx4ltcqwwxdmI4wVz5eBbl/Jaw== X-Received: by 2002:a9d:1405:: with SMTP id h5mr44749735oth.118.1558924426640; Sun, 26 May 2019 19:33:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2c21:: with SMTP id f30ls2677236otb.12.gmail; Sun, 26 May 2019 19:33:46 -0700 (PDT) X-Received: by 2002:a9d:2f67:: with SMTP id h94mr42569278otb.85.1558924425955; Sun, 26 May 2019 19:33:45 -0700 (PDT) Date: Sun, 26 May 2019 19:33:45 -0700 (PDT) From: "Daniel R. Grayson" To: Homotopy Type Theory Message-Id: In-Reply-To: References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> Subject: Re: [HoTT] doing "all of pure mathematics" in type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1623_1276088037.1558924425230" X-Original-Sender: danielrichardgrayson@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_1623_1276088037.1558924425230 Content-Type: multipart/alternative; boundary="----=_Part_1624_233093019.1558924425230" ------=_Part_1624_233093019.1558924425230 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Sunday, May 26, 2019 at 12:00:21 PM UTC-5, Kevin Buzzard wrote: =20 > > ... But looking at=20 > the things he formalised, he was doing things like the p-adic numbers,=20 > and lots and lots of category theory. I am surprised that he did not=20 > attempt to formalise the basic theory of schemes. > UniMath was formed from Voevodsky's Foundations (see=20 https://github.com/UniMath/Foundations ) and some formalizations based on it by other people, starting with=20 Benedikt=20 Ahrens and me, and continuing with many others. In particular, the =20 formalization of category theory began with Ahrens' formalization of the=20 material in a joint paper of his with Kapulkin and Shulman, see=20 =20 https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/READM= E.md , and has been continued by other people, not Voevodsky. Voevodsky was probably too busy writing his papers on the semantics of the= =20 system to turn to formalizing the basic theory of schemes. For a while he said he wasn't=20 even interested in formalizing his proof of the Milnor conjecture, because he was confident it was=20 correct. Then later he said, in a talk, that it would be important top find a constructive proof of the Milnor=20 conjecture, and to formalize it,=20 pinpointing a particular argument due to Merkurjev and Suslin as being=20 non-constructive, see the remark under the entry at=20 =20 http://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#Uni= Math-1 I also remember, perhaps in early 2014, that he told me he was thinking of= =20 formalizing the definition of scheme (or maybe variety) so he could talk about it at a forthcoming talk, but he= =20 never did that. Eventually UniMath should have the theory of schemes in it. By the way, to go back to your original question, I think there are no=20 "pain points" in formalizing traditional mathematics in UniMath. The pain and challenge seem only to=20 come when generalizing traditional facts about sets so they apply also to types that are not assumed to be sets. =20 For an example of that, see Peter Lumsdaine's proof of transfinite induction into a family of types= =20 at =20 https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/WellFo= undedRelations.v#L208 or see our proof with Bezem and Buchholtz that the type of =E2=84=A4-torsor= s=20 satisfies the induction principle into a family of types that the circle satisfies, at https://github.com/UniMath/SymmetryBook/blob/master/ZTors.tex --=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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/d57bb2de-ff98-484b-8bc0-9c3f31620a47%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_1624_233093019.1558924425230 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Sunday, May 26, 2019 at 12:00:21 PM UTC-5, Kevin Buzzar= d wrote:
=C2=A0
... But loo= king at
the things he formalised, he was doing things like the p-adic numbers,
and lots and lots of category theory. I am surprised that he did not
attempt to formalise the basic theory of schemes.
=
UniMath was formed from Voevodsky's Foundations (see=C2= =A0


) and some formalizations based on it by other people, sta= rting with Benedikt=C2=A0
Ahrens and me, and continuing with many= others.=C2=A0 In particular, the=C2=A0=C2=A0
formalization= of category theory began with Ahrens' formalization of the material in= a joint
paper of his with Kapulkin and Shulman, see=C2=A0
<= div>
<= br>
, and has been continued by other people, not Voevodsky.

Voevodsky was probably too busy writing his papers on = the semantics of the system to turn to
formalizing the basic theo= ry of schemes.=C2=A0 For a while he said he wasn't even interested in f= ormalizing
his proof of the Milnor conjecture, because he was con= fident it was correct.=C2=A0 Then later he said, in a talk,
that = it would be important top find a constructive proof of the Milnor conjectur= e, and to formalize it,=C2=A0
pinpointing a particular argument d= ue to Merkurjev and Suslin as being non-constructive, see the remark
<= div>under the entry at=C2=A0


I also remember, perhaps in= early 2014, that he told me he was thinking of formalizing the definition = of scheme
(or maybe variety) so he could talk about it at a forth= coming talk, but he never did that.

Eventually Uni= Math should have the theory of schemes in it.

By t= he way, to go back to your original question, I think there are no "pa= in points" in formalizing
traditional mathematics in UniMath= .=C2=A0 The pain and challenge seem only to come when generalizing traditio= nal facts
about sets so they apply also to types that are not ass= umed to be sets.=C2=A0 For an example of that,
see Peter Lumsdain= e's proof of transfinite induction into a family of types at
=

or see our proof with Bezem and= Buchholtz that the type of=C2=A0=E2=84=A4-torsors satisfies the induction = principle into
a family of types that the circle satisfies, at


--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/d57bb2de-ff98-484b-8bc0-9c3f31620a47%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_1624_233093019.1558924425230-- ------=_Part_1623_1276088037.1558924425230--