{-| Module  : FiniteCategories
Description : An exemple of 'leftAdjoint' and 'rightAdjoint' use.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An exemple of 'leftAdjoint' and 'rightAdjoint' use.


-}
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
    

    -- | The 'leftAdjoint' of a diagonal functor allows to compute colimits.

    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
    
    -- | The 'rightAdjoint' of a diagonal functor allows to compute limits.

    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