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/ for a correct implementation in the standard library.Data/W.agda Hope this helps.Best,FavoniaOn Thu, Jan 25, 2018 at 11:26 AM du yu <doo...@gmail.com> wrote:I have the following initial thoughts but can't work out to define zero as a w type--data Zro : Set wheredata One : Set whereO1 : Onedata Two : Set whereO2 : TwoI2 : Two-- w typesrec2 : (x y : Set) -> Two -> Setrec2 x _ O2 = xrec2 _ y I2 = ydata W (A : Set) (B : A -> Set) : Set where -- well founded treesw : (s : A) -> B s -> W A Bsup : (a : A) -> ((B a) -> ((x : A) -> W A B )) -> W A Bnatw : Setnatw = W Two (rec2 Zro One) -- nat type as w typezero_w : natwzero_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 HomotopyTypeTheory+unsub...@googlegroups.com .
For more options, visit https://groups.google.com/d/optout .