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-x23f.google.com (mail-oi1-x23f.google.com [IPv6:2607:f8b0:4864:20::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 684acfbc for ; Sun, 27 Jan 2019 20:11:17 +0000 (UTC) Received: by mail-oi1-x23f.google.com with SMTP id t83sf7972798oie.16 for ; Sun, 27 Jan 2019 12:11:16 -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=mYHdtPDb7fnSnRpumez3JegdfGFKoU4GM8tCh3MMgfo=; b=Oo6aDfkfOwhmSoAS3756IoEA/pwh1tYiQ+unww3afCVyKQ4L/ZkhdoWUFXEWigu32c ViNH7lrY85/SvQaAqHoCXMuGA+gxAk82x4OxHVExmKcQAiLMfaDsjgicswwopm3hh6Vs mQE9IiQHQ5Ri1FH6/gyAm0xQ8bTQVrEy8ePVwp0AGvnGmZkucdylno0fqtUdI+/HSgOU X7K08pn5w84zyj6S5F86vitCnOTgymJt1XtQkig+e3s3gbDPnhTABaL053bG3TnFjFvq sYp0QpDwqrdAbcA3MDPuyjxweg+5qVWIuK7kIjfRafoEI2sgTC8o+M9Y34OWEQ14BNc+ 0aIg== 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=mYHdtPDb7fnSnRpumez3JegdfGFKoU4GM8tCh3MMgfo=; b=f2Tg5+6hx6Y6NySqOKcSSvGJENgTjs56Z2TEnoAi4OCMcSpkaBKbT2j6eQ8wGuW5kw d20VNIKDcWlaV/0tf3yqJ5WjQJG+XxGoCRDRY9VqI4ydKG6ZAzYFypza9cNZJFS52K7E 5dOooKT+6F1XZMhJBpro/fuqKU/m4M0qotsrVrPNwiEn4jhZ8QMeALJBk1YJECPqoYgH HijLd/xoWC35/QDKetOoEzQ14W66P3zEiMgct8SHLRIUi0CGBEWyQgjIJP7zjzhYmVr8 HMP6dNHQbtxYtPP46n5J3pzR7yGuDo1lKEW7pAYCLzPpcdrAhiC/y3mxkJgK4CC2Pylg 1hCQ== 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=mYHdtPDb7fnSnRpumez3JegdfGFKoU4GM8tCh3MMgfo=; b=KtYngiVhkRtx91JZ2Vy4A5FW0C8gsWMLOybVtOpDPGdXgY1pv1GKoP+uagWaRwDl5J XNf5ODOqau0Ic7KkhIF7xO9aO+0SLDN7Niye9NXhZLlLoMG+sad8r/pOg0NsSsQmr/Vf 79Li6eE8odigDTVZ/LTnH9PSRZRxyDctn7d45F7jb5KBt5jd+vKfRouhTvTs3Dmbg9Ck DhfmXQZS85yRod05aR7yohUxk2PchQ9nkkKxpDJYQlN2zlVgSGLQaYuW3BIEDlEkUZ9S Dv+44/qyN3J9a8EKYaKkYtEiqldmjbXGa3dN/JsmXDWHnFB/ceZ1G/WdntLj+8Cmd/MN S9WA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukc0p7u1qpswIGOn4ddfFXIcmpk0CsEGAtmzFGcp3nW0xWFVLhsp uHMsoa0YVNtBk4TFAWBTi/U= X-Google-Smtp-Source: ALg8bN6az2yGPqKZBTt2jlLfitBO431waVdeKs0AgMqlphRqutBLAvUDTYwOf5XiXMpJ/LUb8e/J4w== X-Received: by 2002:a9d:da3:: with SMTP id 32mr292450ots.3.1548619875496; Sun, 27 Jan 2019 12:11:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3183:: with SMTP id x125ls4022639oix.1.gmail; Sun, 27 Jan 2019 12:11:15 -0800 (PST) X-Received: by 2002:aca:cc0f:: with SMTP id c15mr110661oig.3.1548619875094; Sun, 27 Jan 2019 12:11:15 -0800 (PST) Date: Sun, 27 Jan 2019 12:11:14 -0800 (PST) From: Yuhao Huang To: Homotopy Type Theory Message-Id: <834b3418-8ca1-45a9-afb0-4085e6ee6c9c@googlegroups.com> Subject: [HoTT] Defining n-sphere via HIT in cubical Agda MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1260_532254462.1548619874367" X-Original-Sender: temp.use88@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_1260_532254462.1548619874367 Content-Type: multipart/alternative; boundary="----=_Part_1261_1608999753.1548619874368" ------=_Part_1261_1608999753.1548619874368 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I was experimenting cubical Agda with {-# OPTIONS --cubical --rewriting #-} I tried to define S^2, S^3 separately and found HIT worked fine. However when I was trying to write down Sphere n for general natural number= =20 n it simply won't allow me to do so.=20 And the error message is "The target of a constructor must be the datatype= =20 applied to its parameters". So how do I define a dependent HIT? PtType : Set=E2=82=81 PtType =3D =CE=A3 Set (=CE=BB A =E2=86=92 A) =CE=A91 : PtType =E2=86=92 PtType =CE=A91 A =3D ((A .snd) =E2=89=A1 (A .snd)) , refl =CE=A9 : (n : =E2=84=95) =E2=86=92 PtType =E2=86=92 PtType =CE=A9 0 A =3D A =CE=A9 (suc n) A =3D =CE=A91 (=CE=A9 n A) data S=C2=B2 : Set where base : S=C2=B2 surf : ((=CE=A9 2 (S=C2=B2 , base)) .fst) data S=C2=B3 : Set where base : S=C2=B3 cell : ((=CE=A9 3 (S=C2=B3 , base)) .fst) data Sphere : =E2=84=95 =E2=86=92 Set where base : (n : =E2=84=95) =E2=86=92 Sphere n --cell : (n : =E2=84=95) =E2=86=92 ((=CE=A9 n ((Sphere n) , (base n))) .f= st) -- Error! 222222222222 --=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_1261_1608999753.1548619874368 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I was experimenting cubical Agda with {-# OPTIONS --cubical --rewriting #-}

I tried to define S^2, S^3 separately and found H= IT worked fine.

However when I was trying to write= down Sphere n = for general natural number n it simply won't allow me to do so.
And the= error message is "The target of a constructor must be the datatype ap= plied to its parameters".
So how do I define a dependent= HIT?

PtType : Set=E2=82=81
PtType =3D =CE=A3 Set (=CE= =BB A =E2=86=92 A)

=CE=A91 : PtType =E2=86=92 PtType
=CE=A91 A =3D ((= A .= snd) =E2=89=A1 (A .sn= d))= , refl

=CE=A9 : (n : =E2=84=95) =E2=86=92 PtType =E2=86=92 PtType
= =CE=A9 0 A =3D A
=CE=A9 (suc n) A =3D =CE=A91 (=CE=A9 n A)

data S=C2=B2 : Set where
=C2=A0 base : S=C2=B2
=C2=A0 surf : ((=CE= =A9 2 (S=C2=B2 , base)) .fst)

data S=C2=B3 : Set= where
=C2=A0 base : S=C2=B3
=C2=A0 cell : ((=CE=A9 3 (S=C2=B3 , base))<= /span> .fst)

data Sphere : =E2=84=95 =E2= =86=92 Set where
=C2=A0 base : (n : =E2=84=95) =E2=86=92 Sphere n
=C2=A0 --cell : (<= /span>n : =E2=84=95) <= /span>=E2=86=92 ((=CE=A9= n ((Sphere n) , (base n))= ) .fst) =C2=A0-- Error!
















222222222222


--
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_1261_1608999753.1548619874368-- ------=_Part_1260_532254462.1548619874367--