Control.Category.Instances.Type

(source)

This module defines the category of types and functions, named
`Typ`. Using this is more efficient than something like `Morphism`,
as it erases the types at runtime.

Definitions

data Typ : Type0 -> Type0 -> Type

Totality: total
Visibility: public export
Constructor:

MkTyp : (a .runW0 -> b .runW0) -> Typ a b

Hints:

Bimonoidal Typ Either Pair (W0 Void) (W0 ())
Braided Typ Pair (W0 ())
Braided Typ Either (W0 Void)
Cartesian Typ Pair (W0 ())
CatBifunctor Typ Typ Typ Pair
CatBifunctor Typ Typ Typ Either
CatFunctor Linear Typ id
Category Typ
Closed Typ Pair TypHom (W0 ())
Cocartesian Typ Either (W0 Void)
Monoidal Typ Pair (W0 ())
Monoidal Typ Either (W0 Void)
Promonad0 Typ
Semigroupoid Typ

runTyp : Typ a b -> a .runW0 -> b .runW0

Totality: total
Visibility: public export

.runTyp : Typ a b -> a .runW0 -> b .runW0

Totality: total
Visibility: public export

Typ_ : (0 _ : Type) -> (0 _ : Type) -> Type

Totality: total
Visibility: public export

Pair : Type0 -> Type0 -> Type0

Totality: total
Visibility: public export

Either : Type0 -> Type0 -> Type0

Totality: total
Visibility: public export

TypHom : Type0 -> Type0 -> Type0

Totality: total
Visibility: public export

SemigroupoidTyp : Semigroupoid Typ

Totality: total
Visibility: public export

FromMonad : Monad m => CatMonad Typ (liftW m)

Totality: total
Visibility: public export

FromTensor : Tensor ten i => Monoidal Typ (liftW2 ten) (W0 i)

Totality: total
Visibility: public export

FromFunctor : Functor f => StrongFunctor Typ Pair (liftW f)

Totality: total
Visibility: public export

FromApplicative : Applicative f => Bitraversable ten => StrongFunctor Typ (liftW2 ten) (liftW f)

Totality: total
Visibility: public export

FromMonad : Monad m => Bitraversable ten => StrongMonad Typ (liftW2 ten) (liftW m)

Totality: total
Visibility: public export

FromTensor : (Tensor ten i, Symmetric ten) => Braided Typ (liftW2 ten) (W0 i)

Totality: total
Visibility: public export

Typ : SemigroupoidR

Totality: total
Visibility: public export

Typ : CategoryR

Totality: total
Visibility: public export

Pair : BifunctorR Typ Typ Typ

Totality: total
Visibility: public export

Either : BifunctorR Typ Typ Typ

Totality: total
Visibility: public export

TypPair : MonoidalR

Totality: total
Visibility: public export

TypEither : MonoidalR

Totality: total
Visibility: public export

TypPair : BraidedR

Totality: total
Visibility: public export

TypEither : BraidedR

Totality: total
Visibility: public export

Typ : CartesianR

Totality: total
Visibility: public export

Typ : CocartesianR

Totality: total
Visibility: public export

Typ : ClosedR

Totality: total
Visibility: public export

Typ : BimonoidalR

Totality: total
Visibility: public export

Typ : RigCategoryR

Totality: total
Visibility: public export

Typ : SymRigCategoryR

Totality: total
Visibility: public export

Typ : DistributiveR

Totality: total
Visibility: public export