From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Thu, 25 Jan 2018 08:26:41 -0800 (PST)
From: du yu <doof...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <2d2edbc3-10f6-4c85-a88d-f810acf6789a@googlegroups.com>
Subject: How to define w types in agda?
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_2538_10343604.1516897601078"

------=_Part_2538_10343604.1516897601078
Content-Type: multipart/alternative; 
	boundary="----=_Part_2539_1378637997.1516897601078"

------=_Part_2539_1378637997.1516897601078
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

I have the following initial thoughts but can't work out to define zero as=
=20
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 {!!})


------=_Part_2539_1378637997.1516897601078
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">I have the following initial thoughts but can&#39;t work o=
ut to define zero as a w type<div><br></div><div><div>data Zro : Set=C2=A0 =
where</div><div><br></div><div>data One : Set where</div><div>=C2=A0 O1 : O=
ne</div><div><br></div><div>data Two : Set where</div><div>=C2=A0 O2 : Two<=
/div><div>=C2=A0 I2 : Two</div><div>-- w types=C2=A0</div><div><br></div><d=
iv>rec2 : (x y : Set) -&gt; Two -&gt; Set</div><div>rec2 x _ O2 =3D x</div>=
<div>rec2 _ y I2 =3D y</div><div><br></div><div><br></div><div>data W (A : =
Set) (B : A -&gt; Set) : Set where -- well founded trees</div><div>=C2=A0 w=
 : (s : A) -&gt; B s -&gt; W A B</div><div>=C2=A0 sup : (a : A) -&gt; ((B a=
) -&gt; ((x : A) -&gt; W A B )) -&gt; W A B</div><div><br></div><div>natw :=
 Set</div><div>natw =3D W Two (rec2 Zro One) -- nat type as w type</div><di=
v><br></div><div>zero_w : natw</div><div>zero_w =3D sup O2 (=CE=BB x y =E2=
=86=92 {!!})</div></div><div><br></div></div>
------=_Part_2539_1378637997.1516897601078--

------=_Part_2538_10343604.1516897601078--