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-ot1-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ec431089 for ; Mon, 25 Feb 2019 15:03:45 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id b21sf4997016otl.7 for ; Mon, 25 Feb 2019 07:03:45 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=YPXlkPLY9Cp/JGGJQzEhnOYSa3lbIFRg/EnHkvz5j/E=; b=AJFjD+Gzok+gDmo18LJCD6CyG18Z9mC3nEaNRDJZt4N3GlAP+coe/5cB32LpGsQtQj SdtcZvoK5b9yrLentyd8b7VfN49Yh+iEXFfjndcTn0CcqZjETFU2Hy3GpYc0+F+tc10D MD3+iA8rvwpTv6Uz5mgVIy6whyMfaggiWeE5oWfKFIHxzaV/fIEhoQTI/VY2CPlQgyIp Jvv2/8/YJG+BojoT1jCDpgKeDg2YsjpVv/nCu6dXzPL3sYx2zidJiGOA71180c4LR5Jb nXTfE28d6lEExr74L+Ic5Dc3Q8+iq1vqFuuac4337vCZaspjevB6CkQuGVBm8527dj// 8TRA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=YPXlkPLY9Cp/JGGJQzEhnOYSa3lbIFRg/EnHkvz5j/E=; b=mBgUUJ40tb9r/7NBtUWT/G2TXFh2br4wpKqPtp5Dsa1Ej1MQWnQ142hwrAp0Lhk6FU oowvZNTq9XYQ+WJAPrclcY3z0JKn9eLzEjqJIq0GF4wkKCbwYaHizA7CgARtxVEQn1bk 6/rnxY/mNVpPfc6q62iQTF0NQ2X0iMLX6rbaW11nAKx2AW7hU8nvqKsDjGQdJpnohkUt +5QwvfCJkYW2eK/EDitOfGMkhkhWbizdljCoF+/V7AEQyNp07ZGYYChtMXyWCRhAaO9s AH+OqumknME3TYugQx3j9uycfw1czB0gpHCJSaBGxf9s9RyDAA2kYL9kEJzo+sK6v0cA 2I3Q== 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: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=YPXlkPLY9Cp/JGGJQzEhnOYSa3lbIFRg/EnHkvz5j/E=; b=IHKARksWCgpGFhYZcCjOC/+itn7FyihT1florTTOiB5OqgfXqgo7npDQmgykuoEsuu RCxm/3f7vwdTS3EbMHE0vYNx6gqVuuYT7d16gNMOxZ82iYj6/lgdUaJnU2bWCXndYmEE QX2ep0Np2LhNc9JSbsBox1XQV1fzxQUg80WF03ff+yNRCgzfQHR77IJpeGcZZT4Dt2xD GPZcgANnrbOp8y1ga2ayqK4E+EWVTOvGyPbk8EA5d/hefytR2J45LDMe8bqQKUQkaN+P SGM6kCU9mqHjymadwygrCokLe+fUrUP1NoGlGHsiNH+Zw1DDPgyiPpsuz6FLfAy6kcao LSdQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYJZ3BXdS5r9BINwXFt1pt+SJcSM+7EdQinT8ZOWCJJfJpEy/uc cdmXTsmi7/j1OdmDCJ/f08M= X-Google-Smtp-Source: AHgI3IZwZiodYxUwwY/OLNcLRycFYlGxZOka8jpyj8PL5u9gYw5NqDciUzKOcNoysljR7AKZTd4aMg== X-Received: by 2002:aca:af91:: with SMTP id y139mr11725048oie.54.1551107023910; Mon, 25 Feb 2019 07:03:43 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:5dc1:: with SMTP id r184ls1093999oib.5.gmail; Mon, 25 Feb 2019 07:03:43 -0800 (PST) X-Received: by 2002:aca:fd91:: with SMTP id b139mr11517271oii.170.1551107023325; Mon, 25 Feb 2019 07:03:43 -0800 (PST) Date: Mon, 25 Feb 2019 07:03:42 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <58193e91-74b3-4207-8dc8-c67e41b55b93@googlegroups.com> Subject: [HoTT] Construction of the circle in UniMath MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_818_537950475.1551107022567" X-Original-Sender: UlrikBuchholtz@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_818_537950475.1551107022567 Content-Type: multipart/alternative; boundary="----=_Part_819_618149152.1551107022567" ------=_Part_819_618149152.1551107022567 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Some time ago (May 2014), there was a discussion on this list about=20 defining the circle as the type of Z-torsors. Dan had formalized in UniMath= =20 that this type satisfies the recursion principle for the circle, and Mike= =20 posted a quick sketch showing how to extend the proof to give the induction= =20 principle: =20 https://groups.google.com/d/msg/homotopytypetheory/hE1eY-v_Kes/bdSoAxC9224J We're now pleased to announce that this indeed works, with a detailed proof= =20 developed independently of Mike's sketch by Marc and Ulrik, and formalized= =20 in UniMath by Dan: =20 https://github.com/DanGrayson/UniMath/blob/circle/UniMath/SyntheticHomotopy= Theory/Circle2.v Definition circle :=3D B =E2=84=A4. Definition pt :=3D basepoint circle. Theorem loops_circle : =E2=84=A4 =E2=89=83 =CE=A9 circle. Definition loop :=3D loops_circle 1 : =CE=A9 circle. Definition CircleInduction (circle : Type) (pt : circle) (loop : pt =3D= =20 pt) :=3D =E2=88=8F (X:circle->Type) (x:X pt) (p:PathOver x x loop), =E2=88=91 (f:=E2=88=8F t:circle, X t) (r : f pt =3D x), apd f loop = =3D r =E2=9F=A4 p =E2=9F=A5 !r. Theorem circle_induction : CircleInduction circle pt loop. If the underlying type theory has propositional truncation with an=20 eliminator that computes judgmentally on the point constructor, then the=20 same is true for our circle, i.e., the 'r' above is a reflexivity path. We're working on a detailed write-up of the proof; you'll find a=20 preliminary version of this if you follow a link in the above formalization= . Marc Bezem, Ulrik Buchholtz, and Dan Grayson --=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. For more options, visit https://groups.google.com/d/optout. ------=_Part_819_618149152.1551107022567 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Some time ago (May 2014), there was a discussion on t= his list about defining the circle as the type of Z-torsors. Dan had formal= ized in UniMath that this type satisfies the recursion principle for the ci= rcle, and Mike posted a quick sketch showing how to extend the proof to giv= e the induction principle:

=C2=A0 =C2=A0 https://g= roups.google.com/d/msg/homotopytypetheory/hE1eY-v_Kes/bdSoAxC9224J

We're now pleased to announce that this indeed works, = with a detailed proof developed independently of Mike's sketch by Marc = and Ulrik, and formalized in UniMath by Dan:

=C2= =A0 =C2=A0 https://github.com/DanGrayson/UniMath/blob/circle/UniMath/Synthe= ticHomotopyTheory/Circle2.v

=C2=A0 =C2=A0 Definiti= on circle :=3D B =E2=84=A4.
=C2=A0 =C2=A0 Definition pt :=3D base= point circle.
=C2=A0 =C2=A0 Theorem loops_circle : =E2=84=A4 =E2= =89=83 =CE=A9 circle.
=C2=A0 =C2=A0 Definition loop :=3D loops_ci= rcle 1 : =CE=A9 circle.
=C2=A0 =C2=A0 Definition CircleInduction = (circle : Type) (pt : circle) (loop : pt =3D pt) :=3D
=C2=A0 =C2= =A0 =C2=A0 =E2=88=8F (X:circle->Type) (x:X pt) (p:PathOver x x loop),
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =E2=88=91 (f:=E2=88=8F t:circle, X t) (= r : f pt =3D x), apd f loop =3D r =E2=9F=A4 p =E2=9F=A5 !r.
=C2= =A0 =C2=A0 Theorem circle_induction : CircleInduction circle pt loop.
=

If the underlying type theory has propositional truncat= ion with an eliminator that computes judgmentally on the point constructor,= then the same is true for our circle, i.e., the 'r' above is a ref= lexivity path.

We're working on a detailed wri= te-up of the proof; you'll find a preliminary version of this if you fo= llow a link in the above formalization.

Marc Bezem= , Ulrik Buchholtz, and Dan Grayson

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_819_618149152.1551107022567-- ------=_Part_818_537950475.1551107022567--