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#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 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 <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 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 = x
rec2 _ y I2 = 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 = W Two (rec2 Zro One) -- nat type as w type

zero_w : natw
zero_w = sup O2 (λ x y → {!!})

--
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.