Idris2Doc : Data.Morphisms
- record Endomorphism : Type -> Type
- Totality: total
Constructor: - Endo : (a -> a) -> Endomorphism a
Projection: - .applyEndo : Endomorphism a -> a -> a
- record Kleislimorphism : (Type -> Type) -> Type -> Type -> Type
- Totality: total
Constructor: - Kleisli : (a -> f b) -> Kleislimorphism f a b
Projection: - .applyKleisli : Kleislimorphism f a b -> a -> f b
- record Morphism : Type -> Type -> Type
- Totality: total
Constructor: - Mor : (a -> b) -> Morphism a b
Projection: - .applyMor : Morphism a b -> a -> b
- record Op : Type -> Type -> Type
- Totality: total
Constructor: - MkOp : (a -> b) -> Op b a
Projection: - .applyOp : Op b a -> a -> b
- (~>) : Type -> Type -> Type
- Totality: total
Fixity Declaration: infixr operator, level 1