From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.51.66 with SMTP id k63mr8882293itk.1.1516934319776; Thu, 25 Jan 2018 18:38:39 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.164.20 with SMTP id n20ls4191029ioe.12.gmail; Thu, 25 Jan 2018 18:38:38 -0800 (PST) X-Received: by 10.107.174.136 with SMTP id n8mr8706085ioo.55.1516934318733; Thu, 25 Jan 2018 18:38:38 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1516934318; cv=none; d=google.com; s=arc-20160816; b=MEdui2+bOeBtVC4meKx4FYFInYMrY39AtUI5kmkCzppIbx0l0/2DNrYjZRc4owPcmX tcoRmE426IQqMkBYFRG57kc4ydIpV+LgJqdYIzU+8dypF3rggGTEWI6I/pOsM5v3ve1x 8FC4RSEbubFKyUhRXrQpfMYFNXPlKsgcnwJ/2NYm/0SyjA56mRHVdo1gbc5yD62Dxuyw hjE4e56v2GEufve2p/37ScZEh/T03wWsJuQocTGfiSFThj0L+/pWvjCGHZEwHuCWKZmV eaPZH9B+MxiIbOMcDUe1WISZTlyMcCDC8C2i2GwRdnmG1v4h3g00OnmL45FSuJ+MIWy2 0KsA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=y3DgyQgMrHonRpeKmVmW3jeGWsdYxPEDS1si8D207mg=; b=l+jg+AzULUUo0+SpCEDl7AyDhPEGSmbSHjpSkHMZK2EpWDntUqtQ3iNZYp2qdpttZF SrddQ4dQWfRyyEmcG2AZsYoq+e2yOkEb8XdA9T3kLG07ElKdurrQVNQixNzZ4hFRVXiV VRf6rnVYfbXAYJOMScKR9NMEOjWIwpjApbr6mdkEf5rj+nM9imfcfA1CmcxJY9uBU38W uGR2aH39LUrd8PSOQJYfOnJ0GL3Lb7BfVqXzR4Vber+YzBrOZKA9I8CyfA53w2y+WIva Z7Ccf2uNdVl8hURgNlLmeN+DhLAgkg1NFkfTl7d/St095+vL2YX/0ztysW1ZcAvegYSJ cRyQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Oqk1fzyb; spf=pass (google.com: domain of fav...@gmail.com designates 2607:f8b0:400d:c0d::231 as permitted sender) smtp.mailfrom=fav...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt0-x231.google.com (mail-qt0-x231.google.com. [2607:f8b0:400d:c0d::231]) by gmr-mx.google.com with ESMTPS id g129si147763itd.1.2018.01.25.18.38.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 25 Jan 2018 18:38:38 -0800 (PST) Received-SPF: pass (google.com: domain of fav...@gmail.com designates 2607:f8b0:400d:c0d::231 as permitted sender) client-ip=2607:f8b0:400d:c0d::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Oqk1fzyb; spf=pass (google.com: domain of fav...@gmail.com designates 2607:f8b0:400d:c0d::231 as permitted sender) smtp.mailfrom=fav...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x231.google.com with SMTP id s3so24475702qtb.10 for ; Thu, 25 Jan 2018 18:38:38 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=y3DgyQgMrHonRpeKmVmW3jeGWsdYxPEDS1si8D207mg=; b=Oqk1fzybIKihpJezpr4T7FKZXrcLm+GIhskGu9itPVy4Ol4PD5OOOVv1V+O6Ud5QNl liWLme4cWaZkXdQDRIwwXnmm5OTI8i/QFSWrHRwqHEgtPj4DiSTQEmhyFp2DSIz9EBuX slW5UmFFJP8k/ZTiTrs+pNwh/m3WpMVSGfX0nH74vGx/2Jw8NZK5SMJq0ohwrWgdyyUq UaTrzc00bdhSUTCBqQr1NF9yjqpTBZYKBPR8LAfvL1Q5axBWyODazu916dchedyxKcIY 24tmxOG6WBKeTKZhiV3y5qTkPXlNR64Q+cF9qhtcRlPO/XvmKld4qodpWLC2r68MlLeo YhSw== X-Gm-Message-State: AKwxyteSfarYS8akEtZ7enGA4mc9GjUnuMNRlGicJM4a0hOjwxNAcs8t silchxj1Lox9KryMZxjNMkxMnSeTpCeCb6QQEgMkDg== X-Received: by 10.237.43.39 with SMTP id p36mr20864412qtd.92.1516934318295; Thu, 25 Jan 2018 18:38:38 -0800 (PST) MIME-Version: 1.0 References: <2d2edbc3-10f6-4c85-a88d-f810acf6789a@googlegroups.com> In-Reply-To: <2d2edbc3-10f6-4c85-a88d-f810acf6789a@googlegroups.com> From: Favonia Date: Fri, 26 Jan 2018 02:38:27 +0000 Message-ID: Subject: Re: [HoTT] How to define w types in agda? To: du yu Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="94eb2c0566c43091d80563a4cb12" --94eb2c0566c43091d80563a4cb12 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hello, The first argument to the function is of type Zro, and you can use the absurd pattern to define such a function. See http://agda.readthedocs.io/en/v2.5.3/language/function-definitions.html#abs= urd-patterns . However, there is a bigger issue---your W type seems wrong. At least I do not see why it is equivalent to the standard presentation. See https://github.com/agda/agda-stdlib/blob/master/src/Data/W.agda for a correct implementation in the standard library. Hope this helps. Best, Favonia On Thu, Jan 25, 2018 at 11:26 AM du yu wrote: > I have the following initial thoughts but can't work out to define zero a= s > a w type > > data Zro : Set where > > data One : Set where > O1 : One > > data Two : Set where > O2 : Two > I2 : Two > -- w types > > 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 {!!}) > > -- > 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 > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --94eb2c0566c43091d80563a4cb12 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello,

The first argument to the fu= nction is of type Zro, and you can use the absurd pattern to define such a = function. See=C2=A0http://agda.readthedocs.io/en/v= 2.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 equivalent to the standard presentation. See= =C2=A0https://github.com/agda/agda-stdlib/blob/master/sr= c/Data/W.agda=C2=A0for a correct implementation in the standard library= .

Hope this helps.

Best,<= /div>
Favonia

On T= hu, Jan 25, 2018 at 11:26 AM du yu <doof...@gmail.com> wrote:
I have the following initial thoughts but= can't work out to define zero as a w type

data= Zro : Set=C2=A0 where

data One : Set where
<= div>=C2=A0 O1 : One

data 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 where -- 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 a= s w type

zero_w : natw
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 HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--94eb2c0566c43091d80563a4cb12--