Pandora.Pattern.Functor.Adjoint

Documentation

class (Covariant t, Covariant u) => Adjoint t u where

When providing a new instance, you should ensure it satisfies the four laws:
* Left adjunction identity: phi cozero ≡ identity
* Right adjunction identity: psi zero ≡ identity
* Left adjunction interchange: phi f ≡ comap f . eta
* Right adjunction interchange: psi f ≡ epsilon . comap f

Minimal complete definition

phi, psi

Methods

phi :: (t a -> b) -> a -> u b

Left adjunction

psi :: (a -> u b) -> t a -> b

Right adjunction

eta :: a -> (u :.: t) >< a

epsilon :: ((t :.: u) >< a) -> a

Instances

Adjoint Identity Identity

Defined in Pandora.Paradigm.Basis.Identity

Methods

phi :: (Identity a -> b) -> a -> Identity b

psi :: (a -> Identity b) -> Identity a -> b

eta :: a -> (Identity :.: Identity) >< a

epsilon :: ((Identity :.: Identity) >< a) -> a

(Extractable t, Pointable t, Extractable u, Pointable u) => Adjoint (Yoneda t) (Yoneda u)

Defined in Pandora.Paradigm.Basis.Yoneda

Methods

phi :: (Yoneda t a -> b) -> a -> Yoneda u b

psi :: (a -> Yoneda u b) -> Yoneda t a -> b

eta :: a -> (Yoneda u :.: Yoneda t) >< a

epsilon :: ((Yoneda t :.: Yoneda u) >< a) -> a

Adjoint (Product a) ((->) a :: Type -> Type)

Defined in Pandora.Paradigm.Basis.Product

Methods

phi :: (Product a a0 -> b) -> a0 -> a -> b

psi :: (a0 -> a -> b) -> Product a a0 -> b

eta :: a0 -> ((->) a :.: Product a) >< a0

epsilon :: ((Product a :.: (->) a) >< a0) -> a0

(t :-|: u, v :-|: w) => Adjoint (TU Co Co t v) (TU Co Co u w)

Defined in Pandora.Pattern.Junction.Schemes.TU

Methods

phi :: (TU Co Co t v a -> b) -> a -> TU Co Co u w b

psi :: (a -> TU Co Co u w b) -> TU Co Co t v a -> b

eta :: a -> (TU Co Co u w :.: TU Co Co t v) >< a

epsilon :: ((TU Co Co t v :.: TU Co Co u w) >< a) -> a

(t :-|: w, v :-|: x, u :-|: y) => Adjoint (TUV Co Co Co t v u) (TUV Co Co Co w x y)

Defined in Pandora.Pattern.Junction.Schemes.TUV

Methods

phi :: (TUV Co Co Co t v u a -> b) -> a -> TUV Co Co Co w x y b

psi :: (a -> TUV Co Co Co w x y b) -> TUV Co Co Co t v u a -> b

eta :: a -> (TUV Co Co Co w x y :.: TUV Co Co Co t v u) >< a

epsilon :: ((TUV Co Co Co t v u :.: TUV Co Co Co w x y) >< a) -> a

(t :-|: u, v :-|: w, q :-|: q, r :-|: s) => Adjoint (TUVW Co Co Co Co t v q r) (TUVW Co Co Co Co u w q s)

Defined in Pandora.Pattern.Junction.Schemes.TUVW

Methods

phi :: (TUVW Co Co Co Co t v q r a -> b) -> a -> TUVW Co Co Co Co u w q s b

psi :: (a -> TUVW Co Co Co Co u w q s b) -> TUVW Co Co Co Co t v q r a -> b

eta :: a -> (TUVW Co Co Co Co u w q s :.: TUVW Co Co Co Co t v q r) >< a

epsilon :: ((TUVW Co Co Co Co t v q r :.: TUVW Co Co Co Co u w q s) >< a) -> a

type (-|) = Adjoint