{-# LANGUAGE MonadComprehensions #-}
module Math.Categories.ConeCategory
(
Cone(..),
cone,
unsafeCone,
apex,
baseCone,
legsCone,
universeCategoryCone,
indexingCategoryCone,
topInjectionsCone,
ConeMorphism,
bindingMorphismCone,
ConeCategory,
coneCategory,
limits,
Cocone(..),
cocone,
unsafeCocone,
nadir,
baseCocone,
legsCocone,
universeCategoryCocone,
indexingCategoryCocone,
bottomInjectionsCocone,
CoconeMorphism,
bindingMorphismCocone,
CoconeCategory,
coconeCategory,
colimits,
)
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.Simplifiable
import Math.Category
import Math.FiniteCategory
import Math.Categories.CommaCategory
import Math.Categories.FunctorCategory
import Math.Functors.DiagonalFunctor
import Math.FiniteCategories.One
type Cone c1 m1 o1 c2 m2 o2 = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
cone :: (Morphism m1 o1, FiniteCategory c1 m1 o1,
Morphism m2 o2, FiniteCategory c2 m2 o2,
Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2) =>
o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
cone :: forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Morphism m2 o2,
FiniteCategory c2 m2 o2, Eq c1, Eq m1, Eq o1, Eq c2, Eq m2,
Eq o2) =>
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (Cone c1 m1 o1 c2 m2 o2)
cone o2
apex NaturalTransformation c1 m1 o1 c2 m2 o2
nat
| c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
indexingCat c2
universeCat o2
apex Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c2 m2 o2
nat = Maybe (Cone c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
| Bool
otherwise = Cone c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just Cone c1 m1 o1 c2 m2 o2
result
where
indexingCat :: c1
indexingCat = 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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nat
universeCat :: c2
universeCat = 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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nat
result :: Cone c1 m1 o1 c2 m2 o2
result = o2
-> One
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject o2
apex One
One NaturalTransformation c1 m1 o1 c2 m2 o2
nat
unsafeCone :: o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
unsafeCone :: forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone o2
apex NaturalTransformation c1 m1 o1 c2 m2 o2
nat = o2
-> One
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject o2
apex One
One NaturalTransformation c1 m1 o1 c2 m2 o2
nat
apex :: Cone c1 m1 o1 c2 m2 o2 -> o2
apex :: forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2) -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource
baseCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Morphism m2 o2) =>
Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCone :: forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Morphism m2 o2) =>
Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCone = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target(NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> (Cone c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow
legsCone :: Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone :: forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow
type ConeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism o2 One m2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
bindingMorphismCone :: ConeMorphism c1 m1 o1 c2 m2 o2 -> m2
bindingMorphismCone :: forall c1 m1 o1 c2 m2 o2. ConeMorphism c1 m1 o1 c2 m2 o2 -> m2
bindingMorphismCone = CommaMorphism
o2 One m2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> m2
forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow
type ConeCategory c1 m1 o1 c2 m2 o2 = CommaCategory c2 m2 o2 One One One (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
coneCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
coneCategory :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
coneCategory diag :: Diagram c1 m1 o1 c2 m2 o2
diag@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m1 m2
fm} = CommaCategory {leftDiagram :: Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
leftDiagram = Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct
, rightDiagram :: Diagram
One
One
One
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
rightDiagram = FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
One
One
One
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 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
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
-> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct) Diagram c1 m1 o1 c2 m2 o2
diag}
where
diagonalFunct :: Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct = c1
-> c2
-> Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
Morphism m2 o2) =>
c1
-> c2
-> Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunctor c1
s c2
t
limits :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
limits :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
limits = ConeCategory c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
terminalObjects(ConeCategory c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2))
-> (Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> Set (Cone c1 m1 o1 c2 m2 o2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
coneCategory
loopClasses :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
loopClasses :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
loopClasses c
c = [[o
y | o
y <- c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
x o
y, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
y o
x] | o
x <- c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c]
topObjects :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
topObjects :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
topObjects c
c = [Set o
loopClass | Set o
loopClass <- c -> Set (Set o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
loopClasses c
c, Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\m
f -> (Bool -> Bool
not (m -> o
forall m o. Morphism m o => m -> o
source m
f o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
loopClass)) Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
target m
f o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
loopClass)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c]
possibleDomainsTopContained :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsTopContained :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsTopContained c
c = [[o]] -> Set [o]
forall a. [a] -> Set a
set([[o]] -> Set [o]) -> (Set [o] -> [[o]]) -> Set [o] -> Set [o]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set [o] -> [[o]]
forall a. Eq a => Set a -> [a]
setToList (Set [o] -> Set [o]) -> Set [o] -> Set [o]
forall a b. (a -> b) -> a -> b
$ [Set o] -> Set [o]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets ([Set o] -> Set [o]) -> [Set o] -> Set [o]
forall a b. (a -> b) -> a -> b
$ Set (Set o) -> [Set o]
forall a. Eq a => Set a -> [a]
setToList (Set (Set o) -> [Set o]) -> Set (Set o) -> [Set o]
forall a b. (a -> b) -> a -> b
$ c -> Set (Set o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
topObjects c
c
enumerateInjectiveMaps :: (Eq a, Eq b) => (a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps :: forall a b.
(Eq a, Eq b) =>
(a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps a -> b -> Bool
cond Set a
dom Set b
codom
| Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
dom = [Map a b] -> Set (Map a b)
forall a. [a] -> Set a
set [AssociationList a b -> Map a b
forall k v. AssociationList k v -> Map k v
weakMap []]
| Set b -> Bool
forall a. Set a -> Bool
Set.null Set b
codom = [Map a b] -> Set (Map a b)
forall a. [a] -> Set a
set []
| Set b -> Bool
forall a. Set a -> Bool
Set.null Set b
compatibleYs = [Map a b] -> Set (Map a b)
forall a. [a] -> Set a
set []
| Bool
otherwise = a -> b -> Map a b -> Map a b
forall k a. k -> a -> Map k a -> Map k a
Map.insert a
x b
y (Map a b -> Map a b) -> Set (Map a b) -> Set (Map a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
forall a b.
(Eq a, Eq b) =>
(a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps a -> b -> Bool
cond Set a
xs Set b
ys
where
x :: a
x = Set a -> a
forall a. Set a -> a
anElement Set a
dom
xs :: Set a
xs = a -> Set a -> Set a
forall a. Eq a => a -> Set a -> Set a
Set.delete a
x Set a
dom
compatibleYs :: Set b
compatibleYs = [b
a | b
a <- Set b
codom, a -> b -> Bool
cond a
x b
a]
y :: b
y = Set b -> b
forall a. Set a -> a
anElement Set b
compatibleYs
ys :: Set b
ys = b -> Set b -> Set b
forall a. Eq a => a -> Set a -> Set a
Set.delete b
y Set b
codom
topInjectionsCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Cone c1 m1 o1 c3 m3 o3 -> Cone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2)
topInjectionsCone :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Cone c1 m1 o1 c3 m3 o3 -> Cone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2)
topInjectionsCone Cone c1 m1 o1 c3 m3 o3
c1 Cone c2 m2 o2 c3 m3 o3
c2
| Cone c1 m1 o1 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone c1 m1 o1 c3 m3 o3
c1 o3 -> o3 -> Bool
forall a. Eq a => a -> a -> Bool
== Cone c2 m2 o2 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone c2 m2 o2 c3 m3 o3
c2 = Set (Map o1 o2)
maps
| Bool
otherwise = [Map o1 o2] -> Set (Map o1 o2)
forall a. [a] -> Set a
set []
where
doms :: Set [o1]
doms = c1 -> Set [o1]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsTopContained (c1 -> Set [o1]) -> c1 -> Set [o1]
forall a b. (a -> b) -> a -> b
$ Cone c1 m1 o1 c3 m3 o3 -> c1
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) =>
Cone c1 m1 o1 c2 m2 o2 -> c1
indexingCategoryCone Cone c1 m1 o1 c3 m3 o3
c1
maps :: Set (Map o1 o2)
maps = Set (Set (Map o1 o2)) -> Set (Map o1 o2)
forall a. Set (Set a) -> Set a
Set.concat2 [(o1 -> o2 -> Bool) -> Set o1 -> Set o2 -> Set (Map o1 o2)
forall a b.
(Eq a, Eq b) =>
(a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps (\o1
x o2
y -> Cone c1 m1 o1 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone c1 m1 o1 c3 m3 o3
c1 NaturalTransformation c1 m1 o1 c3 m3 o3 -> o1 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o1
x m3 -> m3 -> Bool
forall a. Eq a => a -> a -> Bool
== Cone c2 m2 o2 c3 m3 o3 -> NaturalTransformation c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone c2 m2 o2 c3 m3 o3
c2 NaturalTransformation c2 m2 o2 c3 m3 o3 -> o2 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o2
y) ([o1] -> Set o1
forall a. [a] -> Set a
set [o1]
dom) (c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob (Cone c2 m2 o2 c3 m3 o3 -> c2
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) =>
Cone c1 m1 o1 c2 m2 o2 -> c1
indexingCategoryCone Cone c2 m2 o2 c3 m3 o3
c2)) | [o1]
dom <- Set [o1]
doms]
type Cocone c1 m1 o1 c2 m2 o2 = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
cocone :: (Morphism m1 o1, FiniteCategory c1 m1 o1,
Morphism m2 o2, FiniteCategory c2 m2 o2,
Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2) =>
o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
cocone :: forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Morphism m2 o2,
FiniteCategory c2 m2 o2, Eq c1, Eq m1, Eq o1, Eq c2, Eq m2,
Eq o2) =>
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (Cocone c1 m1 o1 c2 m2 o2)
cocone o2
nadir NaturalTransformation c1 m1 o1 c2 m2 o2
nat
| c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
indexingCat c2
universeCat o2
nadir Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nat = Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
| Bool
otherwise = Cocone c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just Cocone c1 m1 o1 c2 m2 o2
result
where
indexingCat :: c1
indexingCat = 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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nat
universeCat :: c2
universeCat = 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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nat
result :: Cocone c1 m1 o1 c2 m2 o2
result = One
-> o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One o2
nadir NaturalTransformation c1 m1 o1 c2 m2 o2
nat
unsafeCocone :: o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone :: forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone o2
nadir NaturalTransformation c1 m1 o1 c2 m2 o2
nat = One
-> o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One o2
nadir NaturalTransformation c1 m1 o1 c2 m2 o2
nat
nadir :: Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir :: forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2) -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget
baseCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Morphism m2 o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCocone :: forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Morphism m2 o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCocone = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source(NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> (Cocone c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow
legsCocone :: Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone :: forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow
naturalTransformationToCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1
,FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
naturalTransformationToCocone :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (Cocone c1 m1 o1 c2 m2 o2)
naturalTransformationToCocone NaturalTransformation c1 m1 o1 c2 m2 o2
nt
| Set o1 -> Bool
forall a. Set a -> Bool
Set.null (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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)) = Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
| NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= Diagram c1 m1 o1 c2 m2 o2
constDiag = Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
| Bool
otherwise = Cocone c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just (Cocone c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2))
-> Cocone c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> a -> b
$ One
-> o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One o2
nadirCandidate NaturalTransformation c1 m1 o1 c2 m2 o2
nt
where
nadirCandidate :: o2
nadirCandidate = (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt) 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
->$ (Set o1 -> o1
forall a. Set a -> a
anElement(Set o1 -> o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob(c1 -> Set o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Set o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)
constDiag :: Diagram c1 m1 o1 c2 m2 o2
constDiag = c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram (Diagram 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 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) (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 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) o2
nadirCandidate
type CoconeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism One o2 One m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
bindingMorphismCocone :: CoconeMorphism c1 m1 o1 c2 m2 o2 -> m2
bindingMorphismCocone :: forall c1 m1 o1 c2 m2 o2. CoconeMorphism c1 m1 o1 c2 m2 o2 -> m2
bindingMorphismCocone = CommaMorphism
One o2 One m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> m2
forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow
type CoconeCategory c1 m1 o1 c2 m2 o2 = CommaCategory One One One c2 m2 o2 (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
coconeCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
coconeCategory :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
coconeCategory diag :: Diagram c1 m1 o1 c2 m2 o2
diag@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m1 m2
fm} = CommaCategory {leftDiagram :: Diagram
One
One
One
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
leftDiagram = FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
One
One
One
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 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
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
-> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct) Diagram c1 m1 o1 c2 m2 o2
diag
, rightDiagram :: Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
rightDiagram = Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct}
where
diagonalFunct :: Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct = c1
-> c2
-> Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
Morphism m2 o2) =>
c1
-> c2
-> Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunctor c1
s c2
t
colimits :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)
colimits :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)
colimits = CoconeCategory c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
initialObjects(CoconeCategory c1 m1 o1 c2 m2 o2
-> Set (Cocone c1 m1 o1 c2 m2 o2))
-> (Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> Set (Cocone c1 m1 o1 c2 m2 o2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
coconeCategory
universeCategoryCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Cone c1 m1 o1 c2 m2 o2 -> c2
universeCategoryCone :: 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) =>
Cone c1 m1 o1 c2 m2 o2 -> c2
universeCategoryCone = 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 -> c2)
-> (Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source(NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> (Cone c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone
universeCategoryCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> c2
universeCategoryCocone :: 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) =>
Cocone c1 m1 o1 c2 m2 o2 -> c2
universeCategoryCocone = 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 -> c2)
-> (Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source(NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> (Cocone c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone
indexingCategoryCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Cone c1 m1 o1 c2 m2 o2 -> c1
indexingCategoryCone :: 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) =>
Cone c1 m1 o1 c2 m2 o2 -> c1
indexingCategoryCone = 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 -> c1)
-> (Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source(NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> (Cone c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone
indexingCategoryCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Cocone c1 m1 o1 c2 m2 o2 -> c1
indexingCategoryCocone :: 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) =>
Cocone c1 m1 o1 c2 m2 o2 -> c1
indexingCategoryCocone = 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 -> c1)
-> (Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source(NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2)
-> (Cocone c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone
bottomObjects :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
bottomObjects :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
bottomObjects c
c = [Set o
loopClass | Set o
loopClass <- c -> Set (Set o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
loopClasses c
c, Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\m
f -> (Bool -> Bool
not (m -> o
forall m o. Morphism m o => m -> o
target m
f o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
loopClass)) Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
source m
f o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
loopClass)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c]
possibleDomainsBottomContained :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsBottomContained :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsBottomContained c
c = [[o]] -> Set [o]
forall a. [a] -> Set a
set([[o]] -> Set [o]) -> (Set [o] -> [[o]]) -> Set [o] -> Set [o]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set [o] -> [[o]]
forall a. Eq a => Set a -> [a]
setToList (Set [o] -> Set [o]) -> Set [o] -> Set [o]
forall a b. (a -> b) -> a -> b
$ [Set o] -> Set [o]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets ([Set o] -> Set [o]) -> [Set o] -> Set [o]
forall a b. (a -> b) -> a -> b
$ Set (Set o) -> [Set o]
forall a. Eq a => Set a -> [a]
setToList (Set (Set o) -> [Set o]) -> Set (Set o) -> [Set o]
forall a b. (a -> b) -> a -> b
$ c -> Set (Set o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
bottomObjects c
c
bottomInjectionsCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Cocone c1 m1 o1 c3 m3 o3 -> Cocone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2)
bottomInjectionsCocone :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Cocone c1 m1 o1 c3 m3 o3
-> Cocone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2)
bottomInjectionsCocone Cocone c1 m1 o1 c3 m3 o3
cc1 Cocone c2 m2 o2 c3 m3 o3
cc2
| Cocone c1 m1 o1 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone c1 m1 o1 c3 m3 o3
cc1 o3 -> o3 -> Bool
forall a. Eq a => a -> a -> Bool
== Cocone c2 m2 o2 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone c2 m2 o2 c3 m3 o3
cc2 = Set (Map o1 o2)
maps
| Bool
otherwise = [Map o1 o2] -> Set (Map o1 o2)
forall a. [a] -> Set a
set []
where
doms :: Set [o1]
doms = c1 -> Set [o1]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsBottomContained (c1 -> Set [o1]) -> c1 -> Set [o1]
forall a b. (a -> b) -> a -> b
$ Cocone c1 m1 o1 c3 m3 o3 -> c1
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) =>
Cocone c1 m1 o1 c2 m2 o2 -> c1
indexingCategoryCocone Cocone c1 m1 o1 c3 m3 o3
cc1
maps :: Set (Map o1 o2)
maps = Set (Set (Map o1 o2)) -> Set (Map o1 o2)
forall a. Set (Set a) -> Set a
Set.concat2 [(o1 -> o2 -> Bool) -> Set o1 -> Set o2 -> Set (Map o1 o2)
forall a b.
(Eq a, Eq b) =>
(a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps (\o1
x o2
y -> Cocone c1 m1 o1 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone c1 m1 o1 c3 m3 o3
cc1 NaturalTransformation c1 m1 o1 c3 m3 o3 -> o1 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o1
x m3 -> m3 -> Bool
forall a. Eq a => a -> a -> Bool
== Cocone c2 m2 o2 c3 m3 o3 -> NaturalTransformation c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone c2 m2 o2 c3 m3 o3
cc2 NaturalTransformation c2 m2 o2 c3 m3 o3 -> o2 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o2
y) ([o1] -> Set o1
forall a. [a] -> Set a
set [o1]
dom) (c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob (Cocone c2 m2 o2 c3 m3 o3 -> c2
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) =>
Cocone c1 m1 o1 c2 m2 o2 -> c1
indexingCategoryCocone Cocone c2 m2 o2 c3 m3 o3
cc2)) | [o1]
dom <- Set [o1]
doms]