Induction.Nat

record Box a n

a

 

n

 

MkBox : (call : LT m n -> a m) -> Box a n

call : (rec : Box a n) -> LT m n -> a m

MkBox : (call : LT m n -> a m) -> Box a n

app : All (Box (a :-> b) :-> Box a :-> Box b)

duplicate : All (Box a :-> Box (Box a))

extract : All (Box a) -> All a

fix : (a : Nat -> Type) -> All (Box a :-> a) -> All a

fixBox : All (Box a :-> a) -> All (Box a)

loeb : All (Box (Box a :-> a) :-> Box a)

ltClose : (LT m n -> a n -> a m) -> All (a :-> Box a)

ltLower : LT m n -> Box a n -> Box a m

lteClose : (LTE m n -> a n -> a m) -> All (a :-> Box a)

lteLower : LTE m n -> Box a n -> Box a m

map : (f : All (a :-> b)) -> All (Box a :-> Box b)

map2 : (f : All (a :-> b :-> c)) -> All (Box a :-> Box b :-> Box c)

pure : All a -> All (Box a)