module Math.Categories.ConeCategory
(
Cone,
apex,
baseCone,
legsCone,
naturalTransformationToCone,
ConeMorphism,
bindingMorphismCone,
ConeCategory,
coneCategory,
limits,
Cocone,
nadir,
baseCocone,
legsCocone,
naturalTransformationToCocone,
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 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)
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, Eq c2, Eq m2, Eq 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, Eq c2, Eq m2, Eq 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
naturalTransformationToCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1
,Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
naturalTransformationToCone :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (Cone c1 m1 o1 c2 m2 o2)
naturalTransformationToCone 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 (Cone 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
source 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 (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 -> Maybe (Cone c1 m1 o1 c2 m2 o2))
-> Cone c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> a -> b
$ 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
apexCandidate One
One NaturalTransformation c1 m1 o1 c2 m2 o2
nt
where
apexCandidate :: o2
apexCandidate = (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
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
apexCandidate
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
type Cocone c1 m1 o1 c2 m2 o2 = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
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, Eq c2, Eq m2, Eq 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, Eq c2, Eq m2, Eq 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