{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}

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

Each 'Category' has an opposite one where morphisms are reversed.

A 'CommaCategory' is intuitively a category where objects are selected morphisms of another category /C/ and morphisms are selected commutative squares in /C/.

More precisely, given two 'Diagram's @/T/ : /E/ -> /C/@ and @/S/ : /D/ -> /C/@, a `CommaObject` in the `CommaCategory` (/T/|/S/) is a triplet \<e,d,f\> where @f : /T/(e) -> /S/(d)@.

A `CommaMorphism` from \<e1,d1,f1\> to \<e2,d2,f2\> in the `CommaCategory` (/T/|/S/) is a couple \<k,h\> where @/T/(k) : /T/(e1) -> /T/(e2)@, @/S/(h) : /S/(d1) -> /S/(d2)@ such that @f2 \@ /T/(k) = /S/(h) \@ f1@.

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

If the category /C/ is a 'FiniteCategory', then the 'CommaCategory' of /C/ is also a 'FiniteCategory'. Otherwise it is only a 'Category'.
-}

module Math.Categories.CommaCategory
(
    -- * Comma object

    CommaObject,
    -- ** Getters

    indexSource,
    indexTarget,
    selectedArrow,
    -- ** Smart constructors

    commaObject,
    unsafeCommaObject,
    -- * Comma morphism

    CommaMorphism,
    -- ** Getters

    indexFirstArrow,
    indexSecondArrow,
    -- ** Smart constructors

    commaMorphism,
    unsafeCommaMorphism,
    CommaCategory(..),
    sliceCategory,
    cosliceCategory,
    arrowCategory, 
)
where
    import   qualified  Data.WeakSet        as Set
    import              Data.WeakSet          (Set)
    import              Data.WeakSet.Safe
    import   qualified  Data.WeakMap        as Map
    import              Data.WeakMap          (Map)
    import              Data.WeakMap.Safe
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.Categories.FinCat
    import              Math.Categories.FunctorCategory
    import              Math.FiniteCategories.One
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    -- | 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.

    --

    -- The 'CommaObject' constructor is private, use the smart constructor 'commaObject' or the unsafe one 'unsafeCommaObject'.

    data CommaObject o1 o2 m3 = CommaObject { forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource :: o1 -- ^ e, the indexing object of the source of the 'selectedArrow'.

                                            , forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget :: o2 -- ^ d, the indexing object of the target of the 'selectedArrow'.

                                            , forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow :: m3 -- ^ f, the selected arrow of the target category.

                                            } 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
$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
/= :: CommaObject o1 o2 m3 -> CommaObject o1 o2 m3 -> Bool
Eq, (forall x. CommaObject o1 o2 m3 -> Rep (CommaObject o1 o2 m3) x)
-> (forall x. Rep (CommaObject o1 o2 m3) x -> CommaObject o1 o2 m3)
-> Generic (CommaObject o1 o2 m3)
forall x. Rep (CommaObject o1 o2 m3) x -> CommaObject o1 o2 m3
forall x. CommaObject o1 o2 m3 -> Rep (CommaObject o1 o2 m3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall o1 o2 m3 x.
Rep (CommaObject o1 o2 m3) x -> CommaObject o1 o2 m3
forall o1 o2 m3 x.
CommaObject o1 o2 m3 -> Rep (CommaObject o1 o2 m3) x
$cfrom :: forall o1 o2 m3 x.
CommaObject o1 o2 m3 -> Rep (CommaObject o1 o2 m3) x
from :: forall x. CommaObject o1 o2 m3 -> Rep (CommaObject o1 o2 m3) x
$cto :: forall o1 o2 m3 x.
Rep (CommaObject o1 o2 m3) x -> CommaObject o1 o2 m3
to :: forall x. Rep (CommaObject o1 o2 m3) x -> CommaObject o1 o2 m3
Generic, CommaObject o1 o2 m3 -> CommaObject o1 o2 m3
(CommaObject o1 o2 m3 -> CommaObject o1 o2 m3)
-> Simplifiable (CommaObject o1 o2 m3)
forall a. (a -> a) -> Simplifiable a
forall o1 o2 m3.
(Simplifiable o1, Simplifiable o2, Simplifiable m3) =>
CommaObject o1 o2 m3 -> CommaObject o1 o2 m3
$csimplify :: forall o1 o2 m3.
(Simplifiable o1, Simplifiable o2, Simplifiable m3) =>
CommaObject o1 o2 m3 -> CommaObject o1 o2 m3
simplify :: CommaObject o1 o2 m3 -> CommaObject o1 o2 m3
Simplifiable)
    
    instance (PrettyPrint o1, PrettyPrint o2, PrettyPrint m3) =>
             PrettyPrint (CommaObject o1 o2 m3) where
        pprint :: Int -> CommaObject o1 o2 m3 -> String
pprint Int
0 CommaObject o1 o2 m3
_ = String
"..."
        pprint Int
v CommaObject{indexSource :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource=o1
e, indexTarget :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget=o2
d, selectedArrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow=m3
f} = String
"<"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> o1 -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) o1
eString -> String -> String
forall a. [a] -> [a] -> [a]
++String
", "String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> o2 -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) o2
dString -> String -> String
forall a. [a] -> [a] -> [a]
++String
", "String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> m3 -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) m3
fString -> String -> String
forall a. [a] -> [a] -> [a]
++String
">"
        
        -- pprintWithIndentations 0 ov indent _ = indentation ov indent ++ "...\n"

        -- pprintWithIndentations cv ov indent CommaObject{indexSource=e, indexTarget=d, selectedArrow=f} = indentation (ov - cv) indent ++ "<"++pprint (cv-1) e++", "++pprint (cv-1) d++", "++pprint (cv-1) f++">\n"

        
    instance (Show o1, Show o2, Show m3) =>
            Show (CommaObject o1 o2 m3) where
        show :: CommaObject o1 o2 m3 -> String
show CommaObject{indexSource :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource=o1
e, indexTarget :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget=o2
d, selectedArrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow=m3
f} = String
"(unsafeCommaObject ("String -> String -> String
forall a. [a] -> [a] -> [a]
++ o1 -> String
forall a. Show a => a -> String
show o1
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ o2 -> String
forall a. Show a => a -> String
show o2
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ m3 -> String
forall a. Show a => a -> String
show m3
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"        

    -- | Smart constructor of 'CommaObject' which checks the structure of the 'CommaObject'.

    commaObject :: (Morphism m3 o3, Eq o1, Eq o2, Eq o3) => Diagram c1 m1 o1 c3 m3 o3 -> Diagram c2 m2 o2 c3 m3 o3 -> o1 -> o2 -> m3 -> Maybe (CommaObject o1 o2 m3)
    commaObject :: forall m3 o3 o1 o2 c1 m1 c3 c2 m2.
(Morphism m3 o3, Eq o1, Eq o2, Eq o3) =>
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> o1
-> o2
-> m3
-> Maybe (CommaObject o1 o2 m3)
commaObject Diagram c1 m1 o1 c3 m3 o3
d1 Diagram c2 m2 o2 c3 m3 o3
d2 o1
iS o2
iT m3
arr
        | Diagram c1 m1 o1 c3 m3 o3
d1 Diagram c1 m1 o1 c3 m3 o3 -> o1 -> o3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
iS o3 -> o3 -> Bool
forall a. Eq a => a -> a -> Bool
== (m3 -> o3
forall m o. Morphism m o => m -> o
source m3
arr) Bool -> Bool -> Bool
&& Diagram c2 m2 o2 c3 m3 o3
d2 Diagram c2 m2 o2 c3 m3 o3 -> o2 -> o3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o2
iT o3 -> o3 -> Bool
forall a. Eq a => a -> a -> Bool
== (m3 -> o3
forall m o. Morphism m o => m -> o
target m3
arr) = CommaObject o1 o2 m3 -> Maybe (CommaObject o1 o2 m3)
forall a. a -> Maybe a
Just CommaObject{indexSource :: o1
indexSource=o1
iS, indexTarget :: o2
indexTarget=o2
iT,selectedArrow :: m3
selectedArrow=m3
arr}
        | Bool
otherwise = Maybe (CommaObject o1 o2 m3)
forall a. Maybe a
Nothing
    
    -- | Unsafe way of constructing a 'CommaObject' : the structure of the 'CommaObject' 

    unsafeCommaObject :: o1 -> o2 -> m3 -> CommaObject o1 o2 m3
    unsafeCommaObject :: forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject o1
iS o2
iT m3
arr = CommaObject{indexSource :: o1
indexSource=o1
iS, indexTarget :: o2
indexTarget=o2
iT,selectedArrow :: m3
selectedArrow=m3
arr}
        
    -- | A `CommaMorphism` from \<e1,d1,f1\> to \<e2,d2,f2\> in the `CommaCategory` (/T/|/S/) is a couple \<k,h\> where @/T/(k) : /T/(e1) -> /T/(e2)@, @/S/(h) : /S/(d1) -> /S/(d2)@ such that @f2 \@ /T/(k) = /S/(h) \@ f1@.

    --

    -- 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` (private, use 'source' instead).

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

                                                     , forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow :: m1 -- ^ k, the indexing arrow of the first functor.

                                                     , forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow :: m2} -- ^ h, the indexing arrow of the second functor.

                                                     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
$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
/= :: CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3 -> Bool
Eq, (forall x.
 CommaMorphism o1 o2 m1 m2 m3
 -> Rep (CommaMorphism o1 o2 m1 m2 m3) x)
-> (forall x.
    Rep (CommaMorphism o1 o2 m1 m2 m3) x
    -> CommaMorphism o1 o2 m1 m2 m3)
-> Generic (CommaMorphism o1 o2 m1 m2 m3)
forall x.
Rep (CommaMorphism o1 o2 m1 m2 m3) x
-> CommaMorphism o1 o2 m1 m2 m3
forall x.
CommaMorphism o1 o2 m1 m2 m3
-> Rep (CommaMorphism o1 o2 m1 m2 m3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall o1 o2 m1 m2 m3 x.
Rep (CommaMorphism o1 o2 m1 m2 m3) x
-> CommaMorphism o1 o2 m1 m2 m3
forall o1 o2 m1 m2 m3 x.
CommaMorphism o1 o2 m1 m2 m3
-> Rep (CommaMorphism o1 o2 m1 m2 m3) x
$cfrom :: forall o1 o2 m1 m2 m3 x.
CommaMorphism o1 o2 m1 m2 m3
-> Rep (CommaMorphism o1 o2 m1 m2 m3) x
from :: forall x.
CommaMorphism o1 o2 m1 m2 m3
-> Rep (CommaMorphism o1 o2 m1 m2 m3) x
$cto :: forall o1 o2 m1 m2 m3 x.
Rep (CommaMorphism o1 o2 m1 m2 m3) x
-> CommaMorphism o1 o2 m1 m2 m3
to :: forall x.
Rep (CommaMorphism o1 o2 m1 m2 m3) x
-> CommaMorphism o1 o2 m1 m2 m3
Generic, CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3
(CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3)
-> Simplifiable (CommaMorphism o1 o2 m1 m2 m3)
forall a. (a -> a) -> Simplifiable a
forall o1 o2 m1 m2 m3.
(Simplifiable o1, Simplifiable o2, Simplifiable m3,
 Simplifiable m1, Simplifiable m2) =>
CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3
$csimplify :: forall o1 o2 m1 m2 m3.
(Simplifiable o1, Simplifiable o2, Simplifiable m3,
 Simplifiable m1, Simplifiable m2) =>
CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3
simplify :: CommaMorphism o1 o2 m1 m2 m3 -> CommaMorphism o1 o2 m1 m2 m3
Simplifiable)
    
    -- | Smart constructor of 'CommaMorphism', checks the structure of the 'CommaMorphism' at construction.

    commaMorphism :: (Category c1 m1 o1, Morphism m1 o1, Category c2 m2 o2, Morphism m2 o2, Morphism m3 o3, Eq o1, Eq o2, Eq o3, Eq m1, Eq m2, Eq m3) => Diagram c1 m1 o1 c3 m3 o3 -> Diagram c2 m2 o2 c3 m3 o3 -> (CommaObject o1 o2 m3) -> (CommaObject o1 o2 m3) -> m1 -> m2 -> Maybe (CommaMorphism o1 o2 m1 m2 m3)
    commaMorphism :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2, Morphism m3 o3, Eq o1, Eq o2, Eq o3, Eq m1, Eq m2,
 Eq m3) =>
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaObject o1 o2 m3
-> CommaObject o1 o2 m3
-> m1
-> m2
-> Maybe (CommaMorphism o1 o2 m1 m2 m3)
commaMorphism Diagram c1 m1 o1 c3 m3 o3
d1 Diagram c2 m2 o2 c3 m3 o3
d2 CommaObject o1 o2 m3
s CommaObject o1 o2 m3
t m1
firstArr m2
secondArr
        | Maybe m3 -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe m3
m1 Bool -> Bool -> Bool
|| Maybe m3 -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe m3
m2 Bool -> Bool -> Bool
|| Maybe m3
m1 Maybe m3 -> Maybe m3 -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe m3
m2 = Maybe (CommaMorphism o1 o2 m1 m2 m3)
forall a. Maybe a
Nothing
        | Bool
otherwise = CommaMorphism o1 o2 m1 m2 m3
-> Maybe (CommaMorphism o1 o2 m1 m2 m3)
forall a. a -> Maybe a
Just CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
s, tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
t, indexFirstArrow :: m1
indexFirstArrow=m1
firstArr, indexSecondArrow :: m2
indexSecondArrow=m2
secondArr}
        where
            m1 :: Maybe m3
m1 = (CommaObject o1 o2 m3 -> m3
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject o1 o2 m3
t) m3 -> m3 -> Maybe m3
forall m o. (Morphism m o, Eq o) => m -> m -> Maybe m
@? (Diagram c1 m1 o1 c3 m3 o3
d1 Diagram c1 m1 o1 c3 m3 o3 -> m1 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
firstArr)
            m2 :: Maybe m3
m2 = (Diagram c2 m2 o2 c3 m3 o3
d2 Diagram c2 m2 o2 c3 m3 o3 -> m2 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m2
secondArr) m3 -> m3 -> Maybe m3
forall m o. (Morphism m o, Eq o) => m -> m -> Maybe m
@? (CommaObject o1 o2 m3 -> m3
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject o1 o2 m3
s)
            
    -- | Unsafe constructor of 'CommaMorphism', does not check the structure of the 'CommaMorphism'.

    unsafeCommaMorphism :: (CommaObject o1 o2 m3) -> (CommaObject o1 o2 m3) -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
    unsafeCommaMorphism :: forall o1 o2 m3 m1 m2.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
unsafeCommaMorphism CommaObject o1 o2 m3
s CommaObject o1 o2 m3
t m1
firstArr m2
secondArr = CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
s, tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
t, indexFirstArrow :: m1
indexFirstArrow=m1
firstArr, indexSecondArrow :: m2
indexSecondArrow=m2
secondArr}
        
    instance (Show o1, Show o2, Show m1, Show m2, Show m3) => 
            Show (CommaMorphism o1 o2 m1 m2 m3) where
        show :: CommaMorphism o1 o2 m1 m2 m3 -> String
show CommaMorphism{srcCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
s, tgtCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
tgtCM =CommaObject o1 o2 m3
t, indexFirstArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow=m1
k, indexSecondArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow=m2
h} = String
"(unsafeCommaMorphism ("String -> String -> String
forall a. [a] -> [a] -> [a]
++CommaObject o1 o2 m3 -> String
forall a. Show a => a -> String
show CommaObject o1 o2 m3
sString -> String -> String
forall a. [a] -> [a] -> [a]
++String
") ("String -> String -> String
forall a. [a] -> [a] -> [a]
++CommaObject o1 o2 m3 -> String
forall a. Show a => a -> String
show CommaObject o1 o2 m3
tString -> String -> String
forall a. [a] -> [a] -> [a]
++String
") ("String -> String -> String
forall a. [a] -> [a] -> [a]
++m1 -> String
forall a. Show a => a -> String
show m1
kString -> String -> String
forall a. [a] -> [a] -> [a]
++String
") ("String -> String -> String
forall a. [a] -> [a] -> [a]
++m2 -> String
forall a. Show a => a -> String
show m2
hString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"))"
        
    instance (PrettyPrint m1, PrettyPrint m2, PrettyPrint o1, PrettyPrint o2, PrettyPrint m3) =>
              PrettyPrint (CommaMorphism o1 o2 m1 m2 m3) where
        pprint :: Int -> CommaMorphism o1 o2 m1 m2 m3 -> String
pprint Int
0 CommaMorphism o1 o2 m1 m2 m3
_ = String
"..."
        pprint Int
v 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
_, indexFirstArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow=m1
k, indexSecondArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow=m2
h} = String
"<"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> m1 -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) m1
kString -> String -> String
forall a. [a] -> [a] -> [a]
++String
", "String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> m2 -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) m2
hString -> String -> String
forall a. [a] -> [a] -> [a]
++String
">"
    
        -- pprintWithIndentations 0 ov indent _ = indentation ov indent ++ "...\n"

        -- pprintWithIndentations cv ov indent CommaMorphism{srcCM=_, tgtCM =_, indexFirstArrow=k, indexSecondArrow=h} = indentation (ov - cv) indent ++ "<"++pprint (cv-1) k++", "++pprint (cv-1) h++">\n"

    
    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
        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
        
        @? :: Eq (CommaObject o1 o2 m3) =>
CommaMorphism o1 o2 m1 m2 m3
-> CommaMorphism o1 o2 m1 m2 m3
-> Maybe (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,indexFirstArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow=m1
k2,indexSecondArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow=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,indexFirstArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow=m1
k1,indexSecondArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow=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 = Maybe (CommaMorphism o1 o2 m1 m2 m3)
forall a. Maybe a
Nothing
            | Maybe m1 -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe m1
compoK = Maybe (CommaMorphism o1 o2 m1 m2 m3)
forall a. Maybe a
Nothing
            | Maybe m2 -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe m2
compoH = Maybe (CommaMorphism o1 o2 m1 m2 m3)
forall a. Maybe a
Nothing
            | Bool
otherwise = CommaMorphism o1 o2 m1 m2 m3
-> Maybe (CommaMorphism o1 o2 m1 m2 m3)
forall a. a -> Maybe a
Just CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
s1,tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
t2,indexFirstArrow :: m1
indexFirstArrow=m1
k,indexSecondArrow :: m2
indexSecondArrow=m2
h}
            where
                compoK :: Maybe m1
compoK = m1
k2 m1 -> m1 -> Maybe m1
forall m o. (Morphism m o, Eq o) => m -> m -> Maybe m
@? m1
k1
                Just m1
k = Maybe m1
compoK
                compoH :: Maybe m2
compoH = m2
h2 m2 -> m2 -> Maybe m2
forall m o. (Morphism m o, Eq o) => m -> m -> Maybe m
@? m2
h1
                Just m2
h = Maybe m2
compoH
        
        @ :: 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,indexFirstArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow=m1
k2,indexSecondArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow=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,indexFirstArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow=m1
k1,indexSecondArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow=m2
h1} = CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
s1,tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
t2,indexFirstArrow :: m1
indexFirstArrow = m1
k2 m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ m1
k1,indexSecondArrow :: m2
indexSecondArrow = m2
h2 m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ m2
h1}
        
    -- | 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
leftDiagram :: 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
rightDiagram :: 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 m1, Eq o1, Eq c3, Eq m3, Eq o3, Eq c2, Eq m2, Eq o2,
 FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
 Morphism m2 o2) =>
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 m1, Eq o1, Eq c3, Eq m3, Eq o3, Eq c2, Eq m2, Eq o2,
 FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
 Morphism m2 o2) =>
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 m1, Eq o1, Eq c3, Eq m3, Eq o3, Eq c2, Eq m2, Eq o2,
 FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
 Morphism m2 o2) =>
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, Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String -> String
[CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> String -> String
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int
 -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String -> String)
-> (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> ([CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> String -> String)
-> Show (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> 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 -> String -> String
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 -> String
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
$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 -> String -> String
showsPrec :: Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String -> 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
show :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$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] -> String -> String
showList :: [CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3] -> String -> String
Show, (forall x.
 CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x)
-> (forall x.
    Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
    -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Generic (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall x.
Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall x.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cfrom :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
from :: forall x.
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
$cto :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3 x.
Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
to :: forall x.
Rep (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) x
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Generic, Int
-> Int
-> String
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
(Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> (Int
    -> Int
    -> String
    -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> String)
-> (Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String)
-> PrettyPrint (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
 PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
 PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int
-> Int
-> String
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
 PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
 PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprint :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
 PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
 PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprint :: Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
$cpprintWithIndentations :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
 PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
 PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int
-> Int
-> String
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> String
$cpprintIndent :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(PrettyPrint c1, PrettyPrint c3, PrettyPrint o1, PrettyPrint o3,
 PrettyPrint m1, PrettyPrint m3, PrettyPrint c2, PrettyPrint o2,
 PrettyPrint m2, Eq o1, Eq o3, Eq m1, Eq m3, Eq o2, Eq m2) =>
Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
pprintIndent :: Int -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> String
PrettyPrint, CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
(CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
 -> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
-> Simplifiable (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3)
forall a. (a -> a) -> Simplifiable a
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Simplifiable c1, Simplifiable c3, Simplifiable o1,
 Simplifiable o3, Simplifiable m1, Simplifiable m3, Simplifiable c2,
 Simplifiable o2, Simplifiable m2, Eq o1, Eq m1, Eq o2, Eq m2) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
$csimplify :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(Simplifiable c1, Simplifiable c3, Simplifiable o1,
 Simplifiable o3, Simplifiable m1, Simplifiable m3, Simplifiable c2,
 Simplifiable o2, Simplifiable m2, Eq o1, Eq m1, Eq o2, Eq m2) =>
CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
simplify :: CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
Simplifiable)
    
                                                    
    instance (Category c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
              Category c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
              Category c3 m3 o3, Morphism m3 o3, Eq m3, Eq o3) => Category (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) where
        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 c1 m1 o1 c2 m2 o2 c3 m3 o3
cc CommaObject o1 o2 m3
co = CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM = CommaObject o1 o2 m3
co, tgtCM :: CommaObject o1 o2 m3
tgtCM = CommaObject o1 o2 m3
co, indexFirstArrow :: m1
indexFirstArrow = ((c1 -> o1 -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity(c1 -> o1 -> m1)
-> (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> c1)
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> o1
-> m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.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 -> c1)
-> (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> Diagram c1 m1 o1 c3 m3 o3)
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c3 m3 o3
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
leftDiagram (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> o1 -> m1)
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> o1 -> m1
forall a b. (a -> b) -> a -> b
$ CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
cc) (CommaObject o1 o2 m3 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o1 o2 m3
co)), indexSecondArrow :: m2
indexSecondArrow = ((c2 -> o2 -> m2
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity(c2 -> o2 -> m2)
-> (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> c2)
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> o2
-> m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.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 -> c2)
-> (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
    -> Diagram c2 m2 o2 c3 m3 o3)
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
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
rightDiagram (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> o2 -> m2)
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 -> o2 -> m2
forall a b. (a -> b) -> a -> b
$ CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
cc) (CommaObject o1 o2 m3 -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o1 o2 m3
co))}
        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
-> Set (CommaMorphism o1 o2 m1 m2 m3)
ar CommaCategory{leftDiagram :: 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
leftDiagram = Diagram c1 m1 o1 c3 m3 o3
t, rightDiagram :: 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
rightDiagram = Diagram c2 m2 o2 c3 m3 o3
s} obj1 :: CommaObject o1 o2 m3
obj1@CommaObject{indexSource :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource=o1
e1,indexTarget :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget=o2
d1,selectedArrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow=m3
f1} obj2 :: CommaObject o1 o2 m3
obj2@CommaObject{indexSource :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource=o1
e2,indexTarget :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget=o2
d2,selectedArrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow=m3
f2}
            = [CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
obj1,tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
obj2,indexFirstArrow :: m1
indexFirstArrow=m1
k,indexSecondArrow :: m2
indexSecondArrow=m2
h}| m1
k <- c1 -> o1 -> o1 -> Set m1
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set 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 -> Set m2
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set 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
t Diagram c1 m1 o1 c3 m3 o3 -> m1 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
k) m3 -> m3 -> Bool
forall a. Eq a => a -> a -> Bool
== (Diagram c2 m2 o2 c3 m3 o3
s Diagram c2 m2 o2 c3 m3 o3 -> m2 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m2
h) m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ m3
f1]
            
        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
-> Set (CommaMorphism o1 o2 m1 m2 m3)
genAr CommaCategory{leftDiagram :: 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
leftDiagram = Diagram c1 m1 o1 c3 m3 o3
t, rightDiagram :: 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
rightDiagram = Diagram c2 m2 o2 c3 m3 o3
s} obj1 :: CommaObject o1 o2 m3
obj1@CommaObject{indexSource :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource=o1
e1,indexTarget :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget=o2
d1,selectedArrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow=m3
f1} obj2 :: CommaObject o1 o2 m3
obj2@CommaObject{indexSource :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource=o1
e2,indexTarget :: forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget=o2
d2,selectedArrow :: forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow=m3
f2}
            | o2
d1 o2 -> o2 -> Bool
forall a. Eq a => a -> a -> Bool
== o2
d2 = [CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
obj1,tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
obj2,indexFirstArrow :: m1
indexFirstArrow=m1
k,indexSecondArrow :: m2
indexSecondArrow=c2 -> o2 -> m2
forall c m o. (Category 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
d1}| m1
k <- c1 -> o1 -> o1 -> Set m1
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr (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, m3
f2 m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ (Diagram c1 m1 o1 c3 m3 o3
t Diagram c1 m1 o1 c3 m3 o3 -> m1 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
k) m3 -> m3 -> Bool
forall a. Eq a => a -> a -> Bool
== m3
f1]
            | o1
e1 o1 -> o1 -> Bool
forall a. Eq a => a -> a -> Bool
== o1
e2 = [CommaMorphism{srcCM :: CommaObject o1 o2 m3
srcCM=CommaObject o1 o2 m3
obj1,tgtCM :: CommaObject o1 o2 m3
tgtCM=CommaObject o1 o2 m3
obj2,indexFirstArrow :: m1
indexFirstArrow=c1 -> o1 -> m1
forall c m o. (Category 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
e1,indexSecondArrow :: m2
indexSecondArrow=m2
h}| m2
h <- c2 -> o2 -> o2 -> Set m2
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr (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 -> Bool
forall a. Eq a => a -> a -> Bool
== (Diagram c2 m2 o2 c3 m3 o3
s Diagram c2 m2 o2 c3 m3 o3 -> m2 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m2
h) m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ m3
f1]
            | Bool
otherwise = [CommaMorphism o1 o2 m1 m2 m3]
-> Set (CommaMorphism o1 o2 m1 m2 m3)
forall a. [a] -> Set a
set []
            
        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
cc CommaMorphism o1 o2 m1 m2 m3
cm
            | [CommaMorphism o1 o2 m1 m2 m3] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CommaMorphism o1 o2 m1 m2 m3]
hyp Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = [CommaMorphism o1 o2 m1 m2 m3]
hyp
            | Bool
otherwise = (CommaMorphism o1 o2 m1 m2 m3 -> Bool)
-> [CommaMorphism o1 o2 m1 m2 m3] -> [CommaMorphism o1 o2 m1 m2 m3]
forall a. (a -> Bool) -> [a] -> [a]
filter (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaMorphism o1 o2 m1 m2 m3 -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
cc) [CommaMorphism o1 o2 m1 m2 m3]
hyp
            where
                hyp :: [CommaMorphism o1 o2 m1 m2 m3]
hyp = CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
-> CommaMorphism o1 o2 m1 m2 m3 -> [CommaMorphism o1 o2 m1 m2 m3]
forall {m1} {o} {m3} {o} {m1} {o} {c1} {c2} {c}.
(Eq m1, Eq o, Eq m3, Eq o, Eq m1, Eq o, Category c1 m1 o,
 Category c2 m3 o, Category c m1 o, Morphism m1 o, Morphism m3 o,
 Morphism m1 o) =>
CommaCategory c m1 o c1 m1 o c2 m3 o
-> CommaMorphism o o m1 m1 m3 -> [CommaMorphism o o m1 m1 m3]
decomposeHelper CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
cc CommaMorphism o1 o2 m1 m2 m3
cm
                decomposeHelper :: CommaCategory c m1 o c1 m1 o c2 m3 o
-> CommaMorphism o o m1 m1 m3 -> [CommaMorphism o o m1 m1 m3]
decomposeHelper cc :: CommaCategory c m1 o c1 m1 o c2 m3 o
cc@CommaCategory{leftDiagram :: 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
leftDiagram = Diagram c m1 o c2 m3 o
t, rightDiagram :: 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
rightDiagram = Diagram c1 m1 o c2 m3 o
s} cm :: CommaMorphism o o m1 m1 m3
cm@CommaMorphism{srcCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
srcCM=CommaObject o o m3
xfy,tgtCM :: forall o1 o2 m1 m2 m3.
CommaMorphism o1 o2 m1 m2 m3 -> CommaObject o1 o2 m3
tgtCM=CommaObject o o m3
x'gy',indexFirstArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
indexFirstArrow=m1
h,indexSecondArrow :: forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
indexSecondArrow=m1
i}
                    | CommaObject o o m3
xfy CommaObject o o m3 -> CommaObject o o m3 -> Bool
forall a. Eq a => a -> a -> Bool
== CommaObject o o m3
x'gy' = [CommaCategory c m1 o c1 m1 o c2 m3 o
-> CommaObject o o m3 -> CommaMorphism o o m1 m1 m3
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity CommaCategory c m1 o c1 m1 o c2 m3 o
cc CommaObject o o m3
xfy]
                    | CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
xfy o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
x'gy' = CommaMorphism o o m1 m1 m3
resultTCommaMorphism o o m1 m1 m3
-> [CommaMorphism o o m1 m1 m3] -> [CommaMorphism o o m1 m1 m3]
forall a. a -> [a] -> [a]
:(CommaCategory c m1 o c1 m1 o c2 m3 o
-> CommaMorphism o o m1 m1 m3 -> [CommaMorphism o o m1 m1 m3]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose CommaCategory c m1 o c1 m1 o c2 m3 o
cc (CommaObject o o m3
-> CommaObject o o m3 -> m1 -> m1 -> CommaMorphism o o m1 m1 m3
forall o1 o2 m3 m1 m2.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
unsafeCommaMorphism CommaObject o o m3
xfy (CommaMorphism o o m1 m1 m3 -> CommaObject o o m3
forall m o. Morphism m o => m -> o
source CommaMorphism o o m1 m1 m3
resultT) m1
composeAboveH (c1 -> o -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c1 m1 o c2 m3 o -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o c2 m3 o
s) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
xfy))))
                    | CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
xfy o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
x'gy' = (CommaCategory c m1 o c1 m1 o c2 m3 o
-> CommaMorphism o o m1 m1 m3 -> [CommaMorphism o o m1 m1 m3]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose CommaCategory c m1 o c1 m1 o c2 m3 o
cc (CommaObject o o m3
-> CommaObject o o m3 -> m1 -> m1 -> CommaMorphism o o m1 m1 m3
forall o1 o2 m3 m1 m2.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
unsafeCommaMorphism (CommaMorphism o o m1 m1 m3 -> CommaObject o o m3
forall m o. Morphism m o => m -> o
target CommaMorphism o o m1 m1 m3
resultI) (CommaMorphism o o m1 m1 m3 -> CommaObject o o m3
forall m o. Morphism m o => m -> o
target CommaMorphism o o m1 m1 m3
cm) (c -> o -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c m1 o c2 m3 o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c m1 o c2 m3 o
t) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
xfy)) m1
composeBelowI))[CommaMorphism o o m1 m1 m3]
-> [CommaMorphism o o m1 m1 m3] -> [CommaMorphism o o m1 m1 m3]
forall a. [a] -> [a] -> [a]
++[CommaMorphism o o m1 m1 m3
resultI]
                    | Bool
otherwise = CommaCategory c m1 o c1 m1 o c2 m3 o
-> CommaMorphism o o m1 m1 m3 -> [CommaMorphism o o m1 m1 m3]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose CommaCategory c m1 o c1 m1 o c2 m3 o
cc (CommaObject o o m3
-> CommaObject o o m3 -> m1 -> m1 -> CommaMorphism o o m1 m1 m3
forall o1 o2 m3 m1 m2.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
unsafeCommaMorphism (o -> o -> m3 -> CommaObject o o m3
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
xfy) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
x'gy') (Diagram c1 m1 o c2 m3 o
s Diagram c1 m1 o c2 m3 o -> m1 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
i m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ (CommaObject o o m3 -> m3
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject o o m3
xfy))) CommaObject o o m3
x'gy' m1
h (c1 -> o -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c1 m1 o c2 m3 o -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o c2 m3 o
s) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
x'gy'))) [CommaMorphism o o m1 m1 m3]
-> [CommaMorphism o o m1 m1 m3] -> [CommaMorphism o o m1 m1 m3]
forall a. [a] -> [a] -> [a]
++ CommaCategory c m1 o c1 m1 o c2 m3 o
-> CommaMorphism o o m1 m1 m3 -> [CommaMorphism o o m1 m1 m3]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose CommaCategory c m1 o c1 m1 o c2 m3 o
cc (CommaObject o o m3
-> CommaObject o o m3 -> m1 -> m1 -> CommaMorphism o o m1 m1 m3
forall o1 o2 m3 m1 m2.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
unsafeCommaMorphism CommaObject o o m3
xfy (o -> o -> m3 -> CommaObject o o m3
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
xfy) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
x'gy') (Diagram c1 m1 o c2 m3 o
s Diagram c1 m1 o c2 m3 o -> m1 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
i m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ CommaObject o o m3 -> m3
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject o o m3
xfy)) (c -> o -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c m1 o c2 m3 o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c m1 o c2 m3 o
t) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
xfy)) m1
i)
                    where
                        decompH :: [m1]
decompH = c -> m1 -> [m1]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose (Diagram c m1 o c2 m3 o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c m1 o c2 m3 o
t) m1
h [m1] -> [m1] -> [m1]
forall a. [a] -> [a] -> [a]
++ [c -> o -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c m1 o c2 m3 o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c m1 o c2 m3 o
t) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
xfy)]
                        genH :: m1
genH = [m1] -> m1
forall a. HasCallStack => [a] -> a
head [m1]
decompH
                        composeAboveH :: m1
composeAboveH = [m1] -> m1
forall m o. Morphism m o => [m] -> m
compose([m1] -> m1) -> ([m1] -> [m1]) -> [m1] -> m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[m1] -> [m1]
forall a. HasCallStack => [a] -> [a]
tail ([m1] -> m1) -> [m1] -> m1
forall a b. (a -> b) -> a -> b
$ [m1]
decompH
                        resultT :: CommaMorphism o o m1 m1 m3
resultT = CommaObject o o m3
-> CommaObject o o m3 -> m1 -> m1 -> CommaMorphism o o m1 m1 m3
forall o1 o2 m3 m1 m2.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
unsafeCommaMorphism (o -> o -> m3 -> CommaObject o o m3
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject (m1 -> o
forall m o. Morphism m o => m -> o
source m1
genH) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
xfy) ((CommaObject o o m3 -> m3
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject o o m3
x'gy') m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ (Diagram c m1 o c2 m3 o
t Diagram c m1 o c2 m3 o -> m1 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
genH))) CommaObject o o m3
x'gy' m1
genH (c1 -> o -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c1 m1 o c2 m3 o -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o c2 m3 o
s) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
xfy))
                        decompI :: [m1]
decompI = [c1 -> o -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c1 m1 o c2 m3 o -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o c2 m3 o
s) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget CommaObject o o m3
x'gy')] [m1] -> [m1] -> [m1]
forall a. [a] -> [a] -> [a]
++ c1 -> m1 -> [m1]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose (Diagram c1 m1 o c2 m3 o -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o c2 m3 o
s) m1
i
                        genI :: m1
genI = [m1] -> m1
forall a. HasCallStack => [a] -> a
last [m1]
decompI
                        composeBelowI :: m1
composeBelowI = [m1] -> m1
forall m o. Morphism m o => [m] -> m
compose([m1] -> m1) -> ([m1] -> [m1]) -> [m1] -> m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[m1] -> [m1]
forall a. HasCallStack => [a] -> [a]
init ([m1] -> m1) -> [m1] -> m1
forall a b. (a -> b) -> a -> b
$ [m1]
decompI
                        resultI :: CommaMorphism o o m1 m1 m3
resultI = CommaObject o o m3
-> CommaObject o o m3 -> m1 -> m1 -> CommaMorphism o o m1 m1 m3
forall o1 o2 m3 m1 m2.
CommaObject o1 o2 m3
-> CommaObject o1 o2 m3 -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
unsafeCommaMorphism CommaObject o o m3
xfy (o -> o -> m3 -> CommaObject o o m3
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
xfy) (m1 -> o
forall m o. Morphism m o => m -> o
target m1
genI) ((Diagram c1 m1 o c2 m3 o
s Diagram c1 m1 o c2 m3 o -> m1 -> m3
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
genI) m3 -> m3 -> m3
forall m o. Morphism m o => m -> m -> m
@ (CommaObject o o m3 -> m3
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow CommaObject o o m3
xfy))) (c -> o -> m1
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (Diagram c m1 o c2 m3 o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c m1 o c2 m3 o
t) (CommaObject o o m3 -> o
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource CommaObject o o m3
xfy)) m1
genI
                
            
    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, Eq o3) => 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
-> Set (CommaObject o1 o2 m3)
ob CommaCategory{leftDiagram :: 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
leftDiagram = Diagram c1 m1 o1 c3 m3 o3
t, rightDiagram :: 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
rightDiagram = Diagram c2 m2 o2 c3 m3 o3
s} = [CommaObject{indexSource :: o1
indexSource=o1
e,indexTarget :: o2
indexTarget=o2
d,selectedArrow :: m3
selectedArrow=m3
f}| o1
e <- (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set 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 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set 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 -> Set m3
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set 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
t Diagram c1 m1 o1 c3 m3 o3 -> o1 -> o3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
e) (Diagram c2 m2 o2 c3 m3 o3
s Diagram c2 m2 o2 c3 m3 o3 -> o2 -> o3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o2
d)]
        
        
    -- | Construct the slice category of a category /C/ over an object /o/.

    --

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

    sliceCategory :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => c -> o -> Maybe (CommaCategory c m o One One One c m o)
    sliceCategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
c -> o -> Maybe (CommaCategory c m o One One One c m o)
sliceCategory c
c o
o
        | o
o o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c = 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{leftDiagram :: Diagram c m o c m o
leftDiagram=FinCat c m o -> c -> Diagram c m o c m o
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat c m o
forall c m o. FinCat c m o
FinCat c
c, rightDiagram :: Diagram One One One c m o
rightDiagram=c -> o -> Diagram One One One c m o
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject c
c o
o}
        | Bool
otherwise = Maybe (CommaCategory c m o One One One c m o)
forall a. Maybe a
Nothing
        
    -- | Construct the coslice category of a category /C/ under an object /o/.

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

    cosliceCategory :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => c -> o -> Maybe (CommaCategory One One One c m o c m o)
    cosliceCategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
c -> o -> Maybe (CommaCategory One One One c m o c m o)
cosliceCategory c
c o
o 
        | o
o o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c = 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{leftDiagram :: Diagram One One One c m o
leftDiagram=c -> o -> Diagram One One One c m o
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject c
c o
o, rightDiagram :: Diagram c m o c m o
rightDiagram=FinCat c m o -> c -> Diagram c m o c m o
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat c m o
forall c m o. FinCat c m o
FinCat c
c}
        | Bool
otherwise = Maybe (CommaCategory One One One c m o c m o)
forall a. Maybe a
Nothing
        
    -- | Construct the arrow category of a category /C/.

    arrowCategory :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => c -> CommaCategory c m o c m o c m o
    arrowCategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
c -> CommaCategory c m o c m o c m o
arrowCategory c
c = CommaCategory{leftDiagram :: Diagram c m o c m o
leftDiagram=FinCat c m o -> c -> Diagram c m o c m o
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat c m o
forall c m o. FinCat c m o
FinCat c
c, rightDiagram :: Diagram c m o c m o
rightDiagram=FinCat c m o -> c -> Diagram c m o c m o
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat c m o
forall c m o. FinCat c m o
FinCat c
c}