{-# LANGUAGE MultiParamTypeClasses #-}
module ConeCategory.ConeCategory
(
Cone,
ConeMorphism,
ConeCategory,
apex,
coneToNaturalTransformation,
naturalTransformationToCone,
mkConeCategory,
conesOfApex,
terminalObjects,
limits,
Cocone,
CoconeMorphism,
CoconeCategory,
nadir,
coconeToNaturalTransformation,
naturalTransformationToCocone,
mkCoconeCategory,
coconesOfNadir,
initialObjects,
colimits
)
where
import FiniteCategory.FiniteCategory
import Diagram.Diagram
import DiagonalFunctor.DiagonalFunctor
import CommaCategory.CommaCategory
import FunctorCategory.FunctorCategory
import UsualCategories.One
import Data.Maybe (fromJust)
import Utils.AssociationList
type Cone c1 m1 o1 c2 m2 o2 = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
type ConeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism o2 One m2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
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)
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
indexSrc
coneToNaturalTransformation :: Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
coneToNaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
coneToNaturalTransformation = 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
arrow
naturalTransformationToCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
,FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
naturalTransformationToCone :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
naturalTransformationToCone nt :: NaturalTransformation c1 m1 o1 c2 m2 o2
nt@NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
compo}
| [o1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [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
s)) = [Char] -> Cone c1 m1 o1 c2 m2 o2
forall a. HasCallStack => [Char] -> a
error [Char]
"Cone of a diagram with empty index category"
| Bool
otherwise = CommaObject :: forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
CommaObject{indexSrc :: o2
indexSrc=(Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
s) AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-! ([o1] -> o1
forall a. [a] -> a
head (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [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
s))),indexTgt :: One
indexTgt=One
One,arrow :: NaturalTransformation c1 m1 o1 c2 m2 o2
arrow=NaturalTransformation c1 m1 o1 c2 m2 o2
nt}
mkConeCategory :: (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
mkConeCategory :: 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
mkConeCategory 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 -> AssociationList o1 o2
omap=AssociationList o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap=AssociationList m1 m2
fm} = CommaCategory :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
CommaCategory {leftDiag :: 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)
leftDiag = 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
, rightDiag :: 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)
rightDiag = Maybe
(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))
-> 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 a. HasCallStack => Maybe a -> a
fromJust (Maybe
(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))
-> 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))
-> Maybe
(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))
-> 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 a b. (a -> b) -> a -> b
$ FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Maybe
(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.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 (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, Eq 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)
mkDiagonalFunctor c1
s c2
t
conesOfApex :: (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 -> o2 -> [Cone c1 m1 o1 c2 m2 o2]
conesOfApex :: 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 -> o2 -> [Cone c1 m1 o1 c2 m2 o2]
conesOfApex Diagram c1 m1 o1 c2 m2 o2
diag o2
apx
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ o2 -> [o2] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o2
apx (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [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
diag)) = [Char] -> [Cone c1 m1 o1 c2 m2 o2]
forall a. HasCallStack => [Char] -> a
error [Char]
"Trying to construct cones from an apex not in the target category."
| Bool
otherwise = NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
naturalTransformationToCone (NaturalTransformation 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]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar FunctorCategory c1 m1 o1 c2 m2 o2
forall {m1} {o1} {m2} {o2}. FunctorCategory c1 m1 o1 c2 m2 o2
functCat Diagram c1 m1 o1 c2 m2 o2
constDiag Diagram c1 m1 o1 c2 m2 o2
diag
where
functCat :: FunctorCategory c1 m1 o1 c2 m2 o2
functCat = c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (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
diag) (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
diag)
Just Diagram c1 m1 o1 c2 m2 o2
constDiag = c1 -> c2 -> o2 -> Maybe (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, Eq o2) =>
c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
mkConstantDiagram (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
diag) (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
diag) o2
apx
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 -> [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 -> [Cone c1 m1 o1 c2 m2 o2]
limits = ConeCategory c1 m1 o1 c2 m2 o2 -> [Cone c1 m1 o1 c2 m2 o2]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [o]
terminalObjects(ConeCategory c1 m1 o1 c2 m2 o2 -> [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
-> [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
mkConeCategory
type Cocone c1 m1 o1 c2 m2 o2 = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
type CoconeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism One o2 One m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
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)
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
indexTgt
coconeToNaturalTransformation :: Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
coconeToNaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
coconeToNaturalTransformation = 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
arrow
naturalTransformationToCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
,FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
naturalTransformationToCocone :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
naturalTransformationToCocone nt :: NaturalTransformation c1 m1 o1 c2 m2 o2
nt@NaturalTransformation{srcNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
srcNT=Diagram c1 m1 o1 c2 m2 o2
s,tgtNT :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
tgtNT=Diagram c1 m1 o1 c2 m2 o2
t,component :: forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
component=o1 -> m2
compo}
| [o1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [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
t)) = [Char] -> Cocone c1 m1 o1 c2 m2 o2
forall a. HasCallStack => [Char] -> a
error [Char]
"Diagram with empty index category"
| Bool
otherwise = CommaObject :: forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
CommaObject{indexSrc :: One
indexSrc=One
One,indexTgt :: o2
indexTgt=(Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
t) AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-! ([o1] -> o1
forall a. [a] -> a
head (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [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
t))),arrow :: NaturalTransformation c1 m1 o1 c2 m2 o2
arrow=NaturalTransformation c1 m1 o1 c2 m2 o2
nt}
mkCoconeCategory :: (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
mkCoconeCategory :: 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
mkCoconeCategory 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 -> AssociationList o1 o2
omap=AssociationList o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap=AssociationList m1 m2
fm} = CommaCategory :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
CommaCategory {leftDiag :: 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)
leftDiag = Maybe
(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))
-> 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 a. HasCallStack => Maybe a -> a
fromJust (Maybe
(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))
-> 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))
-> Maybe
(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))
-> 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 a b. (a -> b) -> a -> b
$ FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Maybe
(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.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 (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
, rightDiag :: 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)
rightDiag = 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, Eq 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)
mkDiagonalFunctor c1
s c2
t
coconesOfNadir :: ( 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 -> o2 -> [Cocone c1 m1 o1 c2 m2 o2]
coconesOfNadir :: 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 -> o2 -> [Cocone c1 m1 o1 c2 m2 o2]
coconesOfNadir Diagram c1 m1 o1 c2 m2 o2
diag o2
nadr
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ o2 -> [o2] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o2
nadr (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [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
diag)) = [Char] -> [Cocone c1 m1 o1 c2 m2 o2]
forall a. HasCallStack => [Char] -> a
error [Char]
"Trying to construct cocones to a nadir not in the target category."
| Bool
otherwise = NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
naturalTransformationToCocone (NaturalTransformation 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]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> [NaturalTransformation c1 m1 o1 c2 m2 o2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar FunctorCategory c1 m1 o1 c2 m2 o2
forall {m1} {o1} {m2} {o2}. FunctorCategory c1 m1 o1 c2 m2 o2
functCat Diagram c1 m1 o1 c2 m2 o2
diag Diagram c1 m1 o1 c2 m2 o2
constDiag
where
functCat :: FunctorCategory c1 m1 o1 c2 m2 o2
functCat = c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (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
diag) (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
diag)
Just Diagram c1 m1 o1 c2 m2 o2
constDiag = c1 -> c2 -> o2 -> Maybe (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, Eq o2) =>
c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
mkConstantDiagram (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
diag) (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
diag) o2
nadr
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 -> [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 -> [Cocone c1 m1 o1 c2 m2 o2]
colimits = CoconeCategory c1 m1 o1 c2 m2 o2 -> [Cocone c1 m1 o1 c2 m2 o2]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [o]
initialObjects(CoconeCategory c1 m1 o1 c2 m2 o2 -> [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
-> [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
mkCoconeCategory