Data.Morphisms

Definitions

record Morphism : Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

Mor : (a -> b) -> Morphism a b

Projection: 

.applyMor : Morphism a b -> a -> b

Hints:

Applicative (Morphism r)

Cast (Endomorphism a) (Morphism a a)

Cast (Morphism a a) (Endomorphism a)

Cast (Morphism a (f b)) (Kleislimorphism f a b)

Cast (Kleislimorphism f a b) (Morphism a (f b))

Cast (Morphism a b) (Op b a)

Cast (Op b a) (Morphism a b)

Functor (Morphism r)

Monad (Morphism r)

Monoid a => Monoid (Morphism r a)

Semigroup a => Semigroup (Morphism r a)

.applyMor : Morphism a b -> a -> b

Totality: total
Visibility: public export

applyMor : Morphism a b -> a -> b

Totality: total
Visibility: public export

(~>) : Type -> Type -> Type

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 1

record Endomorphism : Type -> Type

Totality: total
Visibility: public export
Constructor: 

Endo : (a -> a) -> Endomorphism a

Projection: 

.applyEndo : Endomorphism a -> a -> a

Hints:

Cast (Endomorphism a) (Morphism a a)

Cast (Morphism a a) (Endomorphism a)

Cast (Endomorphism a) (Op a a)

Cast (Op a a) (Endomorphism a)

Monoid (Endomorphism a)

Semigroup (Endomorphism a)

.applyEndo : Endomorphism a -> a -> a

Totality: total
Visibility: public export

applyEndo : Endomorphism a -> a -> a

Totality: total
Visibility: public export

record Kleislimorphism : (Type -> Type) -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

Kleisli : (a -> f b) -> Kleislimorphism f a b

Projection: 

.applyKleisli : Kleislimorphism f a b -> a -> f b

Hints:

Applicative f => Applicative (Kleislimorphism f a)

Cast (Morphism a (f b)) (Kleislimorphism f a b)

Cast (Kleislimorphism f a b) (Morphism a (f b))

Cast (Op (f b) a) (Kleislimorphism f a b)

Cast (Kleislimorphism f a b) (Op (f b) a)

Functor f => Functor (Kleislimorphism f a)

Monad f => Monad (Kleislimorphism f a)

(Monoid a, Applicative f) => Monoid (Kleislimorphism f r a)

(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a)

.applyKleisli : Kleislimorphism f a b -> a -> f b

Totality: total
Visibility: public export

applyKleisli : Kleislimorphism f a b -> a -> f b

Totality: total
Visibility: public export

record Op : Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkOp : (a -> b) -> Op b a

Projection: 

.applyOp : Op b a -> a -> b

Hints:

Cast (Endomorphism a) (Op a a)

Cast (Op a a) (Endomorphism a)

Cast (Op (f b) a) (Kleislimorphism f a b)

Cast (Kleislimorphism f a b) (Op (f b) a)

Cast (Morphism a b) (Op b a)

Cast (Op b a) (Morphism a b)

Contravariant (Op b)

.applyOp : Op b a -> a -> b

Totality: total
Visibility: public export

applyOp : Op b a -> a -> b

Totality: total
Visibility: public export