I decided to start from something lighter than BTree. I choosed a List. This is easy because Lists are very like Nats, just a little bit more polymorphic.
When I meditated on that exercise I come to interesting conclusion. wNat has a "type" *, and has a value from "universe of types", W Bool So. Does it mean that when we declare wZero : wNat, wNat gets "expanded" and its' value gets substituted as the type for wZero? My description of Lists follows wNat example from paper. Did I described Lists correctly? ------------------------------------------------------------------------------ let (----------! ! wNat : * ) wNat => W Bool So ------------------------------------------------------------------------------ let (--------------! ! wZero : wNat ) wZero => Sup false notSo ------------------------------------------------------------------------------ ( n : wNat ! let !---------------! ! wSuc n : wNat ) wSuc n => Sup true (lam p => n) ------------------------------------------------------------------------------ ( A : * ; a : A ! let !----------------! ! wList a : * ) wList a => W Bool So ------------------------------------------------------------------------------ ( a : A ! let !------------------! ! wNil a : wList a ) wNil a => Sup false notSo ------------------------------------------------------------------------------ ( a : A ; as : wList A ! let !-----------------------! ! wCons a as : wList A ) wCons a as => Sup true (lam p => as) ------------------------------------------------------------------------------