Type.Dummies

Documentation

data Lower a

"Kind-cast" (* -> *) to *

Instances

Fact (:∈: (Lower s) fam -> :⊆: (Inters fam) s)

Fact (:∈: (Lower s) fam -> :⊆: s (Unions fam))

Fact (:~~>: dom cod (Lower f) -> :~>: dom cod f)

Fact (:~>: dom cod f -> :~~>: dom cod (Lower f))

Applicative a => Fact (:∈: (Lower a) ApplicativeType)

MonadPlus a => Fact (:∈: (Lower a) MonadPlusType)

Monad a => Fact (:∈: (Lower a) MonadType)

Functor a => Fact (:∈: (Lower a) FunctorType)

data Lower1 a where

"Kind-cast" ((* -> *) -> *) to (* -> *) . Also lower elements using Lower.

Constructors

LowerElement :: u x -> Lower1 u (Lower x)

data Lower2 a where

"Kind-cast" (((* -> *) -> *) -> *) to ((* -> *) -> *) . Also lower elements using Lower1.

Constructors

Lower1Element :: u x -> Lower2 u (Lower1 x)

data Lower3 a where

"Kind-cast" ((((* -> *) -> *) -> *) -> *) to (((* -> *) -> *) -> *) . Also lower elements using Lower2.

Constructors

Lower2Element :: u x -> Lower3 u (Lower2 x)

data PAIR a b x

Pair of types of kind (* -> *)

data PAIR1 a b x

Pair of types of kind ((* -> *) -> *)

data PAIR2 a b x

Pair of types of kind (((* -> *) -> *) -> *)

data PAIR3 a b x

Pair of types of kind ((((* -> *) -> *) -> *) -> *)

data Bool0

data Bool1

data BOOL where

Constructors

Bool0 :: BOOL Bool0

Bool1 :: BOOL Bool1

elimBOOL :: BOOL a -> r Bool0 -> r Bool1 -> r a

kelimBOOL :: BOOL a -> r -> r -> r