From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 26 Jan 2018 00:50:57 -0800 (PST) From: du yu To: Homotopy Type Theory Message-Id: <33d5f1c2-7aff-4200-9eb6-b99c035595e9@googlegroups.com> In-Reply-To: References: <2d2edbc3-10f6-4c85-a88d-f810acf6789a@googlegroups.com> Subject: Re: [HoTT] How to define w types in agda? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_634_972652205.1516956657736" ------=_Part_634_972652205.1516956657736 Content-Type: multipart/alternative; boundary="----=_Part_635_1360726471.1516956657736" ------=_Part_635_1360726471.1516956657736 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Wow thanks! I don't know it is already defined in stdlib (google search=20 gives none!). As a beginner for dependent types , the data type definition= =20 is quite confusing sometimes! On Friday, January 26, 2018 at 10:38:39 AM UTC+8, Favonia wrote: > > Hello, > > The first argument to the function is of type Zro, and you can use the=20 > absurd pattern to define such a function. See=20 > http://agda.readthedocs.io/en/v2.5.3/language/function-definitions.html#a= bsurd-patterns > . > > However, there is a bigger issue---your W type seems wrong. At least I do= =20 > not see why it is equivalent to the standard presentation. See=20 > https://github.com/agda/agda-stdlib/blob/master/src/Data/W.agda for a=20 > correct implementation in the standard library. > > Hope this helps. > > Best, > Favonia > > On Thu, Jan 25, 2018 at 11:26 AM du yu >= =20 > wrote: > >> I have the following initial thoughts but can't work out to define zero= =20 >> as a w type >> >> data Zro : Set where >> >> data One : Set where >> O1 : One >> >> data Two : Set where >> O2 : Two >> I2 : Two >> -- w types=20 >> >> rec2 : (x y : Set) -> Two -> Set >> rec2 x _ O2 =3D x >> rec2 _ y I2 =3D y >> >> >> data W (A : Set) (B : A -> Set) : Set where -- well founded trees >> w : (s : A) -> B s -> W A B >> sup : (a : A) -> ((B a) -> ((x : A) -> W A B )) -> W A B >> >> natw : Set >> natw =3D W Two (rec2 Zro One) -- nat type as w type >> >> zero_w : natw >> zero_w =3D sup O2 (=CE=BB x y =E2=86=92 {!!}) >> >> --=20 >> You received this message because you are subscribed to the Google Group= s=20 >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n=20 >> email to HomotopyTypeThe...@googlegroups.com . >> For more options, visit https://groups.google.com/d/optout. >> > ------=_Part_635_1360726471.1516956657736 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Wow thanks! I don't know it is already defined in stdl= ib (google search gives none!). As a beginner for dependent types , the dat= a type definition is quite confusing sometimes!

On Friday, January 2= 6, 2018 at 10:38:39 AM UTC+8, Favonia wrote:
Hello,

The first argu= ment to the function is of type Zro, and you can use the absurd pattern to = define such a function. See=C2=A0h= ttp://agda.readthedocs.io/en/v2.5.3/language/function-definitions= .html#absurd-patterns.

However, there is = a bigger issue---your W type seems wrong. At least I do not see why it is e= quivalent to the standard presentation. See=C2=A0https://github.com/agda/agda-stdlib/blob/m= aster/src/Data/W.agda=C2=A0for a correct implementation in the sta= ndard library.

Hope this helps.

Best,
Favonia

On Thu, Jan 25, 2018 at 11:26 AM du yu <doo...@gmail.com> wro= te:
I have the fol= lowing initial thoughts but can't work out to define zero as a w type
data Zro : Set=C2=A0 where

= data One : Set where
=C2=A0 O1 : One

dat= a Two : Set where
=C2=A0 O2 : Two
=C2=A0 I2 : Two
=
-- w types=C2=A0

rec2 : (x y : Set) -> Two= -> Set
rec2 x _ O2 =3D x
rec2 _ y I2 =3D y


data W (A : Set) (B : A -> Set) : Set wh= ere -- well founded trees
=C2=A0 w : (s : A) -> B s -> W A = B
=C2=A0 sup : (a : A) -> ((B a) -> ((x : A) -> W A B ))= -> W A B

natw : Set
natw =3D W Two (= rec2 Zro One) -- nat type as w type

zero_w : natw<= /div>
zero_w =3D sup O2 (=CE=BB x y =E2=86=92 {!!})

--
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+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/= d/optout.
------=_Part_635_1360726471.1516956657736-- ------=_Part_634_972652205.1516956657736--