{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : Typeclasses for 'Category' with special properties such as being cocomplete.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Typeclasses for 'Category' with special properties such as being cocomplete. 

A 'Category' might have coproducts meaning that any 'discreteDiagram' on it has a colimit.

A 'Category' might have coequalizers meaning that any 'parallelDiagram' on it has a colimit.

If a 'Category' have both coproducts and coequalizers, it is cocomplete meaning that it has all small colimits.

To compute colimits in a custom 'FiniteCategory', see 'colimits' in Math.ConeCategory.
-}

module Math.CocompleteCategory
(
    -- * Colimit type

    Colimit(..),
    uncoproject,
    -- * Helper typeclasses to define a 'CocompleteCategory'

    HasCoproducts(..),
    HasCoequalizers(..),
    colimitFromCoproductsAndCoequalizers,
    -- * Cocomplete Category

    CocompleteCategory(..),
    uncoprojectBase,
)
where
    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
    import              Data.List               (intercalate)
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.Functors.DiagonalFunctor
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.Galaxy
    import              Math.FiniteCategories.DiscreteCategory
    import              Math.FiniteCategories.Parallel
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    -- | For a 'Category' parametrized over a type t, the apex of the colimit of a diagram indexed by a category parametrized over a type i will contain 'Coproduct' constructions. A given distinguished element can be constructed from a 'Coprojection' at a given index.

    --

    -- For example, in 'FinSet', let's consider a discrete diagram from 'DiscreteTwo' to ('FinSet' Int) which selects {1,2} and {3,4}. The nadir of the colimit is obviously {('A',1),('A',2),('B',3),('B',4)}, note that it is not an object of ('Finset' Int) but an object of ('FinSet' (DiscreteTwoOb,Int)). The 'Colimit' type allows to construct type ('FinSet' ('Colimit' 'DiscreteTwo' Int)) in which we can consider the original objects with 'Coprojection' and the new distinguished elements with 'Coproduct'. Thus, the colimit will be {Coproduct 'A' 1,Coproduct 'A' 2,Coproduct 'B' 3,Coproduct 'B' 4}. We can construct coprojections in the same category, for example along 'A', which will map ('Coprojection' 1) to 'Coproduct' 'A' 1.

    data Colimit i t = Coprojection t -- ^ A 'Coprojection' is the parameter type of the original category to coproject them to the colimit.

                     | CoproductElement i t  -- ^ A 'CoproductElement' is a couple containing an indexing object and an object of type t.

                     deriving (Colimit i t -> Colimit i t -> Bool
(Colimit i t -> Colimit i t -> Bool)
-> (Colimit i t -> Colimit i t -> Bool) -> Eq (Colimit i t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i t. (Eq i, Eq t) => Colimit i t -> Colimit i t -> Bool
$c== :: forall i t. (Eq i, Eq t) => Colimit i t -> Colimit i t -> Bool
== :: Colimit i t -> Colimit i t -> Bool
$c/= :: forall i t. (Eq i, Eq t) => Colimit i t -> Colimit i t -> Bool
/= :: Colimit i t -> Colimit i t -> Bool
Eq, Int -> Colimit i t -> ShowS
[Colimit i t] -> ShowS
Colimit i t -> String
(Int -> Colimit i t -> ShowS)
-> (Colimit i t -> String)
-> ([Colimit i t] -> ShowS)
-> Show (Colimit i t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall i t. (Show i, Show t) => Int -> Colimit i t -> ShowS
forall i t. (Show i, Show t) => [Colimit i t] -> ShowS
forall i t. (Show i, Show t) => Colimit i t -> String
$cshowsPrec :: forall i t. (Show i, Show t) => Int -> Colimit i t -> ShowS
showsPrec :: Int -> Colimit i t -> ShowS
$cshow :: forall i t. (Show i, Show t) => Colimit i t -> String
show :: Colimit i t -> String
$cshowList :: forall i t. (Show i, Show t) => [Colimit i t] -> ShowS
showList :: [Colimit i t] -> ShowS
Show, (forall x. Colimit i t -> Rep (Colimit i t) x)
-> (forall x. Rep (Colimit i t) x -> Colimit i t)
-> Generic (Colimit i t)
forall x. Rep (Colimit i t) x -> Colimit i t
forall x. Colimit i t -> Rep (Colimit i t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall i t x. Rep (Colimit i t) x -> Colimit i t
forall i t x. Colimit i t -> Rep (Colimit i t) x
$cfrom :: forall i t x. Colimit i t -> Rep (Colimit i t) x
from :: forall x. Colimit i t -> Rep (Colimit i t) x
$cto :: forall i t x. Rep (Colimit i t) x -> Colimit i t
to :: forall x. Rep (Colimit i t) x -> Colimit i t
Generic, Colimit i t -> Colimit i t
(Colimit i t -> Colimit i t) -> Simplifiable (Colimit i t)
forall a. (a -> a) -> Simplifiable a
forall i t.
(Simplifiable t, Simplifiable i) =>
Colimit i t -> Colimit i t
$csimplify :: forall i t.
(Simplifiable t, Simplifiable i) =>
Colimit i t -> Colimit i t
simplify :: Colimit i t -> Colimit i t
Simplifiable)
                   
    instance (PrettyPrint i, PrettyPrint t, Eq i) => PrettyPrint (Colimit i t) where
        pprint :: Int -> Colimit i t -> String
pprint Int
v (Coprojection t
x) = Int -> t -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v t
x
        pprint Int
v (CoproductElement i
idx t
x) = Int -> t -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> i -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v i
idx
        
        pprintWithIndentations :: Int -> Int -> String -> Colimit i t -> String
pprintWithIndentations Int
cv Int
ov String
indent (Coprojection t
x) = Int -> ShowS
indentation (Int
ov Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
cv) String
indent String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> t -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
cv t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
        pprintWithIndentations Int
cv Int
ov String
indent (CoproductElement i
idx t
x) = Int -> ShowS
indentation (Int
ov Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
cv) String
indent String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> t -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
cv t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> i -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
cv i
idx String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
    
    -- | Remove the constructor 'Coprojection' from an original object t, throws an error if a 'CoproductElement' is given.

    uncoproject :: Colimit oIndex t -> t
    uncoproject :: forall oIndex t. Colimit oIndex t -> t
uncoproject (Coprojection t
t) = t
t
    uncoproject (CoproductElement oIndex
_ t
_) = String -> t
forall a. HasCallStack => String -> a
error String
"Uncoproject a coproduct element."
    
    -- | The typeclass of categories which have all coproducts.

    class (Category c m o, Morphism m o,
           Category cLim mLim oLim, Morphism mLim oLim) =>
           HasCoproducts c m o cLim mLim oLim oIndex | c -> m, m -> o, cLim -> mLim, mLim -> oLim, c oIndex -> cLim where
        -- | Given a 'discreteDiagram' selecting objects, return the coproduct of the selected objects as a 'Cocone'.

        coproduct :: Diagram (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o  -> Cocone(DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex cLim mLim oLim
        
    -- | The typeclass of categories which have all coequalizers.

    class (Category c m o, Morphism m o) => HasCoequalizers c m o | c -> m, m -> o where
        -- | Given a 'parallelDiagram' selecting arrows, return the coequalizer of the selected arrows as a 'Cocone'.  

        coequalize :: Diagram Parallel ParallelAr ParallelOb c m o -> Cocone Parallel ParallelAr ParallelOb c m o
        
    -- | The typeclass of categories which have all colimits.

    class (Category c m o, Morphism m o,
           Category cLim mLim oLim, Morphism mLim oLim) =>
           CocompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex | c -> m, m -> o, cLim -> mLim, mLim -> oLim, c cIndex mIndex oIndex -> cLim where
        
        -- | Return the colimit of a 'Diagram'.

        colimit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => Diagram cIndex mIndex oIndex c m o -> Cocone cIndex mIndex oIndex cLim mLim oLim
        
        -- | A partial 'Diagram' to coproject objects and morphisms of a base like a call of 'colimit' would do.

        --

        -- (coconeBase (colimit diag)) should equal ((coprojectBase diag) <-@<- diag)

        coprojectBase :: Diagram cIndex mIndex oIndex c m o -> Diagram c m o cLim mLim oLim
       

    -- | A partial 'Diagram' to uncoproject objects and morphisms of the base in a 'colimit' cocone.

    --

    -- uncoprojectBase and coprojectBase returned 'Diagram's are inverses.

    uncoprojectBase :: (CocompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex) => Diagram cIndex mIndex oIndex c m o -> Diagram cLim mLim oLim c m o
    uncoprojectBase :: forall c m o cLim mLim oLim cIndex mIndex oIndex.
CocompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex =>
Diagram cIndex mIndex oIndex c m o -> Diagram cLim mLim oLim c m o
uncoprojectBase = Diagram c m o cLim mLim oLim -> Diagram cLim mLim oLim c m o
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c1 m1 o1
unsafeInverseDiagram(Diagram c m o cLim mLim oLim -> Diagram cLim mLim oLim c m o)
-> (Diagram cIndex mIndex oIndex c m o
    -> Diagram c m o cLim mLim oLim)
-> Diagram cIndex mIndex oIndex c m o
-> Diagram cLim mLim oLim c m o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram cIndex mIndex oIndex c m o -> Diagram c m o cLim mLim oLim
forall c m o cLim mLim oLim cIndex mIndex oIndex.
CocompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex =>
Diagram cIndex mIndex oIndex c m o -> Diagram c m o cLim mLim oLim
coprojectBase
        
    
    -- | Computes efficiently colimits thanks to coproducts and coequalizers. Can be used to instantiate 'CocompleteCategory'.

    --

    -- The first argument is a function to transform an object of the original category into a colimit object.

    --

    -- Most of the time, the original category takes one type parameter and the function uses 'Coprojection', when the category does not take any type parameter it is 'id'. 

    --

    -- For example, for 'FinSet', the function has to transform a function {1 -> 2} to the function {Coprojection 1 -> Coprojection 2}.

    colimitFromCoproductsAndCoequalizers ::
      (Category c m o, Morphism m o,
       Category cLim mLim oLim, Morphism mLim oLim, HasCoproducts c m o cLim mLim oLim oIndex,HasCoequalizers cLim mLim oLim,
       FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq oIndex, Eq mIndex, Eq cIndex) => 
       (m -> mLim) -> Diagram cIndex mIndex oIndex c m o -> Cocone cIndex mIndex oIndex cLim mLim oLim
    colimitFromCoproductsAndCoequalizers :: forall c m o cLim mLim oLim oIndex cIndex mIndex.
(Category c m o, Morphism m o, Category cLim mLim oLim,
 Morphism mLim oLim, HasCoproducts c m o cLim mLim oLim oIndex,
 HasCoequalizers cLim mLim oLim,
 FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq oIndex, Eq mIndex, Eq cIndex) =>
(m -> mLim)
-> Diagram cIndex mIndex oIndex c m o
-> Cocone cIndex mIndex oIndex cLim mLim oLim
colimitFromCoproductsAndCoequalizers m -> mLim
transformMorphismIntoColimMorphism Diagram cIndex mIndex oIndex c m o
diag = CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
colim
            where
                idxCat :: cIndex
idxCat = Diagram cIndex mIndex oIndex c m o -> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex c m o
diag
                discreteDiag :: Diagram
  (DiscreteCategory oIndex) (StarIdentity oIndex) oIndex c m o
discreteDiag = Diagram
  (DiscreteCategory oIndex) (StarIdentity oIndex) oIndex c m o
-> Diagram
     (DiscreteCategory oIndex) (StarIdentity oIndex) oIndex c m o
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: DiscreteCategory oIndex
src = Set oIndex -> DiscreteCategory oIndex
forall a. Set a -> DiscreteCategory a
discreteCategory Set oIndex
bottomObjects, tgt :: c
tgt = Diagram cIndex mIndex oIndex c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram cIndex mIndex oIndex c m o
diag, omap :: Map oIndex o
omap = Set (oIndex, o) -> Map oIndex o
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(oIndex
o,Diagram cIndex mIndex oIndex c m o
diag Diagram cIndex mIndex oIndex c m o -> oIndex -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
o) | oIndex
o <- Set oIndex
bottomObjects], mmap :: Map (StarIdentity oIndex) m
mmap = AssociationList (StarIdentity oIndex) m
-> Map (StarIdentity oIndex) m
forall k v. AssociationList k v -> Map k v
weakMap []}
                bottomObjects :: Set oIndex
bottomObjects = (oIndex -> Bool) -> Set oIndex -> Set oIndex
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\oIndex
o -> Set Bool -> Bool
Set.and [Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set mIndex -> Bool
forall a. Set a -> Bool
Set.null (Set mIndex -> Bool) -> Set mIndex -> Bool
forall a b. (a -> b) -> a -> b
$ cIndex -> oIndex -> oIndex -> Set mIndex
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar cIndex
idxCat (mIndex -> oIndex
forall m o. Morphism m o => m -> o
target mIndex
m) oIndex
o | mIndex
m <- cIndex -> oIndex -> Set mIndex
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arFrom cIndex
idxCat oIndex
o]) (cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob cIndex
idxCat)
                objectToAMorphismToABottomObject :: oIndex -> mIndex
objectToAMorphismToABottomObject oIndex
o
                    | oIndex
o oIndex -> Set oIndex -> Bool
forall a. Eq a => a -> Set a -> Bool
`Set.elem` Set oIndex
bottomObjects = cIndex -> oIndex -> mIndex
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity cIndex
idxCat oIndex
o
                    | Bool
otherwise = Set mIndex -> mIndex
forall a. Set a -> a
anElement [mIndex
m | mIndex
m <- cIndex -> oIndex -> Set mIndex
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arFrom cIndex
idxCat oIndex
o, mIndex -> oIndex
forall m o. Morphism m o => m -> o
target mIndex
m oIndex -> Set oIndex -> Bool
forall a. Eq a => a -> Set a -> Bool
`Set.elem` Set oIndex
bottomObjects]
                coprod :: Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
coprod = Diagram
  (DiscreteCategory oIndex) (StarIdentity oIndex) oIndex c m o
-> Cocone
     (DiscreteCategory oIndex)
     (StarIdentity oIndex)
     oIndex
     cLim
     mLim
     oLim
forall c m o cLim mLim oLim oIndex.
HasCoproducts c m o cLim mLim oLim oIndex =>
Diagram
  (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     cLim
     mLim
     oLim
coproduct Diagram
  (DiscreteCategory oIndex) (StarIdentity oIndex) oIndex c m o
discreteDiag
                newDiag :: Diagram cIndex mIndex oIndex cLim mLim oLim
newDiag = (Diagram cIndex mIndex oIndex cLim mLim oLim
-> Diagram cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: cIndex
src = Diagram cIndex mIndex oIndex c m o -> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex c m o
diag, tgt :: cLim
tgt = (Diagram
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> cLim
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> Diagram
     (DiscreteCategory oIndex)
     (StarIdentity oIndex)
     oIndex
     cLim
     mLim
     oLim
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCocone Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
coprod)), omap :: Map oIndex oLim
omap = AssociationList oIndex oLim -> Map oIndex oLim
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map mIndex mLim
mmap = m -> mLim
transformMorphismIntoColimMorphism (m -> mLim) -> Map mIndex m -> Map mIndex mLim
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Diagram cIndex mIndex oIndex c m o -> Map mIndex m
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram cIndex mIndex oIndex c m o
diag})
                undiscrete :: CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
undiscrete = oLim
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
-> CommaObject
     One
     oLim
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> oLim
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
coprod) (Diagram cIndex mIndex oIndex cLim mLim oLim
-> Diagram cIndex mIndex oIndex cLim mLim oLim
-> Map oIndex mLim
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram cIndex mIndex oIndex cLim mLim oLim
newDiag (cIndex
-> cLim -> oLim -> Diagram cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram (Diagram cIndex mIndex oIndex c m o -> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex c m o
diag) (Diagram
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> cLim
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> Diagram
     (DiscreteCategory oIndex)
     (StarIdentity oIndex)
     oIndex
     cLim
     mLim
     oLim
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCocone Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
coprod)) (Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> oLim
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
coprod)) (Set (oIndex, mLim) -> Map oIndex mLim
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(oIndex
o,((Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (StarIdentity oIndex)
     oIndex
     cLim
     mLim
     oLim
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
coprod) NaturalTransformation
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> oIndex -> mLim
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ (mIndex -> oIndex
forall m o. Morphism m o => m -> o
target (mIndex -> oIndex) -> mIndex -> oIndex
forall a b. (a -> b) -> a -> b
$ oIndex -> mIndex
objectToAMorphismToABottomObject oIndex
o)) mLim -> mLim -> mLim
forall m o. Morphism m o => m -> m -> m
@ (Diagram cIndex mIndex oIndex cLim mLim oLim
newDiag Diagram cIndex mIndex oIndex cLim mLim oLim -> mIndex -> mLim
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (oIndex -> mIndex
objectToAMorphismToABottomObject oIndex
o))) | oIndex
o <- (cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob(cIndex -> Set oIndex)
-> (Diagram cIndex mIndex oIndex c m o -> cIndex)
-> Diagram cIndex mIndex oIndex c m o
-> Set oIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram cIndex mIndex oIndex c m o -> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (Diagram cIndex mIndex oIndex c m o -> Set oIndex)
-> Diagram cIndex mIndex oIndex c m o -> Set oIndex
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex c m o
diag)]))
                coequalizeFromMorph :: mIndex
-> CommaObject
     One
     oLim
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> CommaObject
     One
     oLim
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
coequalizeFromMorph mIndex
fIndex CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currColim = oLim
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
-> CommaObject
     One
     oLim
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (Cocone Parallel ParallelAr ParallelOb cLim mLim oLim -> oLim
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone Parallel ParallelAr ParallelOb cLim mLim oLim
coeq) ((mLim -> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
diagonal (Cocone Parallel ParallelAr ParallelOb cLim mLim oLim
-> NaturalTransformation
     Parallel ParallelAr ParallelOb cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone Parallel ParallelAr ParallelOb cLim mLim oLim
coeq NaturalTransformation Parallel ParallelAr ParallelOb cLim mLim oLim
-> ParallelOb -> mLim
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ ParallelOb
ParallelB)) NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall m o. Morphism m o => m -> m -> m
@ (CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currColim))
                    where
                        f :: m
f = Diagram cIndex mIndex oIndex c m o
diag Diagram cIndex mIndex oIndex c m o -> mIndex -> m
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ mIndex
fIndex
                        coeq :: Cocone Parallel ParallelAr ParallelOb cLim mLim oLim
coeq = Diagram Parallel ParallelAr ParallelOb cLim mLim oLim
-> Cocone Parallel ParallelAr ParallelOb cLim mLim oLim
forall c m o.
HasCoequalizers c m o =>
Diagram Parallel ParallelAr ParallelOb c m o
-> Cocone Parallel ParallelAr ParallelOb c m o
coequalize (Diagram Parallel ParallelAr ParallelOb cLim mLim oLim
 -> Cocone Parallel ParallelAr ParallelOb cLim mLim oLim)
-> Diagram Parallel ParallelAr ParallelOb cLim mLim oLim
-> Cocone Parallel ParallelAr ParallelOb cLim mLim oLim
forall a b. (a -> b) -> a -> b
$ Diagram Parallel ParallelAr ParallelOb cLim mLim oLim
-> Diagram Parallel ParallelAr ParallelOb cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: Parallel
src = Parallel
Parallel, tgt :: cLim
tgt = Diagram cIndex mIndex oIndex cLim mLim oLim -> cLim
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> Diagram cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCocone CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currColim), omap :: Map ParallelOb oLim
omap = AssociationList ParallelOb oLim -> Map ParallelOb oLim
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map ParallelAr mLim
mmap = AssociationList ParallelAr mLim -> Map ParallelAr mLim
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelAr
ParallelF, (CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currColim) NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
-> oIndex -> mLim
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ (mIndex -> oIndex
forall m o. Morphism m o => m -> o
source mIndex
fIndex)),(ParallelAr
ParallelG, ((CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currColim) NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
-> oIndex -> mLim
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ (mIndex -> oIndex
forall m o. Morphism m o => m -> o
target mIndex
fIndex)) mLim -> mLim -> mLim
forall m o. Morphism m o => m -> m -> m
@ (m -> mLim
transformMorphismIntoColimMorphism m
f))]}
                        diagonal :: mLim -> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
diagonal mLim
m = Diagram cIndex mIndex oIndex cLim mLim oLim
-> Diagram cIndex mIndex oIndex cLim mLim oLim
-> Map oIndex mLim
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (cIndex
-> cLim -> oLim -> Diagram cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram (Diagram cIndex mIndex oIndex c m o -> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex c m o
diag) (Diagram cIndex mIndex oIndex cLim mLim oLim -> cLim
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> Diagram cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCocone CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
undiscrete)) (mLim -> oLim
forall m o. Morphism m o => m -> o
source mLim
m)) (cIndex
-> cLim -> oLim -> Diagram cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram (Diagram cIndex mIndex oIndex c m o -> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex c m o
diag) (Diagram cIndex mIndex oIndex cLim mLim oLim -> cLim
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> Diagram cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCocone CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
undiscrete)) (mLim -> oLim
forall m o. Morphism m o => m -> o
target mLim
m)) ((oIndex -> mLim) -> Set oIndex -> Map oIndex mLim
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (mLim -> oIndex -> mLim
forall a b. a -> b -> a
const mLim
m) (cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram cIndex mIndex oIndex c m o -> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex c m o
diag)))
                colim :: CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
colim = (mIndex
 -> CommaObject
      One
      oLim
      (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
 -> CommaObject
      One
      oLim
      (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim))
-> CommaObject
     One
     oLim
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> Set mIndex
-> CommaObject
     One
     oLim
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr mIndex
-> CommaObject
     One
     oLim
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> CommaObject
     One
     oLim
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
coequalizeFromMorph CommaObject
  One
  oLim
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
undiscrete (([mIndex] -> Set mIndex
forall a. [a] -> Set a
set([mIndex] -> Set mIndex)
-> (Set mIndex -> [mIndex]) -> Set mIndex -> Set mIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set mIndex -> [mIndex]
forall a. Eq a => Set a -> [a]
setToList) (cIndex -> Set mIndex
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId cIndex
idxCat))