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

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

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

A 'Category' might have products meaning that any 'discreteDiagram' on it has a limit.

A 'Category' might have equalizers meaning that any 'parallelDiagram' on it has a limit.

If a 'Category' have both products and equalizers, it is complete meaning that it has all small limits.

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

module Math.CompleteCategory
(
    -- * Limit type

    Limit(..),
    unproject,
    -- * Helper typeclasses to define a 'CompleteCategory'

    HasProducts(..),
    HasEqualizers(..),
    limitFromProductsAndEqualizers,
    -- * CompleteCategory

    CompleteCategory(..),
    unprojectBase,
)
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 limit of a diagram indexed by a category parametrized over a type i will contain 'ProductElement' constructions (a product element is a tuple). A given tuple can be projected onto a 'Projection' 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 apex of the limit is obviously {(1,3),(1,4),(2,3),(2,4)}, note that it is not an object of ('Finset' Int) but an object of ('FinSet' (Set (Int,Int))). The 'Limit' type allows to construct type ('FinSet' ('Limit' 'DiscreteTwo' Int)) in which we can consider the original objects with 'Projection' and the new tuples with 'ProductElement'. Here, instead of couples, we will consider the limit to be {ProductElement (weakMap [(A,1),(B,3)]),ProductElement (weakMap [(A,1),(B,4)]),ProductElement (weakMap [(A,2),(B,3)]),ProductElement (weakMap [(A,2),(B,4)])}. We can construct projections in the same category, for example along 'A', which will map 'ProductElement' (weakMap [(A,1),(B,3)]) to ('Projection' 1).

    data Limit oIndex t = Projection t -- ^ A 'Projection' is the parameter type of the original category to project the limits back to them.

                   | ProductElement (Map oIndex t) -- ^ A 'ProductElement' is a mapping from the indexing objects to objects of type t.

                   deriving (Limit oIndex t -> Limit oIndex t -> Bool
(Limit oIndex t -> Limit oIndex t -> Bool)
-> (Limit oIndex t -> Limit oIndex t -> Bool)
-> Eq (Limit oIndex t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall oIndex t.
(Eq t, Eq oIndex) =>
Limit oIndex t -> Limit oIndex t -> Bool
$c== :: forall oIndex t.
(Eq t, Eq oIndex) =>
Limit oIndex t -> Limit oIndex t -> Bool
== :: Limit oIndex t -> Limit oIndex t -> Bool
$c/= :: forall oIndex t.
(Eq t, Eq oIndex) =>
Limit oIndex t -> Limit oIndex t -> Bool
/= :: Limit oIndex t -> Limit oIndex t -> Bool
Eq, Int -> Limit oIndex t -> ShowS
[Limit oIndex t] -> ShowS
Limit oIndex t -> String
(Int -> Limit oIndex t -> ShowS)
-> (Limit oIndex t -> String)
-> ([Limit oIndex t] -> ShowS)
-> Show (Limit oIndex t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall oIndex t.
(Show t, Show oIndex) =>
Int -> Limit oIndex t -> ShowS
forall oIndex t. (Show t, Show oIndex) => [Limit oIndex t] -> ShowS
forall oIndex t. (Show t, Show oIndex) => Limit oIndex t -> String
$cshowsPrec :: forall oIndex t.
(Show t, Show oIndex) =>
Int -> Limit oIndex t -> ShowS
showsPrec :: Int -> Limit oIndex t -> ShowS
$cshow :: forall oIndex t. (Show t, Show oIndex) => Limit oIndex t -> String
show :: Limit oIndex t -> String
$cshowList :: forall oIndex t. (Show t, Show oIndex) => [Limit oIndex t] -> ShowS
showList :: [Limit oIndex t] -> ShowS
Show, (forall x. Limit oIndex t -> Rep (Limit oIndex t) x)
-> (forall x. Rep (Limit oIndex t) x -> Limit oIndex t)
-> Generic (Limit oIndex t)
forall x. Rep (Limit oIndex t) x -> Limit oIndex t
forall x. Limit oIndex t -> Rep (Limit oIndex t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall oIndex t x. Rep (Limit oIndex t) x -> Limit oIndex t
forall oIndex t x. Limit oIndex t -> Rep (Limit oIndex t) x
$cfrom :: forall oIndex t x. Limit oIndex t -> Rep (Limit oIndex t) x
from :: forall x. Limit oIndex t -> Rep (Limit oIndex t) x
$cto :: forall oIndex t x. Rep (Limit oIndex t) x -> Limit oIndex t
to :: forall x. Rep (Limit oIndex t) x -> Limit oIndex t
Generic, Limit oIndex t -> Limit oIndex t
(Limit oIndex t -> Limit oIndex t) -> Simplifiable (Limit oIndex t)
forall a. (a -> a) -> Simplifiable a
forall oIndex t.
(Simplifiable t, Simplifiable oIndex, Eq oIndex) =>
Limit oIndex t -> Limit oIndex t
$csimplify :: forall oIndex t.
(Simplifiable t, Simplifiable oIndex, Eq oIndex) =>
Limit oIndex t -> Limit oIndex t
simplify :: Limit oIndex t -> Limit oIndex t
Simplifiable)
                   
    instance (PrettyPrint oIndex, PrettyPrint t, Eq oIndex) => PrettyPrint (Limit oIndex t) where
        pprint :: Int -> Limit oIndex t -> String
pprint Int
v (Projection t
x) = Int -> t -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v t
x
        pprint Int
v (ProductElement Map oIndex t
tuple) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," (Int -> t -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v (t -> String) -> [t] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map oIndex t -> [t]
forall k a. Eq k => Map k a -> [a]
Map.elems Map oIndex t
tuple)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        
        pprintWithIndentations :: Int -> Int -> String -> Limit oIndex t -> String
pprintWithIndentations Int
cv Int
ov String
indent (Projection 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 (ProductElement Map oIndex t
tuple) = 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]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," (Int -> t -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
cv (t -> String) -> [t] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map oIndex t -> [t]
forall k a. Eq k => Map k a -> [a]
Map.elems Map oIndex t
tuple)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")\n"
    
    -- | Remove the constructor 'Projection' from an original object t if possible.

    unproject :: Limit oIndex t -> Maybe t
    unproject :: forall oIndex t. Limit oIndex t -> Maybe t
unproject (Projection t
t) = t -> Maybe t
forall a. a -> Maybe a
Just t
t
    unproject (ProductElement Map oIndex t
_) = Maybe t
forall a. Maybe a
Nothing
    
    -- | The typeclass of categories which have all products.

    class (Category c m o, Morphism m o,
           Category cLim mLim oLim, Morphism mLim oLim) =>
           HasProducts 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 product of the selected objects as a 'Cone'.

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

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

        equalize :: Diagram Parallel ParallelAr ParallelOb c m o -> Cone Parallel ParallelAr ParallelOb c m o
        
    -- | The typeclass of categories which have all limits. cLim is the type of the new category in which we can compute limits and their projections. cIndex is the type of the indexing category of the diagrams.

    class (Category c m o, Morphism m o,
           Category cLim mLim oLim, Morphism mLim oLim) =>
           CompleteCategory 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 limit of a 'Diagram'.

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

        --

        -- (coneBase (limit diag)) should equal ((projectBase diag) <-@<- (diag))

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

    -- | A partial 'Diagram' to unproject object and morphism of the base in a 'limit' cone.

    --

    -- unprojectBase and projectBase returned 'Diagram's are inverses.

    unprojectBase :: (CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex) => Diagram cIndex mIndex oIndex c m o -> Diagram cLim mLim oLim c m o
    unprojectBase :: forall c m o cLim mLim oLim cIndex mIndex oIndex.
CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex =>
Diagram cIndex mIndex oIndex c m o -> Diagram cLim mLim oLim c m o
unprojectBase = 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.
CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex =>
Diagram cIndex mIndex oIndex c m o -> Diagram c m o cLim mLim oLim
projectBase

    -- | Computes efficiently limits thanks to products and equalizers. Can be used to instantiate 'CompleteCategory'.

    --

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

    --

    -- Most of the time, the original category takes one type parameter and the function uses 'Projection', 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 {Projection 1 -> Projection 2}.

    limitFromProductsAndEqualizers :: 
       (Category c m o, Morphism m o,
        Category cLim mLim oLim, Morphism mLim oLim, Eq cLim, Eq mLim, Eq oLim, HasProducts c m o cLim mLim oLim oIndex,HasEqualizers 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 -> Cone cIndex mIndex oIndex cLim mLim oLim
    limitFromProductsAndEqualizers :: forall c m o cLim mLim oLim oIndex cIndex mIndex.
(Category c m o, Morphism m o, Category cLim mLim oLim,
 Morphism mLim oLim, Eq cLim, Eq mLim, Eq oLim,
 HasProducts c m o cLim mLim oLim oIndex,
 HasEqualizers 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
-> Cone cIndex mIndex oIndex cLim mLim oLim
limitFromProductsAndEqualizers m -> mLim
transformMorphismIntoLimMorphism Diagram cIndex mIndex oIndex c m o
diag = CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
lim
            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
topObjects, 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
topObjects], mmap :: Map (StarIdentity oIndex) m
mmap = AssociationList (StarIdentity oIndex) m
-> Map (StarIdentity oIndex) m
forall k v. AssociationList k v -> Map k v
weakMap[]}
                topObjects :: Set oIndex
topObjects = (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 oIndex
o (mIndex -> oIndex
forall m o. Morphism m o => m -> o
source mIndex
m) | mIndex
m <- cIndex -> oIndex -> Set mIndex
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arTo cIndex
idxCat oIndex
o]) (cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob cIndex
idxCat)
                objectToAMorphismFromATopObject :: oIndex -> mIndex
objectToAMorphismFromATopObject oIndex
o
                    | oIndex
o oIndex -> Set oIndex -> Bool
forall a. Eq a => a -> Set a -> Bool
`Set.elem` Set oIndex
topObjects = 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
arTo cIndex
idxCat oIndex
o, mIndex -> oIndex
forall m o. Morphism m o => m -> o
source mIndex
m oIndex -> Set oIndex -> Bool
forall a. Eq a => a -> Set a -> Bool
`Set.elem` Set oIndex
topObjects]
                prod :: Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
prod = Diagram
  (DiscreteCategory oIndex) (StarIdentity oIndex) oIndex c m o
-> Cone
     (DiscreteCategory oIndex)
     (StarIdentity oIndex)
     oIndex
     cLim
     mLim
     oLim
forall c m o cLim mLim oLim oIndex.
HasProducts c m o cLim mLim oLim oIndex =>
Diagram
  (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     cLim
     mLim
     oLim
Math.CompleteCategory.product 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 (Cone
  (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) =>
Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCone Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
prod)), 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
transformMorphismIntoLimMorphism (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
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
undiscrete = oLim
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
-> CommaObject
     oLim
     One
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> oLim
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
prod) (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
  (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 (Cone
  (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) =>
Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCone Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
prod)) (Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> oLim
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
prod)) Diagram cIndex mIndex oIndex cLim mLim oLim
newDiag (Set (oIndex, mLim) -> Map oIndex mLim
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(oIndex
o,(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
objectToAMorphismFromATopObject oIndex
o)) mLim -> mLim -> mLim
forall m o. Morphism m o => m -> m -> m
@ ((Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (StarIdentity oIndex)
     oIndex
     cLim
     mLim
     oLim
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone
  (DiscreteCategory oIndex)
  (StarIdentity oIndex)
  oIndex
  cLim
  mLim
  oLim
prod) 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
source (mIndex -> oIndex) -> mIndex -> oIndex
forall a b. (a -> b) -> a -> b
$ oIndex -> mIndex
objectToAMorphismFromATopObject 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)]))
                equalizeFromMorph :: mIndex
-> CommaObject
     oLim
     One
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> CommaObject
     oLim
     One
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
equalizeFromMorph mIndex
fIndex CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currLim = oLim
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
-> CommaObject
     oLim
     One
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (Cone Parallel ParallelAr ParallelOb cLim mLim oLim -> oLim
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone Parallel ParallelAr ParallelOb cLim mLim oLim
eq) ((CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currLim) 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
@ (mLim -> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
diagonal (Cone Parallel ParallelAr ParallelOb cLim mLim oLim
-> NaturalTransformation
     Parallel ParallelAr ParallelOb cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone Parallel ParallelAr ParallelOb cLim mLim oLim
eq 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
ParallelA)))
                    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
                        eq :: Cone Parallel ParallelAr ParallelOb cLim mLim oLim
eq = Diagram Parallel ParallelAr ParallelOb cLim mLim oLim
-> Cone Parallel ParallelAr ParallelOb cLim mLim oLim
forall c m o.
HasEqualizers c m o =>
Diagram Parallel ParallelAr ParallelOb c m o
-> Cone Parallel ParallelAr ParallelOb c m o
equalize (Diagram Parallel ParallelAr ParallelOb cLim mLim oLim
 -> Cone Parallel ParallelAr ParallelOb cLim mLim oLim)
-> Diagram Parallel ParallelAr ParallelOb cLim mLim oLim
-> Cone 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
  oLim
  One
  (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) =>
Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCone CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currLim), 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
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currLim) 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)),(ParallelAr
ParallelG, (m -> mLim
transformMorphismIntoLimMorphism m
f) mLim -> mLim -> mLim
forall m o. Morphism m o => m -> m -> m
@ ((CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> NaturalTransformation cIndex mIndex oIndex cLim mLim oLim
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
currLim) 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)))]}
                        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
  oLim
  One
  (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) =>
Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCone CommaObject
  oLim
  One
  (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
  oLim
  One
  (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) =>
Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCone CommaObject
  oLim
  One
  (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)))
                lim :: CommaObject
  oLim
  One
  (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
lim = (mIndex
 -> CommaObject
      oLim
      One
      (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
 -> CommaObject
      oLim
      One
      (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim))
-> CommaObject
     oLim
     One
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> Set mIndex
-> CommaObject
     oLim
     One
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr mIndex
-> CommaObject
     oLim
     One
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
-> CommaObject
     oLim
     One
     (NaturalTransformation cIndex mIndex oIndex cLim mLim oLim)
equalizeFromMorph CommaObject
  oLim
  One
  (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 (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)))