{-# 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 :: forall c1 m1 o1 c2 o2 m2.
(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 c1
j c2
c = Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
-> 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
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
   c2
   m2
   o2
   (FunctorCategory c1 m1 o1 c2 m2 o2)
   (NaturalTransformation c1 m1 o1 c2 m2 o2)
   (Diagram c1 m1 o1 c2 m2 o2)
 -> 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)
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
-> 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
forall a b. (a -> b) -> a -> b
$ c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq o2) =>
c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
mkDiagonalFunctor c1
j c2
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 :: forall c1 m1 o1 c2 m2 o2.
(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 c1
j c2
c = Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
-> 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
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
   c2
   m2
   o2
   (FunctorCategory c1 m1 o1 c2 m2 o2)
   (NaturalTransformation c1 m1 o1 c2 m2 o2)
   (Diagram c1 m1 o1 c2 m2 o2)
 -> 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)
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
-> 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
forall a b. (a -> b) -> a -> b
$ c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq o2) =>
c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
mkDiagonalFunctor c1
j c2
c