{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : A comma category is a category where objects are morphisms of another category /C/ and morphisms are commutative squares in /C/.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A comma category is a category where objects are morphisms of another category /C/ and morphisms are commutative squares in /C/.

For example, see Examples.ExampleCommaCategory.*
-}

module CommaCategory.CommaCategory
(
    CommaObject(..),
    CommaMorphism(..),
    CommaCategory(..),
    mkSliceCategory,
    mkCosliceCategory,
    mkArrowCategory,
)
where
    import FiniteCategory.FiniteCategory
    import Diagram.Diagram
    import UsualCategories.One
    import IO.PrettyPrint
    import Utils.AssociationList
    
    -- | A `CommaObject` in the `CommaCategory` (/T/|/S/) is a triplet \</e/,/d/,/f/\> where @f : /T/(e) -> /S/(d)@.

    --

    -- See /Categories for the working mathematician/, Saunders Mac Lane, P.46.

    data CommaObject o1 o2 m3 = CommaObject {forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc :: o1 -- ^ /e/

                                        , forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTgt :: o2 -- ^ /d/

                                        , forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow :: m3} -- ^ /f/

                                        deriving (CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool
(CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool)
-> (CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool)
-> Eq (CommaObject o1 o2 m3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall o1 o2 m3.
(Eq o1, Eq o2, Eq m3) =>
CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool
/= :: CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool
$c/= :: forall o1 o2 m3.
(Eq o1, Eq o2, Eq m3) =>
CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool
== :: CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool
$c== :: forall o1 o2 m3.
(Eq o1, Eq o2, Eq m3) =>
CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool
Eq, Int -> CommaObject o1 o2 m3 -> ShowS
[CommaObject o1 o2 m3] -> ShowS
CommaObject o1 o2 m3 -> String
(Int -> CommaObject o1 o2 m3 -> ShowS)
-> (CommaObject o1 o2 m3 -> String)
-> ([CommaObject o1 o2 m3] -> ShowS)
-> Show (CommaObject o1 o2 m3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall o1 o2 m3.
(Show o1, Show o2, Show m3) =>
Int -> CommaObject o1 o2 m3 -> ShowS
forall o1 o2 m3.
(Show o1, Show o2, Show m3) =>
[CommaObject o1 o2 m3] -> ShowS
forall o1 o2 m3.
(Show o1, Show o2, Show m3) =>
CommaObject o1 o2 m3 -> String
showList :: [CommaObject o1 o2 m3] -> ShowS
$cshowList :: forall o1 o2 m3.
(Show o1, Show o2, Show m3) =>
[CommaObject o1 o2 m3] -> ShowS
show :: CommaObject o1 o2 m3 -> String
$cshow :: forall o1 o2 m3.
(Show o1, Show o2, Show m3) =>
CommaObject o1 o2 m3 -> String
showsPrec :: Int -> CommaObject o1 o2 m3 -> ShowS
$cshowsPrec :: forall o1 o2 m3.
(Show o1, Show o2, Show m3) =>
Int -> CommaObject o1 o2 m3 -> ShowS
Show)
    
    instance (PrettyPrintable o1, PrettyPrintable o2, PrettyPrintable m3) =>
             PrettyPrintable (CommaObject o1 o2 m3) where
        pprint :: CommaObject o1 o2 m3 -> String
pprint CommaObject{indexSrc :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc=o1
e, indexTgt :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTgt=o2
d, arrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow=m3
f} = String
"<"String -> ShowS
forall a. [a] -> [a] -> [a]
++o1 -> String
forall a. PrettyPrintable a => a -> String
pprint o1
eString -> ShowS
forall a. [a] -> [a] -> [a]
++String
", "String -> ShowS
forall a. [a] -> [a] -> [a]
++o2 -> String
forall a. PrettyPrintable a => a -> String
pprint o2
dString -> ShowS
forall a. [a] -> [a] -> [a]
++String
", "String -> ShowS
forall a. [a] -> [a] -> [a]
++m3 -> String
forall a. PrettyPrintable a => a -> String
pprint m3
fString -> ShowS
forall a. [a] -> [a] -> [a]
++String
">"
    
    -- | A `CommaMorphism` in the `CommaCategory` (/T/|/S/) is a couple \</k/,/h/\>.

    --

    -- See /Categories for the working mathematician/, Saunders Mac Lane, P.46.

    data CommaMorphism o1 o2 m1 m2 m3 = CommaMorphism {forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
srcCM :: (CommaObject o1 o2 m3) -- ^ The source `CommaObject`

                                                     , forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
tgtCM :: (CommaObject o1 o2 m3) -- ^ The target `CommaObject`

                                                     , forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexAr1 :: m1 -- ^ /k/

                                                     , forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexAr2 :: m2} -- ^ /h/

                                                     deriving (CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3 -> Bool
(CommaMorphism o1 o2 m1 m2 m3
 -> CommaMorphism o1 o2 m1 m2 m3 -> Bool)
-> (CommaMorphism o1 o2 m1 m2 m3
    -> CommaMorphism o1 o2 m1 m2 m3 -> Bool)
-> Eq (CommaMorphism o1 o2 m1 m2 m3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall o1 o2 m1 m2 m3.
(Eq o1, Eq o2, Eq m3, Eq m1, Eq m2) =>
CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3 -> Bool
/= :: CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3 -> Bool
$c/= :: forall o1 o2 m1 m2 m3.
(Eq o1, Eq o2, Eq m3, Eq m1, Eq m2) =>
CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3 -> Bool
== :: CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3 -> Bool
$c== :: forall o1 o2 m1 m2 m3.
(Eq o1, Eq o2, Eq m3, Eq m1, Eq m2) =>
CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3 -> Bool
Eq, Int -> CommaMorphism o1 o2 m1 m2 m3 -> ShowS
[CommaMorphism o1 o2 m1 m2 m3] -> ShowS
CommaMorphism o1 o2 m1 m2 m3 -> String
(Int -> CommaMorphism o1 o2 m1 m2 m3 -> ShowS)
-> (CommaMorphism o1 o2 m1 m2 m3 -> String)
-> ([CommaMorphism o1 o2 m1 m2 m3] -> ShowS)
-> Show (CommaMorphism o1 o2 m1 m2 m3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall o1 o2 m1 m2 m3.
(Show o1, Show o2, Show m3, Show m1, Show m2) =>
Int -> CommaMorphism o1 o2 m1 m2 m3 -> ShowS
forall o1 o2 m1 m2 m3.
(Show o1, Show o2, Show m3, Show m1, Show m2) =>
[CommaMorphism o1 o2 m1 m2 m3] -> ShowS
forall o1 o2 m1 m2 m3.
(Show o1, Show o2, Show m3, Show m1, Show m2) =>
CommaMorphism o1 o2 m1 m2 m3 -> String
showList :: [CommaMorphism o1 o2 m1 m2 m3] -> ShowS
$cshowList :: forall o1 o2 m1 m2 m3.
(Show o1, Show o2, Show m3, Show m1, Show m2) =>
[CommaMorphism o1 o2 m1 m2 m3] -> ShowS
show :: CommaMorphism o1 o2 m1 m2 m3 -> String
$cshow :: forall o1 o2 m1 m2 m3.
(Show o1, Show o2, Show m3, Show m1, Show m2) =>
CommaMorphism o1 o2 m1 m2 m3 -> String
showsPrec :: Int -> CommaMorphism o1 o2 m1 m2 m3 -> ShowS
$cshowsPrec :: forall o1 o2 m1 m2 m3.
(Show o1, Show o2, Show m3, Show m1, Show m2) =>
Int -> CommaMorphism o1 o2 m1 m2 m3 -> ShowS
Show)
                                                     
    instance (PrettyPrintable m1, PrettyPrintable m2) =>
              PrettyPrintable (CommaMorphism o1 o2 m1 m2 m3) where
        pprint :: CommaMorphism o1 o2 m1 m2 m3 -> String
pprint CommaMorphism{srcCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
_, tgtCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
tgtCM =CommaObject o1 o2 m3
_, indexAr1 :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexAr1=m1
k, indexAr2 :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexAr2=m2
h} = String
"<"String -> ShowS
forall a. [a] -> [a] -> [a]
++m1 -> String
forall a. PrettyPrintable a => a -> String
pprint m1
kString -> ShowS
forall a. [a] -> [a] -> [a]
++String
", "String -> ShowS
forall a. [a] -> [a] -> [a]
++m2 -> String
forall a. PrettyPrintable a => a -> String
pprint m2
hString -> ShowS
forall a. [a] -> [a] -> [a]
++String
">"
    
    instance (Morphism m1 o1, Morphism m2 o2, Eq o1, Eq o2, Eq m3) => Morphism (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) where
        @ :: CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3
(@) CommaMorphism{srcCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
s2,tgtCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
t2,indexAr1 :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexAr1=m1
k2,indexAr2 :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexAr2=m2
h2} CommaMorphism{srcCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
s1,tgtCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
t1,indexAr1 :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexAr1=m1
k1,indexAr2 :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexAr2=m2
h1}
            | CommaObject o1 o2 m3
t1 CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool
forall a. Eq a => a -> a -> Bool
/= CommaObject o1 o2 m3
s2 = String -> CommaMorphism o1 o2 m1 m2 m3
forall a. HasCallStack => String -> a
error String
"Illegal composition of CommaMorphism."
            | Bool
otherwise = CommaMorphism :: forall o1 o2 m1 m2 m3.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
CommaMorphism {srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
s1,tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
t2,indexAr1 :: m1
indexAr1=m1
k2 m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ m1
k1,indexAr2 :: m2
indexAr2=m2
h2 m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ m2
h1}
        source :: CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
source = CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
srcCM
        target :: CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
target = CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
tgtCM
    
    -- | A `CommaCategory` is a couple (/T/|/S/) with /T/ and /S/ two diagrams with the same target.

    --

    -- See /Categories for the working mathematician/, Saunders Mac Lane, P.46.

    data CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = CommaCategory {forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
leftDiag :: Diagram c1 m1 o1 c3 m3 o3 -- ^ /T/

                                                                , forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
rightDiag :: Diagram c2 m2 o2 c3 m3 o3} -- ^ /S/

                                                    deriving (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
(CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool)
-> Eq (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c3, Eq o1, Eq o3, Eq m1, Eq m3, Eq c2, Eq o2, Eq m2) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
/= :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c3, Eq o1, Eq o3, Eq m1, Eq m3, Eq c2, Eq o2, Eq m2) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
== :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Eq c1, Eq c3, Eq o1, Eq o3, Eq m1, Eq m3, Eq c2, Eq o2, Eq m2) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> Bool
Eq, Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
[CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS)
-> (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> ([CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS)
-> Show (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
[CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showList :: [CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
[CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> ShowS
show :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
showsPrec :: Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Show c1, Show c3, Show o1, Show o3, Show m1, Show m3, Show c2,
 Show o2, Show m2) =>
Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> ShowS
Show)
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
              FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m3) => FiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) where
        ob :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> [CommaObject o1 o2 m3]
ob CommaCategory {leftDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
leftDiag = Diagram c1 m1 o1 c3 m3 o3
t, rightDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
rightDiag = Diagram c2 m2 o2 c3 m3 o3
s} = [CommaObject :: forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
CommaObject{indexSrc :: o1
indexSrc=o1
e,indexTgt :: o2
indexTgt=o2
d,arrow :: m3
arrow=m3
f}| o1
e <- (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
t)), o2
d <- (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob (Diagram c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c3 m3 o3
s)), m3
f <- (c3 -> o3 -> o3 -> [m3]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar (Diagram c1 m1 o1 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c3 m3 o3
t) ((Diagram c1 m1 o1 c3 m3 o3 -> AssociationList o1 o3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c3 m3 o3
t) AssociationList o1 o3 -> o1 -> o3
forall a b. Eq a => AssociationList a b -> a -> b
!-! (o1
e)) ((Diagram c2 m2 o2 c3 m3 o3 -> AssociationList o2 o3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c2 m2 o2 c3 m3 o3
s) AssociationList o2 o3 -> o2 -> o3
forall a b. Eq a => AssociationList a b -> a -> b
!-! (o2
d)))]
        identity :: Morphism (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaObject o1 o2 m3 -> CommaMorphism o1 o2 m1 m2 m3
identity CommaCategory{leftDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
leftDiag = Diagram c1 m1 o1 c3 m3 o3
t, rightDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
rightDiag = Diagram c2 m2 o2 c3 m3 o3
s} obj :: CommaObject o1 o2 m3
obj@CommaObject{indexSrc :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc=o1
e,indexTgt :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTgt=o2
d,arrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow=m3
f} 
            = CommaMorphism :: forall o1 o2 m1 m2 m3.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
obj, tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
obj, indexAr1 :: m1
indexAr1=(c1 -> o1 -> m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
t) o1
e), indexAr2 :: m2
indexAr2=(c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity (Diagram c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c3 m3 o3
s) o2
d)}
        ar :: Morphism (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaObject o1 o2 m3
-> CommaObject o1 o2 m3
-> [CommaMorphism o1 o2 m1 m2 m3]
ar CommaCategory{leftDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
leftDiag = Diagram c1 m1 o1 c3 m3 o3
t, rightDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
rightDiag = Diagram c2 m2 o2 c3 m3 o3
s} obj1 :: CommaObject o1 o2 m3
obj1@CommaObject{indexSrc :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc=o1
e1,indexTgt :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTgt=o2
d1,arrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow=m3
f1} obj2 :: CommaObject o1 o2 m3
obj2@CommaObject{indexSrc :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc=o1
e2,indexTgt :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTgt=o2
d2,arrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow=m3
f2}
            = [CommaMorphism :: forall o1 o2 m1 m2 m3.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
obj1,tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
obj2,indexAr1 :: m1
indexAr1=m1
k,indexAr2 :: m2
indexAr2=m2
h}| m1
k <- c1 -> o1 -> o1 -> [m1]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar (Diagram c1 m1 o1 c3 m3 o3 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c3 m3 o3
t) o1
e1 o1
e2, m2
h <- c2 -> o2 -> o2 -> [m2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar (Diagram c2 m2 o2 c3 m3 o3 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c3 m3 o3
s) o2
d1 o2
d2, m3
f2 m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ ((Diagram c1 m1 o1 c3 m3 o3 -> AssociationList m1 m3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c1 m1 o1 c3 m3 o3
t) AssociationList m1 m3 -> m1 -> m3
forall a b. Eq a => AssociationList a b -> a -> b
!-! (m1
k)) m3 -> m3 -> Bool
forall a. Eq a => a -> a -> Bool
== ((Diagram c2 m2 o2 c3 m3 o3 -> AssociationList m2 m3
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c2 m2 o2 c3 m3 o3
s) AssociationList m2 m3 -> m2 -> m3
forall a b. Eq a => AssociationList a b -> a -> b
!-! (m2
h)) m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ m3
f1]
                    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
              FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m3) => GeneratedFiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) where
        genAr :: Morphism (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaObject o1 o2 m3
-> CommaObject o1 o2 m3
-> [CommaMorphism o1 o2 m1 m2 m3]
genAr = CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaObject o1 o2 m3
-> CommaObject o1 o2 m3
-> [CommaMorphism o1 o2 m1 m2 m3]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
defaultGenAr
        decompose :: Morphism (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaMorphism o1 o2 m1 m2 m3 -> [CommaMorphism o1 o2 m1 m2 m3]
decompose = CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaMorphism o1 o2 m1 m2 m3 -> [CommaMorphism o1 o2 m1 m2 m3]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
defaultDecompose

    instance (PrettyPrintable c1, PrettyPrintable m1, PrettyPrintable o1,
              PrettyPrintable c2, PrettyPrintable m2, PrettyPrintable o2,
              PrettyPrintable c3, PrettyPrintable m3, PrettyPrintable o3,
              FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, FiniteCategory c3 m3 o3,
              Morphism m1 o1, Morphism m2 o2, Morphism m3 o3,
              Eq m1, Eq o1, Eq m2, Eq o2) =>
              PrettyPrintable (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        pprint :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint CommaCategory{leftDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
leftDiag=Diagram c1 m1 o1 c3 m3 o3
t, rightDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
rightDiag=Diagram c2 m2 o2 c3 m3 o3
s} = String
"("String -> ShowS
forall a. [a] -> [a] -> [a]
++Diagram c1 m1 o1 c3 m3 o3 -> String
forall a. PrettyPrintable a => a -> String
pprint Diagram c1 m1 o1 c3 m3 o3
tString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"|"String -> ShowS
forall a. [a] -> [a] -> [a]
++Diagram c2 m2 o2 c3 m3 o3 -> String
forall a. PrettyPrintable a => a -> String
pprint Diagram c2 m2 o2 c3 m3 o3
sString -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"

    -- | Constructs the slice category of a category /C/ over an object /o/.

    --

    -- Returns Nothing if the object is not in the category.

    mkSliceCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (CommaCategory c m o One One One c m o)
    mkSliceCategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (CommaCategory c m o One One One c m o)
mkSliceCategory c
c o
o = c -> o -> Maybe (Diagram One One One c m o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 c
c o
o Maybe (Diagram One One One c m o)
-> (Diagram One One One c m o
    -> Maybe (CommaCategory c m o One One One c m o))
-> Maybe (CommaCategory c m o One One One c m o)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Diagram One One One c m o
x -> CommaCategory c m o One One One c m o
-> Maybe (CommaCategory c m o One One One c m o)
forall a. a -> Maybe a
Just 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 c m o c m o
leftDiag=c -> Diagram c m o c m o
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Diagram c m o c m o
mkIdentityDiagram c
c, rightDiag :: Diagram One One One c m o
rightDiag=Diagram One One One c m o
x})
        
    -- | Constructs the coslice category of a category /C/ under an object /o/.

    --

    -- Returns Nothing if the object is not in the category.

    mkCosliceCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (CommaCategory One One One c m o c m o)
    mkCosliceCategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (CommaCategory One One One c m o c m o)
mkCosliceCategory c
c o
o = c -> o -> Maybe (Diagram One One One c m o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 c
c o
o Maybe (Diagram One One One c m o)
-> (Diagram One One One c m o
    -> Maybe (CommaCategory One One One c m o c m o))
-> Maybe (CommaCategory One One One c m o c m o)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Diagram One One One c m o
x -> CommaCategory One One One c m o c m o
-> Maybe (CommaCategory One One One c m o c m o)
forall a. a -> Maybe a
Just 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{rightDiag :: Diagram c m o c m o
rightDiag=c -> Diagram c m o c m o
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Diagram c m o c m o
mkIdentityDiagram c
c, leftDiag :: Diagram One One One c m o
leftDiag=Diagram One One One c m o
x})
        
    -- | Constructs the arrow category of a category /C/.

    mkArrowCategory :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> CommaCategory c m o c m o c m o
    mkArrowCategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> CommaCategory c m o c m o c m o
mkArrowCategory c
c = 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 c m o c m o
leftDiag=c -> Diagram c m o c m o
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Diagram c m o c m o
mkIdentityDiagram c
c, rightDiag :: Diagram c m o c m o
rightDiag=c -> Diagram c m o c m o
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Diagram c m o c m o
mkIdentityDiagram c
c}