Agda.Utils.TypeLevel

type family All (p :: k -> Constraint) (as :: [k]) :: Constraint where ...

type family If (b :: Bool) (l :: k) (r :: k) :: k where ...

type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l where ...

type family Foldr' (c :: Function k (Function l l -> *) -> *) (n :: l) (as :: [k]) :: l where ...

type family Map (f :: Function k l -> *) (as :: [k]) :: [l] where ...

data ConsMap0

data ConsMap1

type family Constant (b :: l) (as :: [k]) :: [l] where ...

type Arrows as r

type Products as

type family IsBase (t :: *) :: Bool where ...

type family Domains (t :: *) :: [*] where ...

type family Domains' (t :: *) :: [*] where ...

type family CoDomain (t :: *) :: * where ...

type family CoDomain' (t :: *) :: * where ...

class Currying as b

data Function

data Constant0

data Constant1

type family Apply (t :: Function k l -> *) (u :: k) :: l