{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE MonadComprehensions  #-}
{-| Module  : FiniteCategories
Description : Utility functions for set-valued functors.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Kan extensions for set-valued functors. Inspired by DBC of M. Fleming, R. Gunther, R. Rosebrugh.
-}

module Math.Functors.SetValued 
(
    -- * Right Kan extension

    LimitObject(..),
    rightKanSetValued,
    -- ** Formatting

    formatLimitObject,
    formatSetOfLimitObjects,
    formatFunctionOfLimitObjects,
    -- * Left Kan extension

    ColimitObject(..),
    leftKanSetValued,
    -- ** Formatting

    formatColimitObject,
    formatSetOfColimitObjects,
    formatFunctionOfColimitObjects,
)
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              Math.FiniteCategory
    import              Math.Categories.FinSet
    import              Math.Categories.FunctorCategory
    import              Math.Categories.CommaCategory
    import              Math.FiniteCategories.One
    import              Math.IO.PrettyPrint
    
    import              GHC.Base            (maxInt)
    
    -- | A 'LimitObject' is a map from a comma object to an element a, the maps should be seen as elements of the cartesian products indexed by comma objects.

    type LimitObject o1 m2 a = Map (CommaObject One o1 m2) a
    
    -- | Format a 'LimitObject' to be readable.

    formatLimitObject :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => LimitObject o1 m2 a -> String
    formatLimitObject :: forall o1 m2 a.
(Eq o1, Eq m2, Eq a, PrettyPrint a) =>
LimitObject o1 m2 a -> String
formatLimitObject LimitObject o1 m2 a
mapping = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," [ (Int -> a -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
maxInt a
v) | (CommaObject One o1 m2
k,a
v) <- LimitObject o1 m2 a -> AssociationList (CommaObject One o1 m2) a
forall k v. Eq k => Map k v -> AssociationList k v
Map.mapToList LimitObject o1 m2 a
mapping] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    
    -- | Format a set of 'LimitObject's to be readable.

    formatSetOfLimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Set (LimitObject o1 m2 a) -> String
    formatSetOfLimitObjects :: forall o1 m2 a.
(Eq o1, Eq m2, Eq a, PrettyPrint a) =>
Set (LimitObject o1 m2 a) -> String
formatSetOfLimitObjects Set (LimitObject o1 m2 a)
setOfMaps = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," (LimitObject o1 m2 a -> String
forall o1 m2 a.
(Eq o1, Eq m2, Eq a, PrettyPrint a) =>
LimitObject o1 m2 a -> String
formatLimitObject (LimitObject o1 m2 a -> String)
-> [LimitObject o1 m2 a] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (LimitObject o1 m2 a) -> [LimitObject o1 m2 a]
forall a. Eq a => Set a -> [a]
setToList Set (LimitObject o1 m2 a)
setOfMaps) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
    
    -- | Format a 'Function' of 'LimitObject's to be readable.

    formatFunctionOfLimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Function (LimitObject o1 m2 a) -> String
    formatFunctionOfLimitObjects :: forall o1 m2 a.
(Eq o1, Eq m2, Eq a, PrettyPrint a) =>
Function (LimitObject o1 m2 a) -> String
formatFunctionOfLimitObjects Function (LimitObject o1 m2 a)
func = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," [(LimitObject o1 m2 a -> String
forall o1 m2 a.
(Eq o1, Eq m2, Eq a, PrettyPrint a) =>
LimitObject o1 m2 a -> String
formatLimitObject LimitObject o1 m2 a
k) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (LimitObject o1 m2 a -> String
forall o1 m2 a.
(Eq o1, Eq m2, Eq a, PrettyPrint a) =>
LimitObject o1 m2 a -> String
formatLimitObject LimitObject o1 m2 a
v) | (LimitObject o1 m2 a
k,LimitObject o1 m2 a
v) <- (Map (LimitObject o1 m2 a) (LimitObject o1 m2 a)
-> AssociationList (LimitObject o1 m2 a) (LimitObject o1 m2 a)
forall k v. Eq k => Map k v -> AssociationList k v
Map.mapToList (Function (LimitObject o1 m2 a)
-> Map (LimitObject o1 m2 a) (LimitObject o1 m2 a)
forall a. Function a -> Map a a
function Function (LimitObject o1 m2 a)
func))]
    
    -- | Compute the image of the right Kan extension on an object of /B/. The image is a set of maps from the comma objects to elements a (you should see the maps as cartesian products indexed by comma objects).

    rightKanSetValuedObjectwise :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                                    FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                                    Eq a) =>
                                    Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> o2 -> Set (LimitObject o1 m2 a)
    rightKanSetValuedObjectwise :: forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (LimitObject o1 m2 a)
rightKanSetValuedObjectwise Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x o2
b = Set (Map (CommaObject One o1 m2) a)
filteredMaps
        where
            commaCat :: CommaCategory One One One c1 m1 o1 c2 m2 o2
commaCat = CommaCategory{leftDiagram :: Diagram One One One c2 m2 o2
leftDiagram=c2 -> o2 -> Diagram One One One c2 m2 o2
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f) o2
b, rightDiagram :: Diagram c1 m1 o1 c2 m2 o2
rightDiagram=Diagram c1 m1 o1 c2 m2 o2
f}
            allMaps :: Set (Map (CommaObject One o1 m2) a)
allMaps = [(CommaObject One o1 m2, a)] -> Map (CommaObject One o1 m2) a
forall k v. AssociationList k v -> Map k v
weakMap ([(CommaObject One o1 m2, a)] -> Map (CommaObject One o1 m2) a)
-> Set [(CommaObject One o1 m2, a)]
-> Set (Map (CommaObject One o1 m2) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Set (CommaObject One o1 m2, a)]
-> Set [(CommaObject One o1 m2, a)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets([Set (CommaObject One o1 m2, a)]
 -> Set [(CommaObject One o1 m2, a)])
-> (Set (Set (CommaObject One o1 m2, a))
    -> [Set (CommaObject One o1 m2, a)])
-> Set (Set (CommaObject One o1 m2, a))
-> Set [(CommaObject One o1 m2, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set (Set (CommaObject One o1 m2, a))
-> [Set (CommaObject One o1 m2, a)]
forall a. Eq a => Set a -> [a]
setToList (Set (Set (CommaObject One o1 m2, a))
 -> Set [(CommaObject One o1 m2, a)])
-> Set (Set (CommaObject One o1 m2, a))
-> Set [(CommaObject One o1 m2, a)]
forall a b. (a -> b) -> a -> b
$ [[(CommaObject One o1 m2
a, a
elemXa) | a
elemXa <- (Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> o1 -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ (CommaObject One o1 m2 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject One o1 m2
a))] | CommaObject One o1 m2
a <- CommaCategory One One One c1 m1 o1 c2 m2 o2
-> Set (CommaObject One o1 m2)
forall c m o. FiniteCategory c m o => c -> Set o
ob CommaCategory One One One c1 m1 o1 c2 m2 o2
commaCat])
            filters :: [Map (CommaObject One o1 m2) a -> Bool]
filters = [\Map (CommaObject One o1 m2) a
mapping -> ((Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> m1 -> Function a
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
->£(CommaMorphism One o1 One m1 m2 -> m1
forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow CommaMorphism One o1 One m1 m2
m)) Function a -> a -> a
forall a. Eq a => Function a -> a -> a
||!|| (Map (CommaObject One o1 m2) a
mapping Map (CommaObject One o1 m2) a -> CommaObject One o1 m2 -> a
forall k v. Eq k => Map k v -> k -> v
|!| (CommaMorphism One o1 One m1 m2 -> CommaObject One o1 m2
forall m o. Morphism m o => m -> o
source CommaMorphism One o1 One m1 m2
m))) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (Map (CommaObject One o1 m2) a
mapping Map (CommaObject One o1 m2) a -> CommaObject One o1 m2 -> a
forall k v. Eq k => Map k v -> k -> v
|!| (CommaMorphism One o1 One m1 m2 -> CommaObject One o1 m2
forall m o. Morphism m o => m -> o
target CommaMorphism One o1 One m1 m2
m))  | CommaMorphism One o1 One m1 m2
m <- Set (CommaMorphism One o1 One m1 m2)
-> [CommaMorphism One o1 One m1 m2]
forall a. Eq a => Set a -> [a]
setToList (Set (CommaMorphism One o1 One m1 m2)
 -> [CommaMorphism One o1 One m1 m2])
-> Set (CommaMorphism One o1 One m1 m2)
-> [CommaMorphism One o1 One m1 m2]
forall a b. (a -> b) -> a -> b
$ CommaCategory One One One c1 m1 o1 c2 m2 o2
-> Set (CommaMorphism One o1 One m1 m2)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows CommaCategory One One One c1 m1 o1 c2 m2 o2
commaCat]
            filteredMaps :: Set (Map (CommaObject One o1 m2) a)
filteredMaps = ((Map (CommaObject One o1 m2) a -> Bool)
 -> Set (Map (CommaObject One o1 m2) a)
 -> Set (Map (CommaObject One o1 m2) a))
-> Set (Map (CommaObject One o1 m2) a)
-> [Map (CommaObject One o1 m2) a -> Bool]
-> Set (Map (CommaObject One o1 m2) a)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Map (CommaObject One o1 m2) a -> Bool)
-> Set (Map (CommaObject One o1 m2) a)
-> Set (Map (CommaObject One o1 m2) a)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Set (Map (CommaObject One o1 m2) a)
allMaps [Map (CommaObject One o1 m2) a -> Bool]
filters
            
    -- | Compute the image of the right Kan extension on a morphism of /B/.

    rightKanSetValuedObjectwiseMorphism :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                                            FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                                            Eq a) =>
                                            Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> m2 -> Function (LimitObject o1 m2 a)
    rightKanSetValuedObjectwiseMorphism :: forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> m2
-> Function (LimitObject o1 m2 a)
rightKanSetValuedObjectwiseMorphism Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x m2
m = Function (LimitObject o1 m2 a)
result
        where
            precompose :: CommaObject o1 o2 m2 -> CommaObject o1 o2 m2
precompose CommaObject o1 o2 m2
commaObj = o1 -> o2 -> m2 -> CommaObject o1 o2 m2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject (CommaObject o1 o2 m2 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o1 o2 m2
commaObj) (CommaObject o1 o2 m2 -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o1 o2 m2
commaObj) ((CommaObject o1 o2 m2 -> m2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject o1 o2 m2
commaObj) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ m2
m)
            imageSrc :: Set (LimitObject o1 m2 a)
imageSrc = Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (LimitObject o1 m2 a)
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (LimitObject o1 m2 a)
rightKanSetValuedObjectwise Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
m)
            imageTgt :: Set (LimitObject o1 m2 a)
imageTgt = Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (LimitObject o1 m2 a)
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (LimitObject o1 m2 a)
rightKanSetValuedObjectwise Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m)
            commaCat2 :: CommaCategory One One One c1 m1 o1 c2 m2 o2
commaCat2 = CommaCategory{leftDiagram :: Diagram One One One c2 m2 o2
leftDiagram=c2 -> o2 -> Diagram One One One c2 m2 o2
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f) (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m), rightDiagram :: Diagram c1 m1 o1 c2 m2 o2
rightDiagram=Diagram c1 m1 o1 c2 m2 o2
f}
            subsetIndexingObjects :: Set (CommaObject One o1 m2)
subsetIndexingObjects = CommaCategory One One One c1 m1 o1 c2 m2 o2
-> Set (CommaObject One o1 m2)
forall c m o. FiniteCategory c m o => c -> Set o
ob CommaCategory One One One c1 m1 o1 c2 m2 o2
commaCat2
            result :: Function (LimitObject o1 m2 a)
result = Function{function :: Map (LimitObject o1 m2 a) (LimitObject o1 m2 a)
function=Set (LimitObject o1 m2 a, LimitObject o1 m2 a)
-> Map (LimitObject o1 m2 a) (LimitObject o1 m2 a)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(LimitObject o1 m2 a
mapping,Set (LimitObject o1 m2 a) -> LimitObject o1 m2 a
forall a. Set a -> a
anElement [LimitObject o1 m2 a
mapping2 | LimitObject o1 m2 a
mapping2 <- Set (LimitObject o1 m2 a)
imageTgt, LimitObject o1 m2 a -> LimitObject o1 m2 a -> Bool
forall k a. (Eq k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf ((CommaObject One o1 m2 -> CommaObject One o1 m2)
-> LimitObject o1 m2 a -> LimitObject o1 m2 a
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys CommaObject One o1 m2 -> CommaObject One o1 m2
forall {o1} {o2}. CommaObject o1 o2 m2 -> CommaObject o1 o2 m2
precompose LimitObject o1 m2 a
mapping2) LimitObject o1 m2 a
mapping]) | LimitObject o1 m2 a
mapping <- Set (LimitObject o1 m2 a)
imageSrc],
                              codomain :: Set (LimitObject o1 m2 a)
codomain=Set (LimitObject o1 m2 a)
imageTgt}
    
    -- | The right Kan extension of @X@ along @F@ where @X@ is a a set-valued functor.

    --

    -- We transform the @X@ functor so that its target becomes @(FinSet (Map (CommaObject One o1 m2) a))@, each object @A@ of @c1@ is mapped to @{Delta : {<One,id,A>} -> e | e <- X(A)}@.

    rightKanSetValued :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                          FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                          Eq a) =>
                          Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> (Diagram c2 m2 o2 (FinSet (LimitObject o1 m2 a)) (Function (LimitObject o1 m2 a)) (Set (LimitObject o1 m2 a)), NaturalTransformation c1 m1 o1 (FinSet (LimitObject o1 m2 a)) (Function (LimitObject o1 m2 a)) (Set (LimitObject o1 m2 a)))
    rightKanSetValued :: forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> (Diagram
      c2
      m2
      o2
      (FinSet (LimitObject o1 m2 a))
      (Function (LimitObject o1 m2 a))
      (Set (LimitObject o1 m2 a)),
    NaturalTransformation
      c1
      m1
      o1
      (FinSet (LimitObject o1 m2 a))
      (Function (LimitObject o1 m2 a))
      (Set (LimitObject o1 m2 a)))
rightKanSetValued Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x = (Diagram
  c2
  m2
  o2
  (FinSet (LimitObject o1 m2 a))
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
forall {a}.
Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
r,NaturalTransformation
  c1
  m1
  o1
  (FinSet (LimitObject o1 m2 a))
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
forall {a}.
NaturalTransformation
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
nat)
        where
            r :: Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
r = Diagram{src :: c2
src=Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f,tgt :: FinSet a
tgt=FinSet a
forall a. FinSet a
FinSet, omap :: Map o2 (Set (LimitObject o1 m2 a))
omap=(o2 -> Set (LimitObject o1 m2 a))
-> Set o2 -> Map o2 (Set (LimitObject o1 m2 a))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (LimitObject o1 m2 a)
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (LimitObject o1 m2 a)
rightKanSetValuedObjectwise Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x) (c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f)), mmap :: Map m2 (Function (LimitObject o1 m2 a))
mmap=(m2 -> Function (LimitObject o1 m2 a))
-> Set m2 -> Map m2 (Function (LimitObject o1 m2 a))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> m2
-> Function (LimitObject o1 m2 a)
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> m2
-> Function (LimitObject o1 m2 a)
rightKanSetValuedObjectwiseMorphism Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x) (c2 -> Set m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f))}
            rof :: Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
rof = Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
forall {a}.
Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
r  Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     c1
     m1
     o1
     (FinSet a)
     (Function (LimitObject o1 m2 a))
     (Set (LimitObject o1 m2 a))
forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- Diagram c1 m1 o1 c2 m2 o2
f
            transformAIntoMap :: o1 -> v -> Map (CommaObject One o1 m2) v
transformAIntoMap o1
k v
a = AssociationList (CommaObject One o1 m2) v
-> Map (CommaObject One o1 m2) v
forall k v. AssociationList k v -> Map k v
weakMap [(One -> o1 -> m2 -> CommaObject One o1 m2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One o1
k (c2 -> o2 -> m2
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f) (Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
k)), v
a)]
            transformSetOfAIntoSetOfMap :: o1 -> m v -> m (Map (CommaObject One o1 m2) v)
transformSetOfAIntoSetOfMap o1
k m v
v = [o1 -> v -> Map (CommaObject One o1 m2) v
forall {v}. o1 -> v -> Map (CommaObject One o1 m2) v
transformAIntoMap o1
k v
e | v
e <- m v
v]
            transformFunctionOfAIntoFunctionOfMaps :: m -> Function v -> Function (Map (CommaObject One o1 m2) v)
transformFunctionOfAIntoFunctionOfMaps m
m1 Function v
func = Function{function :: Map (Map (CommaObject One o1 m2) v) (Map (CommaObject One o1 m2) v)
function=AssociationList
  (Map (CommaObject One o1 m2) v) (Map (CommaObject One o1 m2) v)
-> Map
     (Map (CommaObject One o1 m2) v) (Map (CommaObject One o1 m2) v)
forall k v. AssociationList k v -> Map k v
weakMap [(o1 -> v -> Map (CommaObject One o1 m2) v
forall {v}. o1 -> v -> Map (CommaObject One o1 m2) v
transformAIntoMap (m -> o1
forall m o. Morphism m o => m -> o
source m
m1) v
t,o1 -> v -> Map (CommaObject One o1 m2) v
forall {v}. o1 -> v -> Map (CommaObject One o1 m2) v
transformAIntoMap (m -> o1
forall m o. Morphism m o => m -> o
target m
m1) v
u) | (v
t,v
u) <- Map v v -> AssociationList v v
forall k v. Eq k => Map k v -> AssociationList k v
Map.mapToList (Function v -> Map v v
forall a. Function a -> Map a a
function Function v
func)], codomain :: Set (Map (CommaObject One o1 m2) v)
codomain=o1 -> Set v -> Set (Map (CommaObject One o1 m2) v)
forall {m :: * -> *} {v}.
Monad m =>
o1 -> m v -> m (Map (CommaObject One o1 m2) v)
transformSetOfAIntoSetOfMap (m -> o1
forall m o. Morphism m o => m -> o
target m
m1) (Function v -> Set v
forall a. Function a -> Set a
codomain Function v
func)}
            newX :: Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
newX = Diagram{src :: c1
src=Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x, tgt :: FinSet a
tgt=FinSet a
forall a. FinSet a
FinSet, omap :: Map o1 (Set (LimitObject o1 m2 a))
omap=(o1 -> Set a -> Set (LimitObject o1 m2 a))
-> Map o1 (Set a) -> Map o1 (Set (LimitObject o1 m2 a))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey o1 -> Set a -> Set (LimitObject o1 m2 a)
forall {m :: * -> *} {v}.
Monad m =>
o1 -> m v -> m (Map (CommaObject One o1 m2) v)
transformSetOfAIntoSetOfMap (Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> Map o1 (Set a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x), mmap :: Map m1 (Function (LimitObject o1 m2 a))
mmap=(m1 -> Function a -> Function (LimitObject o1 m2 a))
-> Map m1 (Function a) -> Map m1 (Function (LimitObject o1 m2 a))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey m1 -> Function a -> Function (LimitObject o1 m2 a)
forall {v} {m}.
(Eq v, Morphism m o1) =>
m -> Function v -> Function (Map (CommaObject One o1 m2) v)
transformFunctionOfAIntoFunctionOfMaps (Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> Map m1 (Function a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x)}
            Right NaturalTransformation
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
nat = Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
-> Diagram
     c1
     m1
     o1
     (FinSet a)
     (Function (LimitObject o1 m2 a))
     (Set (LimitObject o1 m2 a))
-> Map o1 (Function (LimitObject o1 m2 a))
-> Either
     (NaturalTransformationError
        c1
        m1
        o1
        (FinSet a)
        (Function (LimitObject o1 m2 a))
        (Set (LimitObject o1 m2 a)))
     (NaturalTransformation
        c1
        m1
        o1
        (FinSet a)
        (Function (LimitObject o1 m2 a))
        (Set (LimitObject o1 m2 a)))
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> Either
     (NaturalTransformationError c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
naturalTransformation Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
rof Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
newX (Set (o1, Function (LimitObject o1 m2 a))
-> Map o1 (Function (LimitObject o1 m2 a))
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(o1
o,Function{function :: Map (LimitObject o1 m2 a) (LimitObject o1 m2 a)
function=Set (LimitObject o1 m2 a, LimitObject o1 m2 a)
-> Map (LimitObject o1 m2 a) (LimitObject o1 m2 a)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(LimitObject o1 m2 a
mapping,o1 -> a -> LimitObject o1 m2 a
forall {v}. o1 -> v -> Map (CommaObject One o1 m2) v
transformAIntoMap o1
o (((CommaObject One o1 m2, a) -> a
forall a b. (a, b) -> b
snd((CommaObject One o1 m2, a) -> a)
-> (Set (CommaObject One o1 m2, a) -> (CommaObject One o1 m2, a))
-> Set (CommaObject One o1 m2, a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set (CommaObject One o1 m2, a) -> (CommaObject One o1 m2, a)
forall a. Set a -> a
anElement) (((CommaObject One o1 m2, a) -> Bool)
-> Set (CommaObject One o1 m2, a) -> Set (CommaObject One o1 m2, a)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(CommaObject One o1 m2, a)
y -> (CommaObject One o1 m2 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget(CommaObject One o1 m2 -> o1)
-> ((CommaObject One o1 m2, a) -> CommaObject One o1 m2)
-> (CommaObject One o1 m2, a)
-> o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(CommaObject One o1 m2, a) -> CommaObject One o1 m2
forall a b. (a, b) -> a
fst) (CommaObject One o1 m2, a)
y o1 -> o1 -> Bool
forall a. Eq a => a -> a -> Bool
== o1
o) (LimitObject o1 m2 a -> Set (CommaObject One o1 m2, a)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet LimitObject o1 m2 a
mapping))) ) | LimitObject o1 m2 a
mapping <- (Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
rof Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
-> o1 -> Set (LimitObject o1 m2 a)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
o)], codomain :: Set (LimitObject o1 m2 a)
codomain=Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
newX Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (LimitObject o1 m2 a))
  (Set (LimitObject o1 m2 a))
-> o1 -> Set (LimitObject o1 m2 a)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
o }) | o1
o <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
f)])
            
            
            
            
            
            
            
            
            
            
            
            
            
            
            
    -- | A 'ColimitObject' is  a set of couples (comma objects, elements a), the couples should be seen as elements of a disjoint union, the set of couples as equivalence classes of elements of a disjoint union.

    type ColimitObject o1 m2 a = Set ((CommaObject o1 One m2), a)
    
    -- | Format a 'ColimitObject' to be readable.

    formatColimitObject :: (PrettyPrint a) => ColimitObject o1 m2 a -> String
    formatColimitObject :: forall a o1 m2. PrettyPrint a => ColimitObject o1 m2 a -> String
formatColimitObject = (Int -> a -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
maxInt)(a -> String)
-> (ColimitObject o1 m2 a -> a) -> ColimitObject o1 m2 a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(CommaObject o1 One m2, a) -> a
forall a b. (a, b) -> b
snd((CommaObject o1 One m2, a) -> a)
-> (ColimitObject o1 m2 a -> (CommaObject o1 One m2, a))
-> ColimitObject o1 m2 a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ColimitObject o1 m2 a -> (CommaObject o1 One m2, a)
forall a. Set a -> a
anElement
    
    -- | Format a set of 'ColimitObject's to be readable.

    formatSetOfColimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Set (ColimitObject o1 m2 a) -> String
    formatSetOfColimitObjects :: forall o1 m2 a.
(Eq o1, Eq m2, Eq a, PrettyPrint a) =>
Set (ColimitObject o1 m2 a) -> String
formatSetOfColimitObjects Set (ColimitObject o1 m2 a)
setOfEquivClasses = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," (ColimitObject o1 m2 a -> String
forall a o1 m2. PrettyPrint a => ColimitObject o1 m2 a -> String
formatColimitObject (ColimitObject o1 m2 a -> String)
-> [ColimitObject o1 m2 a] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (ColimitObject o1 m2 a) -> [ColimitObject o1 m2 a]
forall a. Eq a => Set a -> [a]
setToList Set (ColimitObject o1 m2 a)
setOfEquivClasses) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
    
    -- | Format a 'Function' of 'ColimitObject's to be readable.

    formatFunctionOfColimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Function (ColimitObject o1 m2 a) -> String
    formatFunctionOfColimitObjects :: forall o1 m2 a.
(Eq o1, Eq m2, Eq a, PrettyPrint a) =>
Function (ColimitObject o1 m2 a) -> String
formatFunctionOfColimitObjects Function (ColimitObject o1 m2 a)
func = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," [(ColimitObject o1 m2 a -> String
forall a o1 m2. PrettyPrint a => ColimitObject o1 m2 a -> String
formatColimitObject ColimitObject o1 m2 a
k) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (ColimitObject o1 m2 a -> String
forall a o1 m2. PrettyPrint a => ColimitObject o1 m2 a -> String
formatColimitObject ColimitObject o1 m2 a
v) | (ColimitObject o1 m2 a
k,ColimitObject o1 m2 a
v) <- (Map (ColimitObject o1 m2 a) (ColimitObject o1 m2 a)
-> AssociationList (ColimitObject o1 m2 a) (ColimitObject o1 m2 a)
forall k v. Eq k => Map k v -> AssociationList k v
Map.mapToList (Function (ColimitObject o1 m2 a)
-> Map (ColimitObject o1 m2 a) (ColimitObject o1 m2 a)
forall a. Function a -> Map a a
function Function (ColimitObject o1 m2 a)
func))]
 
    transformGraphToEquivRelation :: (Eq a) => Set (a,a) -> Set a -> Set (Set a)
    transformGraphToEquivRelation :: forall a. Eq a => Set (a, a) -> Set a -> Set (Set a)
transformGraphToEquivRelation Set (a, a)
couples Set a
initialNodes = (a -> Set (Set a) -> Set (Set a))
-> Set (Set a) -> Set a -> Set (Set a)
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\a
candidate Set (Set a)
clusters -> if (Set a -> Bool) -> Set (Set a) -> Bool
forall a. (a -> Bool) -> Set a -> Bool
Set.any (a -> Set a -> Bool
forall a. Eq a => a -> Set a -> Bool
isIn a
candidate) Set (Set a)
clusters then Set (Set a)
clusters else (Set a -> Set (Set a) -> Set (Set a)
forall a. a -> Set a -> Set a
Set.insert (a -> Set a -> Set a
forall a. a -> Set a -> Set a
Set.insert a
candidate (a -> [a] -> [a] -> Set a
dfs a
candidate [a
candidate] (Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList Set a
initialNodes))) Set (Set a)
clusters)) ([Set a] -> Set (Set a)
forall a. [a] -> Set a
set []) Set a
initialNodes
        where
            dfs :: a -> [a] -> [a] -> Set a
dfs a
node [a]
blacklist [] = [a] -> Set a
forall a. [a] -> Set a
set []
            dfs a
node [a]
blacklist (a
candidate:[a]
nodes)
                | a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
candidate [a]
blacklist = (a -> [a] -> [a] -> Set a
dfs a
node [a]
blacklist [a]
nodes)
                | (a
node,a
candidate) (a, a) -> Set (a, a) -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set (a, a)
couples Bool -> Bool -> Bool
|| (a
candidate,a
node) (a, a) -> Set (a, a) -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set (a, a)
couples = a -> Set a -> Set a
forall a. a -> Set a -> Set a
Set.insert a
candidate ((a -> [a] -> [a] -> Set a
dfs a
node [a]
blacklist [a]
nodes) Set a -> Set a -> Set a
forall a. Set a -> Set a -> Set a
||| (a -> [a] -> [a] -> Set a
dfs a
candidate (a
nodea -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
blacklist) (Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList Set a
initialNodes)))
                | Bool
otherwise = (a -> [a] -> [a] -> Set a
dfs a
node [a]
blacklist [a]
nodes)
    
    -- | Compute the image of the left Kan extension on an object of /B/. The image is a set of set of couples (comma objects, elements a) (you should see the couples as element of a disjoint union, the set of couples as equivalence classes of elements).

    leftKanSetValuedObjectwise :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                                   FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                                   Eq a) =>
                                   Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> o2 -> Set (ColimitObject o1 m2 a)
    leftKanSetValuedObjectwise :: forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (ColimitObject o1 m2 a)
leftKanSetValuedObjectwise Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x o2
b = Set (Set (CommaObject o1 One m2, a))
equivClasses
        where
            commaCat :: CommaCategory c1 m1 o1 One One One c2 m2 o2
commaCat = CommaCategory{leftDiagram :: Diagram c1 m1 o1 c2 m2 o2
leftDiagram=Diagram c1 m1 o1 c2 m2 o2
f, rightDiagram :: Diagram One One One c2 m2 o2
rightDiagram=c2 -> o2 -> Diagram One One One c2 m2 o2
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f) o2
b}
            allCouples :: Set (CommaObject o1 One m2, a)
allCouples = (([Set (CommaObject o1 One m2, a)] -> Set (CommaObject o1 One m2, a)
forall (f :: * -> *) a. Foldable f => f (Set a) -> Set a
Set.unions)([Set (CommaObject o1 One m2, a)]
 -> Set (CommaObject o1 One m2, a))
-> (Set (Set (CommaObject o1 One m2, a))
    -> [Set (CommaObject o1 One m2, a)])
-> Set (Set (CommaObject o1 One m2, a))
-> Set (CommaObject o1 One m2, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set (Set (CommaObject o1 One m2, a))
-> [Set (CommaObject o1 One m2, a)]
forall a. Eq a => Set a -> [a]
setToList (Set (Set (CommaObject o1 One m2, a))
 -> Set (CommaObject o1 One m2, a))
-> Set (Set (CommaObject o1 One m2, a))
-> Set (CommaObject o1 One m2, a)
forall a b. (a -> b) -> a -> b
$ [[(CommaObject o1 One m2
a, a
elemXa) | a
elemXa <- (Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> o1 -> Set a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ (CommaObject o1 One m2 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o1 One m2
a))] | CommaObject o1 One m2
a <- CommaCategory c1 m1 o1 One One One c2 m2 o2
-> Set (CommaObject o1 One m2)
forall c m o. FiniteCategory c m o => c -> Set o
ob CommaCategory c1 m1 o1 One One One c2 m2 o2
commaCat])
            graphRelations :: Set ((CommaObject o1 One m2, a), (CommaObject o1 One m2, a))
graphRelations =  [Set ((CommaObject o1 One m2, a), (CommaObject o1 One m2, a))]
-> Set ((CommaObject o1 One m2, a), (CommaObject o1 One m2, a))
forall (f :: * -> *) a. Foldable f => f (Set a) -> Set a
Set.unions [[((CommaMorphism o1 One m1 One m2 -> CommaObject o1 One m2
forall m o. Morphism m o => m -> o
source CommaMorphism o1 One m1 One m2
m,a
a),(CommaMorphism o1 One m1 One m2 -> CommaObject o1 One m2
forall m o. Morphism m o => m -> o
target CommaMorphism o1 One m1 One m2
m,a
b)) | (a
a,a
b) <- (Map a a -> Set (a, a)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet (Function a -> Map a a
forall a. Function a -> Map a a
function (Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> m1 -> Function a
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
->£(CommaMorphism o1 One m1 One m2 -> m1
forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow CommaMorphism o1 One m1 One m2
m))))] | CommaMorphism o1 One m1 One m2
m <- (Set (CommaMorphism o1 One m1 One m2)
-> [CommaMorphism o1 One m1 One m2]
forall a. Eq a => Set a -> [a]
setToList (CommaCategory c1 m1 o1 One One One c2 m2 o2
-> Set (CommaMorphism o1 One m1 One m2)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows CommaCategory c1 m1 o1 One One One c2 m2 o2
commaCat)), Bool -> Bool
not (CommaCategory c1 m1 o1 One One One c2 m2 o2
-> CommaMorphism o1 One m1 One m2 -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity CommaCategory c1 m1 o1 One One One c2 m2 o2
commaCat CommaMorphism o1 One m1 One m2
m)]
            equivClasses :: Set (Set (CommaObject o1 One m2, a))
equivClasses = Set ((CommaObject o1 One m2, a), (CommaObject o1 One m2, a))
-> Set (CommaObject o1 One m2, a)
-> Set (Set (CommaObject o1 One m2, a))
forall a. Eq a => Set (a, a) -> Set a -> Set (Set a)
transformGraphToEquivRelation Set ((CommaObject o1 One m2, a), (CommaObject o1 One m2, a))
graphRelations Set (CommaObject o1 One m2, a)
allCouples
            
    -- | Compute the image of the left Kan extension on a morphism of /B/. 

    leftKanSetValuedObjectwiseMorphism :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                                            FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                                            Eq a) =>
                                            Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> m2 -> Function (ColimitObject o1 m2 a)
    leftKanSetValuedObjectwiseMorphism :: forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> m2
-> Function (ColimitObject o1 m2 a)
leftKanSetValuedObjectwiseMorphism Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x m2
m = Function (ColimitObject o1 m2 a)
result
        where
            postcompose :: CommaObject o1 o2 m2 -> CommaObject o1 o2 m2
postcompose CommaObject o1 o2 m2
commaObj = o1 -> o2 -> m2 -> CommaObject o1 o2 m2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject (CommaObject o1 o2 m2 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o1 o2 m2
commaObj) (CommaObject o1 o2 m2 -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o1 o2 m2
commaObj) (m2
m m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (CommaObject o1 o2 m2 -> m2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject o1 o2 m2
commaObj))
            imageSrc :: Set (ColimitObject o1 m2 a)
imageSrc = Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (ColimitObject o1 m2 a)
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (ColimitObject o1 m2 a)
leftKanSetValuedObjectwise Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
m)
            imageTgt :: Set (ColimitObject o1 m2 a)
imageTgt = Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (ColimitObject o1 m2 a)
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (ColimitObject o1 m2 a)
leftKanSetValuedObjectwise Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m)
            result :: Function (ColimitObject o1 m2 a)
result = Function{function :: Map (ColimitObject o1 m2 a) (ColimitObject o1 m2 a)
function=Set (ColimitObject o1 m2 a, ColimitObject o1 m2 a)
-> Map (ColimitObject o1 m2 a) (ColimitObject o1 m2 a)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(ColimitObject o1 m2 a
equivClass1, Set (ColimitObject o1 m2 a) -> ColimitObject o1 m2 a
forall a. Set a -> a
anElement [ColimitObject o1 m2 a
equivClass2 | ColimitObject o1 m2 a
equivClass2 <- Set (ColimitObject o1 m2 a)
imageTgt, ((CommaObject o1 One m2, a) -> Bool)
-> ColimitObject o1 m2 a -> Bool
forall a. (a -> Bool) -> Set a -> Bool
Set.any (\(CommaObject o1 One m2
co, a
a) -> (CommaObject o1 One m2 -> CommaObject o1 One m2
forall {o1} {o2}. CommaObject o1 o2 m2 -> CommaObject o1 o2 m2
postcompose CommaObject o1 One m2
co, a
a) (CommaObject o1 One m2, a) -> ColimitObject o1 m2 a -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` ColimitObject o1 m2 a
equivClass2) ColimitObject o1 m2 a
equivClass1 ]) | ColimitObject o1 m2 a
equivClass1 <- Set (ColimitObject o1 m2 a)
imageSrc],
                              codomain :: Set (ColimitObject o1 m2 a)
codomain=Set (ColimitObject o1 m2 a)
imageTgt}
    
    -- | The left Kan extension of @X@ along @F@ where @X@ is a a set-valued functor.

    --

    -- We transform the @X@ functor so that its target becomes @(FinSet (Set ((CommaObject One o1 m2), a)))@, each object @A@ of @c1@ is mapped to @{(<One,id,A>},e) | e <- X(A)}@.

    leftKanSetValued :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                         FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                         Eq a) =>
                         Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> (Diagram c2 m2 o2 (FinSet (ColimitObject o1 m2 a)) (Function (ColimitObject o1 m2 a)) (Set (ColimitObject o1 m2 a)), NaturalTransformation c1 m1 o1 (FinSet (ColimitObject o1 m2 a)) (Function (ColimitObject o1 m2 a)) (Set (ColimitObject o1 m2 a)))
    leftKanSetValued :: forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> (Diagram
      c2
      m2
      o2
      (FinSet (ColimitObject o1 m2 a))
      (Function (ColimitObject o1 m2 a))
      (Set (ColimitObject o1 m2 a)),
    NaturalTransformation
      c1
      m1
      o1
      (FinSet (ColimitObject o1 m2 a))
      (Function (ColimitObject o1 m2 a))
      (Set (ColimitObject o1 m2 a)))
leftKanSetValued Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x = (Diagram
  c2
  m2
  o2
  (FinSet (ColimitObject o1 m2 a))
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
forall {a}.
Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
l,NaturalTransformation
  c1
  m1
  o1
  (FinSet (ColimitObject o1 m2 a))
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
forall {a}.
NaturalTransformation
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
nat)
        where
            l :: Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
l = Diagram{src :: c2
src=Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f,tgt :: FinSet a
tgt=FinSet a
forall a. FinSet a
FinSet, omap :: Map o2 (Set (ColimitObject o1 m2 a))
omap=(o2 -> Set (ColimitObject o1 m2 a))
-> Set o2 -> Map o2 (Set (ColimitObject o1 m2 a))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (ColimitObject o1 m2 a)
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> o2
-> Set (ColimitObject o1 m2 a)
leftKanSetValuedObjectwise Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x) (c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f)), mmap :: Map m2 (Function (ColimitObject o1 m2 a))
mmap=(m2 -> Function (ColimitObject o1 m2 a))
-> Set m2 -> Map m2 (Function (ColimitObject o1 m2 a))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> m2
-> Function (ColimitObject o1 m2 a)
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> m2
-> Function (ColimitObject o1 m2 a)
leftKanSetValuedObjectwiseMorphism Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x) (c2 -> Set m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f))}
            lof :: Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
lof = Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
forall {a}.
Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
l  Diagram
  c2
  m2
  o2
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     c1
     m1
     o1
     (FinSet a)
     (Function (ColimitObject o1 m2 a))
     (Set (ColimitObject o1 m2 a))
forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- Diagram c1 m1 o1 c2 m2 o2
f
            transformAIntoEquivClass :: o1 -> b -> Set (CommaObject o1 One m2, b)
transformAIntoEquivClass o1
k b
a = [(CommaObject o1 One m2, b)] -> Set (CommaObject o1 One m2, b)
forall a. [a] -> Set a
set [(o1 -> One -> m2 -> CommaObject o1 One m2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject o1
k One
One (c2 -> o2 -> m2
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
f) (Diagram c1 m1 o1 c2 m2 o2
f Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
k)), b
a)]
            transformSetOfAIntoSetOfEquivClasses :: o1 -> m b -> m (Set (CommaObject o1 One m2, b))
transformSetOfAIntoSetOfEquivClasses o1
k m b
v = [o1 -> b -> Set (CommaObject o1 One m2, b)
forall {b}. o1 -> b -> Set (CommaObject o1 One m2, b)
transformAIntoEquivClass o1
k b
e | b
e <- m b
v]
            transformFunctionOfAIntoFunctionOfSetsOfEquivClasses :: m -> Function b -> Function (Set (CommaObject o1 One m2, b))
transformFunctionOfAIntoFunctionOfSetsOfEquivClasses m
m1 Function b
func = Function{function :: Map
  (Set (CommaObject o1 One m2, b)) (Set (CommaObject o1 One m2, b))
function=AssociationList
  (Set (CommaObject o1 One m2, b)) (Set (CommaObject o1 One m2, b))
-> Map
     (Set (CommaObject o1 One m2, b)) (Set (CommaObject o1 One m2, b))
forall k v. AssociationList k v -> Map k v
weakMap [(o1 -> b -> Set (CommaObject o1 One m2, b)
forall {b}. o1 -> b -> Set (CommaObject o1 One m2, b)
transformAIntoEquivClass (m -> o1
forall m o. Morphism m o => m -> o
source m
m1) b
t,o1 -> b -> Set (CommaObject o1 One m2, b)
forall {b}. o1 -> b -> Set (CommaObject o1 One m2, b)
transformAIntoEquivClass (m -> o1
forall m o. Morphism m o => m -> o
target m
m1) b
u) | (b
t,b
u) <- Map b b -> AssociationList b b
forall k v. Eq k => Map k v -> AssociationList k v
Map.mapToList (Function b -> Map b b
forall a. Function a -> Map a a
function Function b
func)], codomain :: Set (Set (CommaObject o1 One m2, b))
codomain=o1 -> Set b -> Set (Set (CommaObject o1 One m2, b))
forall {m :: * -> *} {b}.
Monad m =>
o1 -> m b -> m (Set (CommaObject o1 One m2, b))
transformSetOfAIntoSetOfEquivClasses (m -> o1
forall m o. Morphism m o => m -> o
target m
m1) (Function b -> Set b
forall a. Function a -> Set a
codomain Function b
func)}
            newX :: Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
newX = Diagram{src :: c1
src=Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x, tgt :: FinSet a
tgt=FinSet a
forall a. FinSet a
FinSet, omap :: Map o1 (Set (ColimitObject o1 m2 a))
omap=(o1 -> Set a -> Set (ColimitObject o1 m2 a))
-> Map o1 (Set a) -> Map o1 (Set (ColimitObject o1 m2 a))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey o1 -> Set a -> Set (ColimitObject o1 m2 a)
forall {m :: * -> *} {b}.
Monad m =>
o1 -> m b -> m (Set (CommaObject o1 One m2, b))
transformSetOfAIntoSetOfEquivClasses (Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> Map o1 (Set a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x), mmap :: Map m1 (Function (ColimitObject o1 m2 a))
mmap=(m1 -> Function a -> Function (ColimitObject o1 m2 a))
-> Map m1 (Function a) -> Map m1 (Function (ColimitObject o1 m2 a))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey m1 -> Function a -> Function (ColimitObject o1 m2 a)
forall {b} {m}.
(Eq b, Morphism m o1) =>
m -> Function b -> Function (Set (CommaObject o1 One m2, b))
transformFunctionOfAIntoFunctionOfSetsOfEquivClasses (Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> Map m1 (Function a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
x)}
            Right NaturalTransformation
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
nat = Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
-> Diagram
     c1
     m1
     o1
     (FinSet a)
     (Function (ColimitObject o1 m2 a))
     (Set (ColimitObject o1 m2 a))
-> Map o1 (Function (ColimitObject o1 m2 a))
-> Either
     (NaturalTransformationError
        c1
        m1
        o1
        (FinSet a)
        (Function (ColimitObject o1 m2 a))
        (Set (ColimitObject o1 m2 a)))
     (NaturalTransformation
        c1
        m1
        o1
        (FinSet a)
        (Function (ColimitObject o1 m2 a))
        (Set (ColimitObject o1 m2 a)))
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> Either
     (NaturalTransformationError c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
naturalTransformation Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
newX Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
lof (Set (o1, Function (ColimitObject o1 m2 a))
-> Map o1 (Function (ColimitObject o1 m2 a))
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(o1
o,Function{function :: Map (ColimitObject o1 m2 a) (ColimitObject o1 m2 a)
function=Set (ColimitObject o1 m2 a, ColimitObject o1 m2 a)
-> Map (ColimitObject o1 m2 a) (ColimitObject o1 m2 a)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(ColimitObject o1 m2 a
equivClass,Set (ColimitObject o1 m2 a) -> ColimitObject o1 m2 a
forall a. Set a -> a
anElement [ColimitObject o1 m2 a
equivClass2 | ColimitObject o1 m2 a
equivClass2 <- (Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
lof Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
-> o1 -> Set (ColimitObject o1 m2 a)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
o), ((CommaObject o1 One m2, a) -> Bool)
-> ColimitObject o1 m2 a -> Bool
forall a. (a -> Bool) -> Set a -> Bool
Set.any (\(CommaObject o1 One m2
co,a
a2) -> CommaObject o1 One m2 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o1 One m2
co o1 -> o1 -> Bool
forall a. Eq a => a -> a -> Bool
== o1
o Bool -> Bool -> Bool
&& ((CommaObject o1 One m2, a) -> a
forall a b. (a, b) -> b
snd((CommaObject o1 One m2, a) -> a)
-> (ColimitObject o1 m2 a -> (CommaObject o1 One m2, a))
-> ColimitObject o1 m2 a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ColimitObject o1 m2 a -> (CommaObject o1 One m2, a)
forall a. Set a -> a
anElement (ColimitObject o1 m2 a -> a) -> ColimitObject o1 m2 a -> a
forall a b. (a -> b) -> a -> b
$ ColimitObject o1 m2 a
equivClass) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a2) ColimitObject o1 m2 a
equivClass2]) | ColimitObject o1 m2 a
equivClass <- (Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
newX Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
-> o1 -> Set (ColimitObject o1 m2 a)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
o)], codomain :: Set (ColimitObject o1 m2 a)
codomain=Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
forall {a}.
Diagram
  c1
  m1
  o1
  (FinSet a)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
lof Diagram
  c1
  m1
  o1
  (FinSet Any)
  (Function (ColimitObject o1 m2 a))
  (Set (ColimitObject o1 m2 a))
-> o1 -> Set (ColimitObject o1 m2 a)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
o }) | o1
o <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
f)])