FiniteCategories-0.6.0.0: src/Math/Functors/Adjunction/Examples.hs
{-| 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 = leftAdjoint 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 = rightAdjoint exampleDiagonalFunctor