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