module Math.Functors.Adjunction.Examples
(
exampleLeftAdjoint,
exampleRightAdjoint,
)
where
import Math.FiniteCategory
import Math.Categories
import Math.FiniteCategories
import Math.Functors.DiagonalFunctor.Examples
import Math.Functors.Adjunction
import Math.Functors.DiagonalFunctor
import Data.WeakSet (Set)
import qualified Data.WeakSet as Set
import Data.WeakSet.Safe
import Data.WeakMap (Map)
import qualified Data.WeakMap as Map
import Data.WeakMap.Safe
exampleLeftAdjoint :: Diagram (FunctorCategory (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (NaturalTransformation (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (Ens Int) (Function Int) (Set Int)
exampleLeftAdjoint :: Diagram
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
exampleLeftAdjoint = Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c1 m1 o1
leftAdjoint Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
exampleDiagonalFunctor
exampleRightAdjoint :: Diagram (FunctorCategory (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (NaturalTransformation (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (Ens Int) (Function Int) (Set Int)
exampleRightAdjoint :: Diagram
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
exampleRightAdjoint = Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c1 m1 o1 -> Diagram c1 m1 o1 c2 m2 o2
rightAdjoint Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
exampleDiagonalFunctor