Idris2Doc : Data.Morphisms

Data.Morphisms

recordEndomorphism : Type -> Type
Totality: total
Constructor: 
Endo : (a -> a) -> Endomorphisma

Projection: 
.applyEndo : Endomorphisma -> a -> a
recordKleislimorphism : (Type -> Type) -> Type -> Type -> Type
Totality: total
Constructor: 
Kleisli : (a -> fb) -> Kleislimorphismfab

Projection: 
.applyKleisli : Kleislimorphismfab -> a -> fb
recordMorphism : Type -> Type -> Type
Totality: total
Constructor: 
Mor : (a -> b) -> Morphismab

Projection: 
.applyMor : Morphismab -> a -> b
recordOp : Type -> Type -> Type
Totality: total
Constructor: 
MkOp : (a -> b) -> Opba

Projection: 
.applyOp : Opba -> a -> b
(~>) : Type -> Type -> Type
Totality: total
Fixity Declaration: infixr operator, level 1