{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : The lim functor which takes every diagram to its limit object. See also ConeCategory for the limit of a specific diagram.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The lim functor which takes every diagram to its limit object according to the global definition of limit. See also ConeCategory for the limit of a specific diagram.
-}

module Limit.Limit 
(
    limitFunctor,
    colimitFunctor,
)
where
    import              FiniteCategory.FiniteCategory
    import              Diagram.Diagram
    import              Adjunction.Adjunction
    import              FunctorCategory.FunctorCategory
    import              DiagonalFunctor.DiagonalFunctor
    import  IO.PrettyPrint
    
    -- | Returns the limit functor according to the global definition of limit (see https://ncatlab.org/nlab/show/limit#global_definition_in_terms_of_adjoint_of_the_constant_diagram_functor).
    --
    -- Given an indexing category @J@ and a category @C@, returns a functor which maps each diagram of form @J@ in @C@ to its limit object in @C@. 
    limitFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, PrettyPrintable c1, PrettyPrintable c2, PrettyPrintable o1, PrettyPrintable o2, PrettyPrintable m1, PrettyPrintable m2,
                     FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
                     c1 -> c2 -> Diagram (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) c2 m2 o2 
    limitFunctor j c = rightAdjoint $ mkDiagonalFunctor j c
    
    -- | Returns the colimit functor according to the global definition of colimit (see https://ncatlab.org/nlab/show/limit#global_definition_in_terms_of_adjoint_of_the_constant_diagram_functor).
    --
    -- Given an indexing category @J@ and a category @C@, returns a functor which maps each diagram of form @J@ in @C@ to its colimit object in @C@. 
    colimitFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                     FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
                     c1 -> c2 -> Diagram (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) c2 m2 o2 
    colimitFunctor j c = leftAdjoint $ mkDiagonalFunctor j c