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.2 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-x240.google.com (mail-oi1-x240.google.com [IPv6:2607:f8b0:4864:20::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b4d7c805 for ; Wed, 18 Sep 2019 12:00:32 +0000 (UTC) Received: by mail-oi1-x240.google.com with SMTP id p206sf2664090oib.14 for ; Wed, 18 Sep 2019 05:00:32 -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=j8zR5Ru6zDy34V+fhVV5U1DxuqGKRs9S1KIgJk3JMY8=; b=nn8pMj4Y+887Nz42qPYD3nxpXt4PUexRD6dUcEY9E95TakX7p6avdR3l34vI5qerZp UwyFo2pG+eAAE3yBByXcNOmPFezSfg5FkVDNJjMqcUOzvrDxsN3IRT8vYQXEZ0FTKuQD /B4SimwT1IfhQ0DCFGGJUVpdsHkyzoFw8wNB2M+oUBWXGzDgW5cVWvHn+jqhUW8N5NJG s/U9tb+RpzUqz94XTDq8C5x6ly5wLN9xMGJpKa4HGpg/scU1MF2mWfFEXdZy64ThJz7O 3crpOail7+uIybIBdzPNx7P94ocioGSEE2/1P6P4SrM9nKtS4M9TVe5XFx8xcYE0rnVD 2KkQ== 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=j8zR5Ru6zDy34V+fhVV5U1DxuqGKRs9S1KIgJk3JMY8=; b=Aft1esO/oVS9jA6QVpqW5o/ye3OnooIJo4AeVrXxTjpUHTkFk7UMBz3dEX4xdZPEGI GSiEQXyoY8zx/SoEGFP0YWSVnJYhnRsgH3SNbV87BRWL6fLEX8hnOuf1dDgS3K3y9nrj bRiQFRWMr83KeTmnYnhAUzB66upOrc1AlhkXxU6rtibWbigi/7h2H/KePTczXWQ/ylyY nrAuOwDC2Gims9O86sb52MaQGv1uBQSktEYc/5iYfT2dAFagZGDgZneBO8AkL00v5tkf I6+9CMoiZialN4wvL7pPu+Wf5eATuFJFhYM3qhiMpxdgrI85zBo+sxQkC1Bc3rWTPC+1 9vmA== 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=j8zR5Ru6zDy34V+fhVV5U1DxuqGKRs9S1KIgJk3JMY8=; b=FS+OtwA0FyTHnnubEObR20dqhqO0h2vX6//V2aUPaqSRcbK4brKh4e0YMuKswXg7Ez 8EfKM2qTdEF5OXg14MESw4DA4Vr4KF2wxfdXRL9C/OYeb4vOQnzqqGUYmRVp7Z9yPz/v QCZIlpV+YnQ1wohmwcp+mraCa46IHrC3nNDl3nIAZzJyBBAxcKuQ2px6OdmEeHyl1J2x kVoqe+fCz+TJYYEoG4LRFKiTKYgXBjKIWdqyqRiAWNATLiKwubqDK+vOb6xcY9Mx4REK Qwzbz6YjlYJMpaf39mPnRV7DOoyG0QXWqnQqxnkPhkklDHmPTnyrAbYAGpqvGyhjGHCz 9xkw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWAqDDw6QQGzQiP78qfxhCP/hRL8BUIWwtscKHucfGiiN80m3N1 oHs7UNL5x+jUWVDdHp+w3X8= X-Google-Smtp-Source: APXvYqxQ+raCx/ZSu8vbZDcRoAWmjlETiLiMy7pDPuWTspeKWp/DfHCnn6YCXxOtPQ34nJI7w2xvXg== X-Received: by 2002:a05:6830:1198:: with SMTP id u24mr2582836otq.117.1568808030925; Wed, 18 Sep 2019 05:00:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:bd44:: with SMTP id n65ls374962oif.6.gmail; Wed, 18 Sep 2019 05:00:30 -0700 (PDT) X-Received: by 2002:aca:d584:: with SMTP id m126mr1933167oig.74.1568808030375; Wed, 18 Sep 2019 05:00:30 -0700 (PDT) Date: Wed, 18 Sep 2019 05:00:29 -0700 (PDT) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: <6c150b9c-fba6-47c1-2a6d-975b90f64638@gmail.com> Subject: Re: [HoTT] Different definitions of Sn MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_3269_209704738.1568808029788" X-Original-Sender: andersmortberg@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_3269_209704738.1568808029788 Content-Type: multipart/alternative; boundary="----=_Part_3270_1352620414.1568808029789" ------=_Part_3270_1352620414.1568808029789 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Let me elaborate a bit on my answer. One might naively try to copy Dan and= =20 Guillaume's definition and write the following in Cubical Agda: Omega : (A : Type=E2=82=80) =E2=86=92 A =E2=86=92 Type=E2=82=80 Omega A a =3D (a =E2=89=A1 a) itOmega : =E2=84=95 =E2=86=92 (A : Type=E2=82=80) =E2=86=92 A =E2=86=92 Typ= e=E2=82=80 itOmega zero A a =3D Omega A a itOmega (suc n) A a =3D itOmega n (Omega A a) refl data Sn (n : =E2=84=95) : Type=E2=82=80 where base : Sn n surf : itOmega n (Sn n) base However Agda will complain as surf is not constructing an element of Sn.=20 This might seem a bit funny as Cubical Agda is perfectly happy with data S=C2=B3 : Type=E2=82=80 where=20 base : S=C2=B3=20 surf : Path (Path (base =E2=89=A1 base) refl refl) refl refl=20 But what is happening under the hood is that surf is a constructor taking= =20 i, j, and k in the interval and returning an element of S^3 with boundary= =20 "base" whenever i, j and k are 0 or 1. In cubicaltt we can write this HIT= =20 in the following way: data S3 =3D base | surf [ (i=3D0) -> base , (i=3D1) -> base , (j=3D0) -> base , (j=3D1) -> base , (k=3D0) -> base , (k=3D1) -> base ] The problem is then clearer: in order to write the surf constructor of Sn= =20 we would have to quantify over n interval variables and specify the=20 boundary of the n-cell. This is what that is not supported by any of the=20 cubical schemas for HITs. -- Anders On Wednesday, September 18, 2019 at 11:00:22 AM UTC+2, Guillaume Brunerie= =20 wrote: > > Hi,=20 > > We give a definition of S^n with one point and one n-loop by=20 > introduction/elimination/reduction rules in our paper with Dan Licata=20 > (https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can be=20 > implemented in Agda (so Kristina=E2=80=99s question can be formulated and= can=20 > presumably be formalized in Agda) but I don=E2=80=99t think we actually p= roved=20 > it.=20 > > Best,=20 > Guillaume=20 > > Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg >:=20 > >=20 > > Hi Kristina,=20 > >=20 > > We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda:=20 > > https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda= =20 > >=20 > > However, I don't think we can even write down the general version of=20 > > S^n as a type with a point and an n-loop with the schema implemented=20 > > in Cubical Agda. As far as I know no other schema for HITs support=20 > > this kind of types either.=20 > >=20 > > --=20 > > Anders=20 > >=20 > > On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova=20 > > > wrote:=20 > > >=20 > > > Hello everybody,=20 > > >=20 > > > Is it worked out somewhere that the two definitions of Sn as a=20 > > > suspension on one hand and a HIT with a point and an n-loop on the=20 > other=20 > > > hand are equivalent? This is also an exercise in the book. I know=20 > > > Favonia has some Agda code on spheres but I couldn't find this result= =20 > in=20 > > > there.=20 > > >=20 > > > Thanks,=20 > > >=20 > > > Kristina=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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/db712ad2-396f-4328-bb73-898dcb956834%40googlegroups.com. ------=_Part_3270_1352620414.1568808029789 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Let me elaborate a bit on my answer. One might naivel= y try to copy Dan and Guillaume's definition and write the following in= Cubical Agda:


Omega : (A :<= /span> Type=E2=82=80) =E2=86=92 A =E2=86=92 Type=E2=82=80
Omega A a =3D (a =E2=89=A1 a)

itOmega : =E2=84=95 =E2=86=92 (A : Type=E2=82=80) =E2=86=92 A =E2=86=92 Type=E2= =82=80
= itOmega zero A a =3D= Omega A a
itOmeg= a (= suc n) A a =3D itOmega n (Omega A a) refl

data Sn (n : =E2=84=95) : Type=E2=82=80 where
=C2=A0 base<= span style=3D"color: #000;" class=3D"styled-by-prettify"> : Sn n
=C2=A0 surf : itOmega n (Sn n= ) <= span style=3D"color: #008;" class=3D"styled-by-prettify">base
<= /code>


However Agda will complain as surf is n= ot constructing an element of Sn. This might seem a bit funny as Cubical Ag= da is perfectly happy with


data S=C2=B3 : Type=E2=82=80 where =
=C2=A0 base : S=C2=B3
=C2=A0 surf : Path (Path= (<= span style=3D"color: #008;" class=3D"styled-by-prettify">base =E2=89=A1 base) refl refl) refl refl


But what is happening under the hood is that surf is a constructor= taking i, j, and k in the interval and returning an element of S^3 with bo= undary "base" whenever i, j and k are 0 or 1. In cubicaltt we can= write this HIT in the following way:


data = S3 =3D base
=C2=A0| surf <i j k> [= (<= span style=3D"color: #000;" class=3D"styled-by-prettify">i=3D0) -> base
= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 , (i=3D1) -> base
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 , = (j=3D0) -> base
= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 , (j=3D1) -> base
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 , = (k=3D0) -> base
= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 , (k=3D1) -> base ]
The problem is then clearer: in ord= er to write the surf constructor of Sn we would have to quantify over n int= erval variables and specify the boundary of the n-cell. This is what that i= s not supported by any of the cubical schemas for HITs.

<= /div>
--
Anders

On Wednesday, Septemb= er 18, 2019 at 11:00:22 AM UTC+2, Guillaume Brunerie wrote:
Hi,

We give a definition of S^n with one point and one n-loop by
introduction/elimination/reduction rules in our paper with Dan Lic= ata
(https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can= be
implemented in Agda (so Kristina=E2=80=99s question can be formulated a= nd can
presumably be formalized in Agda) but I don=E2=80=99t think we actually= proved
it.

Best,
Guillaume

Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg <andersm...@gmail.com= >:
>
> Hi Kristina,
>
> We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda:
> https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda
>
> However, I don't think we can even write down the general vers= ion of
> S^n as a type with a point and an n-loop with the schema implement= ed
> in Cubical Agda. As far as I know no other schema for HITs support
> this kind of types either.
>
> --
> Anders
>
> On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova
> <sojakova...@gmail.com> wrote:
> >
> > Hello everybody,
> >
> > Is it worked out somewhere that the two definitions of Sn as = a
> > suspension on one hand and a HIT with a point and an n-loop o= n the other
> > hand are equivalent? This is also an exercise in the book. I = know
> > Favonia has some Agda code on spheres but I couldn't find= this result in
> > there.
> >
> > Thanks,
> >
> > Kristina
> >
> >

--
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/db712ad2-396f-4328-bb73-898dcb956834%40googleg= roups.com.
------=_Part_3270_1352620414.1568808029789-- ------=_Part_3269_209704738.1568808029788--