{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MonadComprehensions #-}
module Math.Functors.SetValued
(
LimitObject(..),
rightKanSetValued,
formatLimitObject,
formatSetOfLimitObjects,
formatFunctionOfLimitObjects,
ColimitObject(..),
leftKanSetValued,
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)
type LimitObject o1 m2 a = Map (CommaObject One o1 m2) a
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
")"
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
"}"
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))]
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
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}
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)])
type ColimitObject o1 m2 a = Set ((CommaObject o1 One m2), a)
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
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
"}"
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)
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
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}
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)])