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

{-| Module  : FiniteCategories
Description : A 'LimitCategory' is the category in which lives the limit of a diagram in 'FinCat'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'LimitCategory' is the category in which the limit of a diagram in 'FinCat' lives. To compute limits in a usual category, see Math.CompleteCategory. To compute limits in a custom 'FiniteCategory', see 'limits' in Math.ConeCategory.
-}

module Math.FiniteCategories.LimitCategory
(
    -- * Limit category

    LimitCategory(..),
    
)
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.FiniteCategories.DiscreteTwo
    import              Math.CompleteCategory
    import              Math.CartesianClosedCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.FinCat
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    
        
    instance (Morphism m o, Eq m, Eq oIndex) => Morphism (Limit oIndex m) (Limit oIndex o) where
        source :: Limit oIndex m -> Limit oIndex o
source (Projection m
m) = o -> Limit oIndex o
forall oIndex t. t -> Limit oIndex t
Projection (m -> o
forall m o. Morphism m o => m -> o
source m
m)
        source (ProductElement Map oIndex m
tuple) = Map oIndex o -> Limit oIndex o
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (m -> o
forall m o. Morphism m o => m -> o
source (m -> o) -> Map oIndex m -> Map oIndex o
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map oIndex m
tuple)
        target :: Limit oIndex m -> Limit oIndex o
target (Projection m
m) = o -> Limit oIndex o
forall oIndex t. t -> Limit oIndex t
Projection (m -> o
forall m o. Morphism m o => m -> o
target m
m)
        target (ProductElement Map oIndex m
tuple) = Map oIndex o -> Limit oIndex o
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (m -> o
forall m o. Morphism m o => m -> o
target (m -> o) -> Map oIndex m -> Map oIndex o
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map oIndex m
tuple)
        (Projection m
m2) @ :: Limit oIndex m -> Limit oIndex m -> Limit oIndex m
@ (Projection m
m1) = m -> Limit oIndex m
forall oIndex t. t -> Limit oIndex t
Projection (m -> Limit oIndex m) -> m -> Limit oIndex m
forall a b. (a -> b) -> a -> b
$ m
m2 m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
m1
        (ProductElement Map oIndex m
tuple2) @ (ProductElement Map oIndex m
tuple1) = Map oIndex m -> Limit oIndex m
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (Map oIndex m -> Limit oIndex m) -> Map oIndex m -> Limit oIndex m
forall a b. (a -> b) -> a -> b
$ Set (oIndex, m) -> Map oIndex m
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(oIndex
k1,(Map oIndex m
tuple2 Map oIndex m -> oIndex -> m
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
k1) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
v1) | (oIndex
k1,m
v1) <- Map oIndex m -> Set (oIndex, m)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map oIndex m
tuple1]
        Limit oIndex m
_ @ Limit oIndex m
_ = [Char] -> Limit oIndex m
forall a. HasCallStack => [Char] -> a
error [Char]
"Incompatible composition of Limit morphisms."
    
    -- | A 'LimitCategory' is either a 'ProjectedCategory' (an original category) or a 'LimitCategory'.

    data LimitCategory cIndex mIndex oIndex c m o = ProjectedCategory c -- ^ An original category in 'FinCat' with the indexing object of the category.

                                                  | LimitCategory (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c)     -- ^ The limit category of a given 'Diagram'.

        deriving (LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o -> Bool
(LimitCategory cIndex mIndex oIndex c m o
 -> LimitCategory cIndex mIndex oIndex c m o -> Bool)
-> (LimitCategory cIndex mIndex oIndex c m o
    -> LimitCategory cIndex mIndex oIndex c m o -> Bool)
-> Eq (LimitCategory cIndex mIndex oIndex c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall cIndex mIndex oIndex c m o.
(Eq c, Eq cIndex, Eq mIndex, Eq oIndex, Eq m, Eq o,
 FiniteCategory c m o, FiniteCategory cIndex mIndex oIndex,
 Morphism m o, Morphism mIndex oIndex) =>
LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o -> Bool
$c== :: forall cIndex mIndex oIndex c m o.
(Eq c, Eq cIndex, Eq mIndex, Eq oIndex, Eq m, Eq o,
 FiniteCategory c m o, FiniteCategory cIndex mIndex oIndex,
 Morphism m o, Morphism mIndex oIndex) =>
LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o -> Bool
== :: LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o -> Bool
$c/= :: forall cIndex mIndex oIndex c m o.
(Eq c, Eq cIndex, Eq mIndex, Eq oIndex, Eq m, Eq o,
 FiniteCategory c m o, FiniteCategory cIndex mIndex oIndex,
 Morphism m o, Morphism mIndex oIndex) =>
LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o -> Bool
/= :: LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o -> Bool
Eq, Int -> LimitCategory cIndex mIndex oIndex c m o -> ShowS
[LimitCategory cIndex mIndex oIndex c m o] -> ShowS
LimitCategory cIndex mIndex oIndex c m o -> [Char]
(Int -> LimitCategory cIndex mIndex oIndex c m o -> ShowS)
-> (LimitCategory cIndex mIndex oIndex c m o -> [Char])
-> ([LimitCategory cIndex mIndex oIndex c m o] -> ShowS)
-> Show (LimitCategory cIndex mIndex oIndex c m o)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
forall cIndex mIndex oIndex c m o.
(Show c, Show cIndex, Show oIndex, Show mIndex, Show o, Show m) =>
Int -> LimitCategory cIndex mIndex oIndex c m o -> ShowS
forall cIndex mIndex oIndex c m o.
(Show c, Show cIndex, Show oIndex, Show mIndex, Show o, Show m) =>
[LimitCategory cIndex mIndex oIndex c m o] -> ShowS
forall cIndex mIndex oIndex c m o.
(Show c, Show cIndex, Show oIndex, Show mIndex, Show o, Show m) =>
LimitCategory cIndex mIndex oIndex c m o -> [Char]
$cshowsPrec :: forall cIndex mIndex oIndex c m o.
(Show c, Show cIndex, Show oIndex, Show mIndex, Show o, Show m) =>
Int -> LimitCategory cIndex mIndex oIndex c m o -> ShowS
showsPrec :: Int -> LimitCategory cIndex mIndex oIndex c m o -> ShowS
$cshow :: forall cIndex mIndex oIndex c m o.
(Show c, Show cIndex, Show oIndex, Show mIndex, Show o, Show m) =>
LimitCategory cIndex mIndex oIndex c m o -> [Char]
show :: LimitCategory cIndex mIndex oIndex c m o -> [Char]
$cshowList :: forall cIndex mIndex oIndex c m o.
(Show c, Show cIndex, Show oIndex, Show mIndex, Show o, Show m) =>
[LimitCategory cIndex mIndex oIndex c m o] -> ShowS
showList :: [LimitCategory cIndex mIndex oIndex c m o] -> ShowS
Show, (forall x.
 LimitCategory cIndex mIndex oIndex c m o
 -> Rep (LimitCategory cIndex mIndex oIndex c m o) x)
-> (forall x.
    Rep (LimitCategory cIndex mIndex oIndex c m o) x
    -> LimitCategory cIndex mIndex oIndex c m o)
-> Generic (LimitCategory cIndex mIndex oIndex c m o)
forall x.
Rep (LimitCategory cIndex mIndex oIndex c m o) x
-> LimitCategory cIndex mIndex oIndex c m o
forall x.
LimitCategory cIndex mIndex oIndex c m o
-> Rep (LimitCategory cIndex mIndex oIndex c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall cIndex mIndex oIndex c m o x.
Rep (LimitCategory cIndex mIndex oIndex c m o) x
-> LimitCategory cIndex mIndex oIndex c m o
forall cIndex mIndex oIndex c m o x.
LimitCategory cIndex mIndex oIndex c m o
-> Rep (LimitCategory cIndex mIndex oIndex c m o) x
$cfrom :: forall cIndex mIndex oIndex c m o x.
LimitCategory cIndex mIndex oIndex c m o
-> Rep (LimitCategory cIndex mIndex oIndex c m o) x
from :: forall x.
LimitCategory cIndex mIndex oIndex c m o
-> Rep (LimitCategory cIndex mIndex oIndex c m o) x
$cto :: forall cIndex mIndex oIndex c m o x.
Rep (LimitCategory cIndex mIndex oIndex c m o) x
-> LimitCategory cIndex mIndex oIndex c m o
to :: forall x.
Rep (LimitCategory cIndex mIndex oIndex c m o) x
-> LimitCategory cIndex mIndex oIndex c m o
Generic, LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o
(LimitCategory cIndex mIndex oIndex c m o
 -> LimitCategory cIndex mIndex oIndex c m o)
-> Simplifiable (LimitCategory cIndex mIndex oIndex c m o)
forall a. (a -> a) -> Simplifiable a
forall cIndex mIndex oIndex c m o.
(Simplifiable c, Simplifiable cIndex, Simplifiable oIndex,
 Simplifiable mIndex, Simplifiable o, Simplifiable m, Eq o, Eq m,
 Eq oIndex, Eq mIndex) =>
LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o
$csimplify :: forall cIndex mIndex oIndex c m o.
(Simplifiable c, Simplifiable cIndex, Simplifiable oIndex,
 Simplifiable mIndex, Simplifiable o, Simplifiable m, Eq o, Eq m,
 Eq oIndex, Eq mIndex) =>
LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o
simplify :: LimitCategory cIndex mIndex oIndex c m o
-> LimitCategory cIndex mIndex oIndex c m o
Simplifiable, Int
-> Int
-> [Char]
-> LimitCategory cIndex mIndex oIndex c m o
-> [Char]
Int -> LimitCategory cIndex mIndex oIndex c m o -> [Char]
(Int -> LimitCategory cIndex mIndex oIndex c m o -> [Char])
-> (Int
    -> Int
    -> [Char]
    -> LimitCategory cIndex mIndex oIndex c m o
    -> [Char])
-> (Int -> LimitCategory cIndex mIndex oIndex c m o -> [Char])
-> PrettyPrint (LimitCategory cIndex mIndex oIndex c m o)
forall a.
(Int -> a -> [Char])
-> (Int -> Int -> [Char] -> a -> [Char])
-> (Int -> a -> [Char])
-> PrettyPrint a
forall cIndex mIndex oIndex c m o.
(PrettyPrint c, PrettyPrint cIndex, PrettyPrint oIndex,
 PrettyPrint mIndex, PrettyPrint o, PrettyPrint m, Eq o, Eq m,
 Eq oIndex, Eq c, Eq mIndex, FiniteCategory c m o, Morphism m o) =>
Int
-> Int
-> [Char]
-> LimitCategory cIndex mIndex oIndex c m o
-> [Char]
forall cIndex mIndex oIndex c m o.
(PrettyPrint c, PrettyPrint cIndex, PrettyPrint oIndex,
 PrettyPrint mIndex, PrettyPrint o, PrettyPrint m, Eq o, Eq m,
 Eq oIndex, Eq c, Eq mIndex, FiniteCategory c m o, Morphism m o) =>
Int -> LimitCategory cIndex mIndex oIndex c m o -> [Char]
$cpprint :: forall cIndex mIndex oIndex c m o.
(PrettyPrint c, PrettyPrint cIndex, PrettyPrint oIndex,
 PrettyPrint mIndex, PrettyPrint o, PrettyPrint m, Eq o, Eq m,
 Eq oIndex, Eq c, Eq mIndex, FiniteCategory c m o, Morphism m o) =>
Int -> LimitCategory cIndex mIndex oIndex c m o -> [Char]
pprint :: Int -> LimitCategory cIndex mIndex oIndex c m o -> [Char]
$cpprintWithIndentations :: forall cIndex mIndex oIndex c m o.
(PrettyPrint c, PrettyPrint cIndex, PrettyPrint oIndex,
 PrettyPrint mIndex, PrettyPrint o, PrettyPrint m, Eq o, Eq m,
 Eq oIndex, Eq c, Eq mIndex, FiniteCategory c m o, Morphism m o) =>
Int
-> Int
-> [Char]
-> LimitCategory cIndex mIndex oIndex c m o
-> [Char]
pprintWithIndentations :: Int
-> Int
-> [Char]
-> LimitCategory cIndex mIndex oIndex c m o
-> [Char]
$cpprintIndent :: forall cIndex mIndex oIndex c m o.
(PrettyPrint c, PrettyPrint cIndex, PrettyPrint oIndex,
 PrettyPrint mIndex, PrettyPrint o, PrettyPrint m, Eq o, Eq m,
 Eq oIndex, Eq c, Eq mIndex, FiniteCategory c m o, Morphism m o) =>
Int -> LimitCategory cIndex mIndex oIndex c m o -> [Char]
pprintIndent :: Int -> LimitCategory cIndex mIndex oIndex c m o -> [Char]
PrettyPrint)    

    
    instance (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq mIndex, Eq oIndex,
              Category c m o, Morphism m o, Eq m, Eq o) => Category (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o) where
        identity :: Morphism (Limit oIndex m) (Limit oIndex o) =>
LimitCategory cIndex mIndex oIndex c m o
-> Limit oIndex o -> Limit oIndex m
identity (ProjectedCategory c
c) (Projection o
o) = m -> Limit oIndex m
forall oIndex t. t -> Limit oIndex t
Projection (m -> Limit oIndex m) -> m -> Limit oIndex m
forall a b. (a -> b) -> a -> b
$ c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
o
        identity (LimitCategory Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
_) (Projection o
_) = [Char] -> Limit oIndex m
forall a. HasCallStack => [Char] -> a
error [Char]
"Identity in a limit category on a projected object."
        identity (ProjectedCategory c
_) (ProductElement Map oIndex o
_) = [Char] -> Limit oIndex m
forall a. HasCallStack => [Char] -> a
error [Char]
"Identity in a projected category on a limit object."
        identity (LimitCategory Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag) (ProductElement Map oIndex o
tupleObj) 
            | Set oIndex
topObjects Set oIndex -> Set oIndex -> Bool
forall a. Eq a => a -> a -> Bool
/= Map oIndex o -> Set oIndex
forall k a. Map k a -> Set k
domain Map oIndex o
tupleObj = [Char] -> Limit oIndex m
forall a. HasCallStack => [Char] -> a
error [Char]
"Identity in a limit category on a limit object with different indexing objects."
            | Bool
otherwise = Map oIndex m -> Limit oIndex m
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (Map oIndex m -> Limit oIndex m) -> Map oIndex m -> Limit oIndex m
forall a b. (a -> b) -> a -> b
$ Set (oIndex, m) -> Map oIndex m
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(oIndex
k,c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> oIndex -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
k) (Map oIndex o
tupleObj Map oIndex o -> oIndex -> o
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
k)) | oIndex
k <- Set oIndex
topObjects]
            where
                idxCat :: cIndex
idxCat = (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)
                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)
         
        ar :: Morphism (Limit oIndex m) (Limit oIndex o) =>
LimitCategory cIndex mIndex oIndex c m o
-> Limit oIndex o -> Limit oIndex o -> Set (Limit oIndex m)
ar (ProjectedCategory c
c) (Projection o
s) (Projection o
t) = m -> Limit oIndex m
forall oIndex t. t -> Limit oIndex t
Projection (m -> Limit oIndex m) -> Set m -> Set (Limit oIndex m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s o
t
        ar (ProjectedCategory c
_) (Projection o
_) (ProductElement Map oIndex o
_) = [Char] -> Set (Limit oIndex m)
forall a. HasCallStack => [Char] -> a
error [Char]
"Ar in a projected category where the target is a limit object."
        ar (ProjectedCategory c
_) (ProductElement Map oIndex o
_) (Projection o
_) = [Char] -> Set (Limit oIndex m)
forall a. HasCallStack => [Char] -> a
error [Char]
"Ar in a projected category where the source is a limit object."
        ar (ProjectedCategory c
_) (ProductElement Map oIndex o
_) (ProductElement Map oIndex o
_) = [Char] -> Set (Limit oIndex m)
forall a. HasCallStack => [Char] -> a
error [Char]
"Ar in a projected category where the source and the target are limit objects."
        ar (LimitCategory Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
_) (Projection o
_) (Projection o
_) = [Char] -> Set (Limit oIndex m)
forall a. HasCallStack => [Char] -> a
error [Char]
"Ar in a limit category where the source and target are projected objects."
        ar (LimitCategory Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
_) (Projection o
_) (ProductElement Map oIndex o
_) = [Char] -> Set (Limit oIndex m)
forall a. HasCallStack => [Char] -> a
error [Char]
"Ar in a limit category where the source is a projected object."
        ar (LimitCategory Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
_) (ProductElement Map oIndex o
_) (Projection o
_) = [Char] -> Set (Limit oIndex m)
forall a. HasCallStack => [Char] -> a
error [Char]
"Ar in a limit category where the target is a projected object."
        ar (LimitCategory Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag) (ProductElement Map oIndex o
tupleSource) (ProductElement Map oIndex o
tupleTarget)
            | Set oIndex
topObjects Set oIndex -> Set oIndex -> Bool
forall a. Eq a => a -> a -> Bool
/= Map oIndex o -> Set oIndex
forall k a. Map k a -> Set k
domain Map oIndex o
tupleSource Bool -> Bool -> Bool
|| Set oIndex
topObjects Set oIndex -> Set oIndex -> Bool
forall a. Eq a => a -> a -> Bool
/= Map oIndex o -> Set oIndex
forall k a. Map k a -> Set k
domain Map oIndex o
tupleTarget = [Char] -> Set (Limit oIndex m)
forall a. HasCallStack => [Char] -> a
error [Char]
"Ar in a limit category where the source and target limit objects don't have the same indexing objects."
            | Bool
otherwise = (Limit oIndex m -> Bool)
-> Set (Limit oIndex m) -> Set (Limit oIndex m)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Limit oIndex m -> Bool
filterProduct Set (Limit oIndex m)
products
            where
                products :: Set (Limit oIndex m)
products = Map oIndex m -> Limit oIndex m
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (Map oIndex m -> Limit oIndex m)
-> ([(oIndex, m)] -> Map oIndex m)
-> [(oIndex, m)]
-> Limit oIndex m
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(oIndex, m)] -> Map oIndex m
forall k v. AssociationList k v -> Map k v
weakMap ([(oIndex, m)] -> Limit oIndex m)
-> Set [(oIndex, m)] -> Set (Limit oIndex m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Set (oIndex, m)] -> Set [(oIndex, m)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets [(\m
x -> (oIndex
k,m
x)) (m -> (oIndex, m)) -> Set m -> Set (oIndex, m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> oIndex -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
k) (Map oIndex o
tupleSource Map oIndex o -> oIndex -> o
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
k) (Map oIndex o
tupleTarget Map oIndex o -> oIndex -> o
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
k) | oIndex
k <- Set oIndex -> [oIndex]
forall a. Eq a => Set a -> [a]
Set.setToList Set oIndex
topObjects]
                idxCat :: cIndex
idxCat = (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)
                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]
                filterProduct :: Limit oIndex m -> Bool
filterProduct (ProductElement Map oIndex m
tupleMorph) = Set Bool -> Bool
Set.and [(Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
i)) FinFunctor c m o -> m -> 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
->£ (Map oIndex m
tupleMorph Map oIndex m -> oIndex -> m
forall k v. Eq k => Map k v -> k -> v
|!| (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
i)) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
m) FinFunctor c m o -> m -> 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
->£ (Map oIndex m
tupleMorph Map oIndex m -> oIndex -> m
forall k v. Eq k => Map k v -> k -> v
|!| (mIndex -> oIndex
forall m o. Morphism m o => m -> o
source (mIndex -> oIndex) -> mIndex -> oIndex
forall a b. (a -> b) -> a -> b
$ mIndex
m)) | oIndex
i <- (cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob cIndex
idxCat), oIndex
s <- Set oIndex
topObjects, mIndex
m <- cIndex -> oIndex -> oIndex -> Set mIndex
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> o -> Set m
arWithoutId cIndex
idxCat oIndex
s (mIndex -> oIndex
forall m o. Morphism m o => m -> o
target (mIndex -> oIndex) -> mIndex -> oIndex
forall a b. (a -> b) -> a -> b
$ oIndex -> mIndex
objectToAMorphismFromATopObject oIndex
i)]
            
            
    instance (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq mIndex, Eq oIndex,
              FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FiniteCategory (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o) where
        ob :: LimitCategory cIndex mIndex oIndex c m o -> Set (Limit oIndex o)
ob (ProjectedCategory c
cat) = o -> Limit oIndex o
forall oIndex t. t -> Limit oIndex t
Projection (o -> Limit oIndex o) -> Set o -> Set (Limit oIndex o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat
        ob (LimitCategory Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag) = (Limit oIndex o -> Bool)
-> Set (Limit oIndex o) -> Set (Limit oIndex o)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Limit oIndex o -> Bool
filterProduct Set (Limit oIndex o)
products
            where
                products :: Set (Limit oIndex o)
products = Map oIndex o -> Limit oIndex o
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (Map oIndex o -> Limit oIndex o)
-> ([(oIndex, o)] -> Map oIndex o)
-> [(oIndex, o)]
-> Limit oIndex o
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(oIndex, o)] -> Map oIndex o
forall k v. AssociationList k v -> Map k v
weakMap ([(oIndex, o)] -> Limit oIndex o)
-> Set [(oIndex, o)] -> Set (Limit oIndex o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Set (oIndex, o)] -> Set [(oIndex, o)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets (Set (Set (oIndex, o)) -> [Set (oIndex, o)]
forall a. Eq a => Set a -> [a]
Set.setToList [(\o
x -> (oIndex
k,o
x)) (o -> (oIndex, o)) -> Set o -> Set (oIndex, o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> oIndex -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
k) | oIndex
k <- Set oIndex
topObjects])
                idxCat :: cIndex
idxCat = (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)
                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]
                filterProduct :: Limit oIndex o -> Bool
filterProduct (ProductElement Map oIndex o
tupleObj) = Set Bool -> Bool
Set.and [(Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
i)) FinFunctor c m o -> o -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ (Map oIndex o
tupleObj Map oIndex o -> oIndex -> o
forall k v. Eq k => Map k v -> k -> v
|!| (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
i)) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
m) FinFunctor c m o -> o -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ (Map oIndex o
tupleObj Map oIndex o -> oIndex -> o
forall k v. Eq k => Map k v -> k -> v
|!| (mIndex -> oIndex
forall m o. Morphism m o => m -> o
source (mIndex -> oIndex) -> mIndex -> oIndex
forall a b. (a -> b) -> a -> b
$ mIndex
m)) | oIndex
i <- (cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob cIndex
idxCat), oIndex
s <- Set oIndex
topObjects, mIndex
m <- cIndex -> oIndex -> oIndex -> Set mIndex
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> o -> Set m
arWithoutId cIndex
idxCat oIndex
s (mIndex -> oIndex
forall m o. Morphism m o => m -> o
target (mIndex -> oIndex) -> mIndex -> oIndex
forall a b. (a -> b) -> a -> b
$ oIndex -> mIndex
objectToAMorphismFromATopObject oIndex
i)]
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o,
              FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => 
        CompleteCategory (FinCat c m o) (FinFunctor c m o) c (FinCat (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (FinFunctor (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (LimitCategory cIndex mIndex oIndex c m o) cIndex mIndex oIndex where
        
        limit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Cone
     cIndex
     mIndex
     oIndex
     (FinCat
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (FinFunctor
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (LimitCategory cIndex mIndex oIndex c m o)
limit Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag = LimitCategory cIndex mIndex oIndex c m o
-> NaturalTransformation
     cIndex
     mIndex
     oIndex
     (FinCat
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (FinFunctor
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (LimitCategory cIndex mIndex oIndex c m o)
-> Cone
     cIndex
     mIndex
     oIndex
     (FinCat
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (FinFunctor
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (LimitCategory cIndex mIndex oIndex c m o)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone LimitCategory cIndex mIndex oIndex c m o
apex NaturalTransformation
  cIndex
  mIndex
  oIndex
  (FinCat
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (FinFunctor
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
nat
            where
                apex :: LimitCategory cIndex mIndex oIndex c m o
apex = Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> LimitCategory cIndex mIndex oIndex c m o
forall cIndex mIndex oIndex c m o.
Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> LimitCategory cIndex mIndex oIndex c m o
LimitCategory Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag
                newDiag :: Diagram
  cIndex
  mIndex
  oIndex
  (FinCat c m o)
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
newDiag = Diagram {src :: cIndex
src = Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag, tgt :: FinCat c m o
tgt = FinCat c m o
forall c m o. FinCat c m o
FinCat, omap :: Map oIndex (LimitCategory cIndex mIndex oIndex c m o)
omap = Map oIndex (LimitCategory cIndex mIndex oIndex c m o)
forall {cIndex} {mIndex} {oIndex} {m} {o}.
Map oIndex (LimitCategory cIndex mIndex oIndex c m o)
newOmap, mmap :: Map
  mIndex
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
mmap = Map
  mIndex
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
forall {cIndex} {mIndex} {oIndex} {m} {o} {oIndex} {oIndex}
       {cIndex} {mIndex} {oIndex} {m} {o} {oIndex} {oIndex}.
Map
  mIndex
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
newMmap}
                newOmap :: Map oIndex (LimitCategory cIndex mIndex oIndex c m o)
newOmap = Set (oIndex, LimitCategory cIndex mIndex oIndex c m o)
-> Map oIndex (LimitCategory cIndex mIndex oIndex c m o)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
k, c -> LimitCategory cIndex mIndex oIndex c m o
forall cIndex mIndex oIndex c m o.
c -> LimitCategory cIndex mIndex oIndex c m o
ProjectedCategory c
v) | (oIndex
k,c
v) <- (Map oIndex c -> Set (oIndex, c)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet (Map oIndex c -> Set (oIndex, c))
-> Map oIndex c -> Set (oIndex, c)
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Map oIndex c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)]
                newMmap :: Map
  mIndex
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
newMmap = Set
  (mIndex,
   Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
-> Map
     mIndex
     (Diagram
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o)
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(mIndex
k, FinFunctor c m o
-> Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
forall {o1} {t} {c1} {c2} {t} {o2} {cIndex} {mIndex} {oIndex} {m}
       {o} {oIndex} {oIndex} {cIndex} {mIndex} {oIndex} {m} {o} {oIndex}
       {oIndex}.
(Eq o1, Eq t) =>
Diagram c1 t o1 c2 t o2
-> Diagram
     (LimitCategory cIndex mIndex oIndex c1 m o)
     (Limit oIndex t)
     (Limit oIndex o1)
     (LimitCategory cIndex mIndex oIndex c2 m o)
     (Limit oIndex t)
     (Limit oIndex o2)
transformDiagramToProjectedDiagram FinFunctor c m o
v) | (mIndex
k,FinFunctor c m o
v) <- (Map mIndex (FinFunctor c m o) -> Set (mIndex, FinFunctor c m o)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet (Map mIndex (FinFunctor c m o) -> Set (mIndex, FinFunctor c m o))
-> Map mIndex (FinFunctor c m o) -> Set (mIndex, FinFunctor c m o)
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Map mIndex (FinFunctor c m o)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)]
                transformDiagramToProjectedDiagram :: Diagram c1 t o1 c2 t o2
-> Diagram
     (LimitCategory cIndex mIndex oIndex c1 m o)
     (Limit oIndex t)
     (Limit oIndex o1)
     (LimitCategory cIndex mIndex oIndex c2 m o)
     (Limit oIndex t)
     (Limit oIndex o2)
transformDiagramToProjectedDiagram Diagram c1 t o1 c2 t o2
diag_ = Diagram{src :: LimitCategory cIndex mIndex oIndex c1 m o
src = c1 -> LimitCategory cIndex mIndex oIndex c1 m o
forall cIndex mIndex oIndex c m o.
c -> LimitCategory cIndex mIndex oIndex c m o
ProjectedCategory (Diagram c1 t o1 c2 t o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 t o1 c2 t o2
diag_), tgt :: LimitCategory cIndex mIndex oIndex c2 m o
tgt = c2 -> LimitCategory cIndex mIndex oIndex c2 m o
forall cIndex mIndex oIndex c m o.
c -> LimitCategory cIndex mIndex oIndex c m o
ProjectedCategory (Diagram c1 t o1 c2 t o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 t o1 c2 t o2
diag_), omap :: Map (Limit oIndex o1) (Limit oIndex o2)
omap = Map o1 o2 -> Map (Limit oIndex o1) (Limit oIndex o2)
forall {t} {t} {oIndex} {oIndex}.
Eq t =>
Map t t -> Map (Limit oIndex t) (Limit oIndex t)
transformOmapToProjectedOmap (Diagram c1 t o1 c2 t o2 -> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 t o1 c2 t o2
diag_), mmap :: Map (Limit oIndex t) (Limit oIndex t)
mmap = Map t t -> Map (Limit oIndex t) (Limit oIndex t)
forall {t} {t} {oIndex} {oIndex}.
Eq t =>
Map t t -> Map (Limit oIndex t) (Limit oIndex t)
transformMmapToProjectedMmap (Diagram c1 t o1 c2 t o2 -> Map t t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c1 t o1 c2 t o2
diag_)}
                transformOmapToProjectedOmap :: Map t t -> Map (Limit oIndex t) (Limit oIndex t)
transformOmapToProjectedOmap Map t t
om = Set (Limit oIndex t, Limit oIndex t)
-> Map (Limit oIndex t) (Limit oIndex t)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
o1, t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
o2) | (t
o1,t
o2) <- (Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map t t
om)]
                transformMmapToProjectedMmap :: Map t t -> Map (Limit oIndex t) (Limit oIndex t)
transformMmapToProjectedMmap Map t t
mm = Set (Limit oIndex t, Limit oIndex t)
-> Map (Limit oIndex t) (Limit oIndex t)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
m1, t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
m2) | (t
m1,t
m2) <- (Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map t t
mm)]
                nat :: NaturalTransformation
  cIndex
  mIndex
  oIndex
  (FinCat
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (FinFunctor
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
nat = Diagram
  cIndex
  mIndex
  oIndex
  (FinCat
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (FinFunctor
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
-> Diagram
     cIndex
     mIndex
     oIndex
     (FinCat
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (FinFunctor
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (LimitCategory cIndex mIndex oIndex c m o)
-> Map
     oIndex
     (FinFunctor
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
-> NaturalTransformation
     cIndex
     mIndex
     oIndex
     (FinCat
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (FinFunctor
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (LimitCategory cIndex mIndex oIndex c m o)
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
-> FinCat
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
-> LimitCategory cIndex mIndex oIndex c m o
-> Diagram
     cIndex
     mIndex
     oIndex
     (FinCat
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (FinFunctor
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (LimitCategory cIndex mIndex oIndex c m o)
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 (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag) FinCat
  (LimitCategory cIndex mIndex oIndex c m o)
  (Limit oIndex m)
  (Limit oIndex o)
forall c m o. FinCat c m o
FinCat LimitCategory cIndex mIndex oIndex c m o
apex) Diagram
  cIndex
  mIndex
  oIndex
  (FinCat
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (FinFunctor
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
forall {c} {m} {o} {cIndex} {mIndex} {oIndex} {m} {o} {oIndex}
       {oIndex} {cIndex} {mIndex} {oIndex} {m} {o} {oIndex} {oIndex}
       {cIndex} {mIndex} {oIndex} {m} {o}.
Diagram
  cIndex
  mIndex
  oIndex
  (FinCat c m o)
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
newDiag Map
  oIndex
  (FinFunctor
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
forall {cIndex} {mIndex} {oIndex} {m} {o} {oIndex} {oIndex}.
Map
  oIndex
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
components_
                components_ :: Map
  oIndex
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
components_ = Set
  (oIndex,
   Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
-> Map
     oIndex
     (Diagram
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o)
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
oIndex, oIndex
-> Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
forall {cIndex} {mIndex} {oIndex} {m} {o} {oIndex} {oIndex}.
oIndex
-> Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
leg oIndex
oIndex) | oIndex
oIndex <- (cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob(cIndex -> Set oIndex)
-> (Diagram
      cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
    -> cIndex)
-> Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Set oIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
 -> Set oIndex)
-> Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Set oIndex
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)]
                idxCat :: cIndex
idxCat = (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)
                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]
                leg :: oIndex
-> Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
leg oIndex
oIndex = Diagram{src :: LimitCategory cIndex mIndex oIndex c m o
src = LimitCategory cIndex mIndex oIndex c m o
apex, tgt :: LimitCategory cIndex mIndex oIndex c m o
tgt = c -> LimitCategory cIndex mIndex oIndex c m o
forall cIndex mIndex oIndex c m o.
c -> LimitCategory cIndex mIndex oIndex c m o
ProjectedCategory (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> oIndex -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
oIndex), omap :: Map (Limit oIndex o) (Limit oIndex o)
omap = Set (Limit oIndex o, Limit oIndex o)
-> Map (Limit oIndex o) (Limit oIndex o)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Limit oIndex o
tuple, (o -> Limit oIndex o
forall oIndex t. t -> Limit oIndex t
Projection ((Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
oIndex)) FinFunctor c m o -> o -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ((Limit oIndex o -> Map oIndex o
forall {oIndex} {t}. Limit oIndex t -> Map oIndex t
extractProductObj Limit oIndex o
tuple) Map oIndex o -> oIndex -> o
forall k v. Eq k => Map k v -> k -> v
|!| (mIndex -> oIndex
forall m o. Morphism m o => m -> o
source (oIndex -> mIndex
objectToAMorphismFromATopObject oIndex
oIndex)))))) | Limit oIndex o
tuple <- LimitCategory cIndex mIndex oIndex c m o -> Set (Limit oIndex o)
forall c m o. FiniteCategory c m o => c -> Set o
ob LimitCategory cIndex mIndex oIndex c m o
apex], mmap :: Map (Limit oIndex m) (Limit oIndex m)
mmap = Set (Limit oIndex m, Limit oIndex m)
-> Map (Limit oIndex m) (Limit oIndex m)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Limit oIndex m
tuple, (m -> Limit oIndex m
forall oIndex t. t -> Limit oIndex t
Projection ((Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
oIndex)) FinFunctor c m o -> m -> 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
->£ ((Limit oIndex m -> Map oIndex m
forall {oIndex} {t}. Limit oIndex t -> Map oIndex t
extractProductMorph Limit oIndex m
tuple) Map oIndex m -> oIndex -> m
forall k v. Eq k => Map k v -> k -> v
|!| (mIndex -> oIndex
forall m o. Morphism m o => m -> o
source (oIndex -> mIndex
objectToAMorphismFromATopObject oIndex
oIndex)))))) | Limit oIndex m
tuple <- LimitCategory cIndex mIndex oIndex c m o -> Set (Limit oIndex m)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows LimitCategory cIndex mIndex oIndex c m o
apex]}
                extractProductObj :: Limit oIndex t -> Map oIndex t
extractProductObj (ProductElement Map oIndex t
m) = Map oIndex t
m  
                extractProductMorph :: Limit oIndex t -> Map oIndex t
extractProductMorph (ProductElement Map oIndex t
m) = Map oIndex t
m

        projectBase :: Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Diagram
     (FinCat c m o)
     (FinFunctor c m o)
     c
     (FinCat
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (FinFunctor
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
     (LimitCategory cIndex mIndex oIndex c m o)
projectBase Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag = Diagram
  (FinCat c m o)
  (FinFunctor c m o)
  c
  (FinCat
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (FinFunctor
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
forall {c} {m} {o} {c} {m} {o} {cIndex} {mIndex} {oIndex} {m} {o}
       {oIndex} {oIndex} {cIndex} {mIndex} {oIndex} {m} {o} {oIndex}
       {oIndex} {cIndex} {mIndex} {oIndex} {m} {o}.
Diagram
  (FinCat c m o)
  (FinFunctor c m o)
  c
  (FinCat c m o)
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
newDiag
            where
                newDiag :: Diagram
  (FinCat c m o)
  (FinFunctor c m o)
  c
  (FinCat c m o)
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
  (LimitCategory cIndex mIndex oIndex c m o)
newDiag = Diagram {src :: FinCat c m o
src = FinCat c m o
forall c m o. FinCat c m o
FinCat, tgt :: FinCat c m o
tgt = FinCat c m o
forall c m o. FinCat c m o
FinCat, omap :: Map c (LimitCategory cIndex mIndex oIndex c m o)
omap = Map c (LimitCategory cIndex mIndex oIndex c m o)
forall {cIndex} {mIndex} {oIndex} {m} {o}.
Map c (LimitCategory cIndex mIndex oIndex c m o)
newOmap, mmap :: Map
  (FinFunctor c m o)
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
mmap = Map
  (FinFunctor c m o)
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
forall {cIndex} {mIndex} {oIndex} {m} {o} {oIndex} {oIndex}
       {cIndex} {mIndex} {oIndex} {m} {o} {oIndex} {oIndex}.
Map
  (FinFunctor c m o)
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
newMmap}
                newOmap :: Map c (LimitCategory cIndex mIndex oIndex c m o)
newOmap = Set (c, LimitCategory cIndex mIndex oIndex c m o)
-> Map c (LimitCategory cIndex mIndex oIndex c m o)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(c
v, c -> LimitCategory cIndex mIndex oIndex c m o
forall cIndex mIndex oIndex c m o.
c -> LimitCategory cIndex mIndex oIndex c m o
ProjectedCategory c
v) | (oIndex
k,c
v) <- (Map oIndex c -> Set (oIndex, c)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet (Map oIndex c -> Set (oIndex, c))
-> Map oIndex c -> Set (oIndex, c)
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Map oIndex c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)]
                newMmap :: Map
  (FinFunctor c m o)
  (Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
newMmap = Set
  (FinFunctor c m o,
   Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o))
-> Map
     (FinFunctor c m o)
     (Diagram
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o)
        (LimitCategory cIndex mIndex oIndex c m o)
        (Limit oIndex m)
        (Limit oIndex o))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(FinFunctor c m o
v, FinFunctor c m o
-> Diagram
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
     (LimitCategory cIndex mIndex oIndex c m o)
     (Limit oIndex m)
     (Limit oIndex o)
forall {o1} {t} {c1} {c2} {t} {o2} {cIndex} {mIndex} {oIndex} {m}
       {o} {oIndex} {oIndex} {cIndex} {mIndex} {oIndex} {m} {o} {oIndex}
       {oIndex}.
(Eq o1, Eq t) =>
Diagram c1 t o1 c2 t o2
-> Diagram
     (LimitCategory cIndex mIndex oIndex c1 m o)
     (Limit oIndex t)
     (Limit oIndex o1)
     (LimitCategory cIndex mIndex oIndex c2 m o)
     (Limit oIndex t)
     (Limit oIndex o2)
transformDiagramToProjectedDiagram FinFunctor c m o
v) | (mIndex
k,FinFunctor c m o
v) <- (Map mIndex (FinFunctor c m o) -> Set (mIndex, FinFunctor c m o)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet (Map mIndex (FinFunctor c m o) -> Set (mIndex, FinFunctor c m o))
-> Map mIndex (FinFunctor c m o) -> Set (mIndex, FinFunctor c m o)
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Map mIndex (FinFunctor c m o)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)]
                transformDiagramToProjectedDiagram :: Diagram c1 t o1 c2 t o2
-> Diagram
     (LimitCategory cIndex mIndex oIndex c1 m o)
     (Limit oIndex t)
     (Limit oIndex o1)
     (LimitCategory cIndex mIndex oIndex c2 m o)
     (Limit oIndex t)
     (Limit oIndex o2)
transformDiagramToProjectedDiagram Diagram c1 t o1 c2 t o2
diag_ = Diagram{src :: LimitCategory cIndex mIndex oIndex c1 m o
src = c1 -> LimitCategory cIndex mIndex oIndex c1 m o
forall cIndex mIndex oIndex c m o.
c -> LimitCategory cIndex mIndex oIndex c m o
ProjectedCategory (Diagram c1 t o1 c2 t o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 t o1 c2 t o2
diag_), tgt :: LimitCategory cIndex mIndex oIndex c2 m o
tgt = c2 -> LimitCategory cIndex mIndex oIndex c2 m o
forall cIndex mIndex oIndex c m o.
c -> LimitCategory cIndex mIndex oIndex c m o
ProjectedCategory (Diagram c1 t o1 c2 t o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 t o1 c2 t o2
diag_), omap :: Map (Limit oIndex o1) (Limit oIndex o2)
omap = Map o1 o2 -> Map (Limit oIndex o1) (Limit oIndex o2)
forall {t} {t} {oIndex} {oIndex}.
Eq t =>
Map t t -> Map (Limit oIndex t) (Limit oIndex t)
transformOmapToProjectedOmap (Diagram c1 t o1 c2 t o2 -> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 t o1 c2 t o2
diag_), mmap :: Map (Limit oIndex t) (Limit oIndex t)
mmap = Map t t -> Map (Limit oIndex t) (Limit oIndex t)
forall {t} {t} {oIndex} {oIndex}.
Eq t =>
Map t t -> Map (Limit oIndex t) (Limit oIndex t)
transformMmapToProjectedMmap (Diagram c1 t o1 c2 t o2 -> Map t t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c1 t o1 c2 t o2
diag_)}
                transformOmapToProjectedOmap :: Map t t -> Map (Limit oIndex t) (Limit oIndex t)
transformOmapToProjectedOmap Map t t
om = Set (Limit oIndex t, Limit oIndex t)
-> Map (Limit oIndex t) (Limit oIndex t)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
o1, t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
o2) | (t
o1,t
o2) <- (Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map t t
om)]
                transformMmapToProjectedMmap :: Map t t -> Map (Limit oIndex t) (Limit oIndex t)
transformMmapToProjectedMmap Map t t
mm = Set (Limit oIndex t, Limit oIndex t)
-> Map (Limit oIndex t) (Limit oIndex t)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
m1, t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
m2) | (t
m1,t
m2) <- (Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map t t
mm)]