{-| Module  : FiniteCategories
Description : Functions to create usual and arbitrary diagrams.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A diagram is a heterogeneous FinFunctor, it is a shift of perspective : we view the functor not as a morphism of categories but as a selection in a category.
 
By heterogeneous, we mean that the type of the source category may be different from the target category.
 
To convert a `Diagram` into any other kind of functor, see @Diagram.Conversion@.

To enumerate all diagrams between two categories, see the `ob` function of /FunctorCategory/.
-}

module Diagram.Diagram
(
    -- * Diagram typeclass and useful functions

    Diagram(..),
    checkFunctoriality,
    completeMmap,
    composeDiag,
    objectImage,
    -- * Constructors of diagrams

    mkDiagram,
    mkIdentityDiagram,
    mkConstantDiagram,
    mkDiscreteDiagram,
    mkSelect0,
    mkSelect1,
    mkSelect2,
    mkSelect3,
    mkTriangle,
    mkParallel,
    mkV,
    mkHat,
)
where
    import Prelude                          hiding ((@))
    import FiniteCategory.FiniteCategory
    import Cat.FinCat
    import Cat.PartialFinCat
    import UsualCategories.DiscreteCategory
    import UsualCategories.Zero
    import UsualCategories.One
    import qualified UsualCategories.Two   as Two
    import qualified UsualCategories.Three as Three
    import qualified UsualCategories.Parallel as Par
    import qualified UsualCategories.V as V
    import qualified UsualCategories.Hat as Hat
    import Data.List (intercalate, nub)
    import Utils.SetList
    import Utils.AssociationList
    import IO.PrettyPrint
    import IO.Show
    
    -- | A diagram is a heterogeneous FinFunctor /F/, it is a shift of perspective : we view the FinFunctor not as a morphism of categories but as a selection in a category. It must obey the following rules :

    --

    -- prop> F (src f) = src (F f) 

    -- prop> F (tgt f) = tgt (F f)

    -- prop> F (f @ g) = F(f) @ F(g)

    -- prop> F (identity a) = identity (F a)

    --

    -- Unlike /FinFunctor/, a `Diagram` can have a source category and a target category with different types.

    --

    -- Using constructor functions `mkDiagram`, `mkConstantDiagram`, `mkDiscreteDiagram`, `mkSelect0`, `mkSelect1`, `mkSelect2`, `mkSelect3`, `mkTriangle` and `mkParallel` 

    -- is the safe way to instantiate a `Diagram` (FinFunctoriality is checked during construction).

    -- 

    -- Therefore, if you want to construct an arbitrary diagram, use the constructor function `mkDiagram` unless it is too long to check FinFunctoriality in which case

    -- you should use the `Diagram` constructor. It is then your responsability to ensure the FinFunctoriality property is verified.

    data Diagram c1 m1 o1 c2 m2 o2 = Diagram {forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src :: c1 -- ^ The source category of the `Diagram`

                                            , forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt :: c2 -- ^ The target category of the `Diagram`

                                            , forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap :: AssociationList o1 o2 -- ^ The object map

                                            , forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap :: AssociationList m1 m2} -- ^ The morphism map

                                            deriving (Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
(Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool)
-> (Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool)
-> Eq (Diagram c1 m1 o1 c2 m2 o2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
/= :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
$c/= :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
== :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
$c== :: forall c1 m1 o1 c2 m2 o2.
(Eq c1, Eq c2, Eq o1, Eq o2, Eq m1, Eq m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
Eq, Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS
[Diagram c1 m1 o1 c2 m2 o2] -> ShowS
Diagram c1 m1 o1 c2 m2 o2 -> String
(Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS)
-> (Diagram c1 m1 o1 c2 m2 o2 -> String)
-> ([Diagram c1 m1 o1 c2 m2 o2] -> ShowS)
-> Show (Diagram c1 m1 o1 c2 m2 o2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
[Diagram c1 m1 o1 c2 m2 o2] -> ShowS
forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String
showList :: [Diagram c1 m1 o1 c2 m2 o2] -> ShowS
$cshowList :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
[Diagram c1 m1 o1 c2 m2 o2] -> ShowS
show :: Diagram c1 m1 o1 c2 m2 o2 -> String
$cshow :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String
showsPrec :: Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS
$cshowsPrec :: forall c1 m1 o1 c2 m2 o2.
(Show c1, Show c2, Show o1, Show o2, Show m1, Show m2) =>
Int -> Diagram c1 m1 o1 c2 m2 o2 -> ShowS
Show)
    
    -- | Checks wether the properties of a Diagram are respected. Returns True if the diagram is well formed, else False.

    checkFunctoriality :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                           FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                          Diagram c1 m1 o1 c2 m2 o2 -> Bool
    checkFunctoriality :: 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, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Bool
checkFunctoriality 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}
        | Bool -> Bool
not ((Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Bool -> Bool -> Bool
(&&) Bool
True [Bool]
imIdNotId) = Bool
False
        | Bool -> Bool
not ((Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Bool -> Bool -> Bool
(&&) Bool
True [Bool]
errFunct) = Bool
False
        | Bool
otherwise = Bool
True
        where
            imIdNotId :: [Bool]
imIdNotId = [AssociationList m1 m2
fm AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-! (c1 -> o1 -> m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c1
s o1
a) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
== c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c2
t (AssociationList o1 o2
om AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-! o1
a) | o1
a <- c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob c1
s]
            errFunct :: [Bool]
errFunct = [AssociationList m1 m2
fm AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-! (m1
g m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ m1
f) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
== (AssociationList m1 m2
fm AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-! m1
g) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (AssociationList m1 m2
fm AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-! m1
f) | m1
f <- (c1 -> [m1]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c1
s), m1
g <- (c1 -> o1 -> [m1]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arFrom c1
s (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f))]
    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, PrettyPrintable m1, PrettyPrintable o1, Eq m1, Eq o1, PrettyPrintable c1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, PrettyPrintable m2, PrettyPrintable o2, PrettyPrintable c2) =>
              PrettyPrintable (Diagram c1 m1 o1 c2 m2 o2) where
        pprint :: Diagram c1 m1 o1 c2 m2 o2 -> String
pprint 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} = String
"Diagram "String -> ShowS
forall a. [a] -> [a] -> [a]
++c1 -> String
forall a. PrettyPrintable a => a -> String
pprint c1
sString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" -> "String -> ShowS
forall a. [a] -> [a] -> [a]
++c2 -> String
forall a. PrettyPrintable a => a -> String
pprint c2
tString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++AssociationList o1 o2 -> String
forall a. PrettyPrintable a => a -> String
pprint AssociationList o1 o2
omString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++AssociationList m1 m2 -> String
forall a. PrettyPrintable a => a -> String
pprint AssociationList m1 m2
fm
    
    -- | Constructor of an arbitrary `Diagram` that checks functoriality.

    --

    -- Use the `Diagram` constructor if the functoriality check is too slow. It is then your responsability to ensure the functoriality property is verified.

    mkDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                  FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                  c1 -- ^ The source category of the diagram.

               -> c2 -- ^ The target category of the diagram.

               -> AssociationList o1 o2 -- ^ The object map of the diagram.

               -> AssociationList m1 m2 -- ^ The morphism map of the diagram.

               -> Maybe (Diagram c1 m1 o1 c2 m2 o2) -- ^ The constructor returns Nothing if the FinFunctoriality check failed.

    mkDiagram :: 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, Eq m2, Eq o2) =>
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Maybe (Diagram c1 m1 o1 c2 m2 o2)
mkDiagram c1
c1 c2
c2 AssociationList o1 o2
om AssociationList m1 m2
fm = if Diagram c1 m1 o1 c2 m2 o2 -> Bool
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, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Bool
checkFunctoriality Diagram c1 m1 o1 c2 m2 o2
diag then Diagram c1 m1 o1 c2 m2 o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just Diagram c1 m1 o1 c2 m2 o2
diag else Maybe (Diagram c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
        where diag :: Diagram c1 m1 o1 c2 m2 o2
diag = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: c1
src=c1
c1, tgt :: c2
tgt=c2
c2, omap :: AssociationList o1 o2
omap=AssociationList o1 o2
om, mmap :: AssociationList m1 m2
mmap=AssociationList m1 m2
fm}
    
    -- | Completes the function map `mmap` of a diagram so that you do not have to specify images of identites and composite arrows.

    completeMmap :: (GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
                              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
                       c1 -- ^ The source category, it must be a generated category. 

                    -> c2 -- ^ The target category. 

                    -> AssociationList o1 o2 -- ^ The omap. 

                    -> AssociationList m1 m2 -- ^ The mmap to complete. 

                    -> AssociationList m1 m2 -- ^ The completed mmap.

    completeMmap :: forall c1 m1 o1 c2 m2 o2.
(GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> AssociationList m1 m2
completeMmap c1
c1 c2
c2 AssociationList o1 o2
om AssociationList m1 m2
fm = AssociationList m1 m2 -> AssociationList m1 m2
forall a. Eq a => [a] -> [a]
nub AssociationList m1 m2
fm2
        where
            fm1 :: AssociationList m1 m2
fm1 = [(c1 -> o1 -> m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c1
c1 o1
o, c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c2
c2 (AssociationList o1 o2
om AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-! o1
o)) | o1
o <- c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob c1
c1]AssociationList m1 m2
-> AssociationList m1 m2 -> AssociationList m1 m2
forall a. [a] -> [a] -> [a]
++AssociationList m1 m2
fm
            fm2 :: AssociationList m1 m2
fm2 = [(m1
a,[m2] -> m2
forall m o. Morphism m o => [m] -> m
compose ([m2] -> m2) -> [m2] -> m2
forall a b. (a -> b) -> a -> b
$ (AssociationList m1 m2
fm1 AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-!) (m1 -> m2) -> [m1] -> [m2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c1 -> m1 -> [m1]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose c1
c1 m1
a) | m1
a <- c1 -> [m1]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c1
c1]AssociationList m1 m2
-> AssociationList m1 m2 -> AssociationList m1 m2
forall a. [a] -> [a] -> [a]
++AssociationList m1 m2
fm1
            
    -- | Compose two diagrams.

    composeDiag :: (FiniteCategory c1 m1 o1, Morphism m1 o1
           ,FiniteCategory c2 m2 o2, Morphism m2 o2
           ,FiniteCategory c3 m3 o3, Morphism m3 o3
           ,Eq m1, Eq o1, Eq m2, Eq o2) => 
           Diagram c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
    Diagram c2 m2 o2 c3 m3 o3
diag2 composeDiag :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m1,
 Eq o1, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
`composeDiag` Diagram c1 m1 o1 c2 m2 o2
diag1 = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: c1
src=(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
diag1), tgt :: c3
tgt=(Diagram c2 m2 o2 c3 m3 o3 -> c3
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c3 m3 o3
diag2), omap :: AssociationList o1 o3
omap=((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
diag2)AssociationList o2 o3
-> AssociationList o1 o2 -> AssociationList o1 o3
forall a b c.
(Eq a, Eq b) =>
AssociationList b c -> AssociationList a b -> AssociationList a c
!-.(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
diag1)), mmap :: AssociationList m1 m3
mmap=((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
diag2)AssociationList m2 m3
-> AssociationList m1 m2 -> AssociationList m1 m3
forall a b c.
(Eq a, Eq b) =>
AssociationList b c -> AssociationList a b -> AssociationList a c
!-.(Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c1 m1 o1 c2 m2 o2
diag1))} 
    
    -- | Returns the objects image of the diagram.

    objectImage :: (FiniteCategory c1 m1 o1, Morphism m1 o1
                   ,FiniteCategory c2 m2 o2, Morphism m2 o2) =>
                    Diagram c1 m1 o1 c2 m2 o2 -> [o2]
    objectImage :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> [o2]
objectImage Diagram c1 m1 o1 c2 m2 o2
diag = (o1, o2) -> o2
forall a b. (a, b) -> b
snd ((o1, o2) -> o2) -> [(o1, o2)] -> [o2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram c1 m1 o1 c2 m2 o2 -> [(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
diag)
    
    -- | Constructs a diagram which maps a category to itself to that each object is mapped to itself and each morphism is mapped to itself too.

    mkIdentityDiagram :: (FiniteCategory c m o, Morphism m o) => c -> (Diagram c m o c m o)
    mkIdentityDiagram :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Diagram c m o c m o
mkIdentityDiagram c
c = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: c
src=c
c, tgt :: c
tgt=c
c, omap :: AssociationList o o
omap=(o -> o) -> [o] -> AssociationList o o
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList o -> o
forall a. a -> a
id (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c),mmap :: AssociationList m m
mmap=(m -> m) -> [m] -> AssociationList m m
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList m -> m
forall a. a -> a
id (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
c)}
    
    -- | Constructs a diagram where every object is mapped to a single object and every morphism is mapped to the identity of this single object.

    mkConstantDiagram :: (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 :: 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 c1
c1 c2
c2 o2
o2
        | o2 -> [o2] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o2
o2 (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob c2
c2) = Diagram c1 m1 o1 c2 m2 o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: c1
src=c1
c1, tgt :: c2
tgt=c2
c2, omap :: AssociationList o1 o2
omap=(o1 -> o2) -> [o1] -> AssociationList o1 o2
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList (\o1
x -> o2
o2) (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob c1
c1),mmap :: AssociationList m1 m2
mmap=(m1 -> m2) -> [m1] -> AssociationList m1 m2
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList (\m1
x -> (c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c2
c2 o2
o2)) (c1 -> [m1]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c1
c1)}
        | Bool
otherwise = Maybe (Diagram c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
    
    -- | Constructs a diagram that selects a list of objects of a category.

    mkDiscreteDiagram :: (FiniteCategory c m o, Morphism m o, Eq o) =>
                          c -> [o] -> Maybe (Diagram (DiscreteCategory o) (DiscreteIdentity o) (DiscreteObject o) c m o)
    mkDiscreteDiagram :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c
-> [o]
-> Maybe
     (Diagram
        (DiscreteCategory o) (DiscreteIdentity o) (DiscreteObject o) c m o)
mkDiscreteDiagram c
c [o]
objs
        | [o]
objs [o] -> [o] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isIncludedIn` (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) = Diagram
  (DiscreteCategory o) (DiscreteIdentity o) (DiscreteObject o) c m o
-> Maybe
     (Diagram
        (DiscreteCategory o) (DiscreteIdentity o) (DiscreteObject o) c m o)
forall a. a -> Maybe a
Just Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: DiscreteCategory o
src=[o] -> DiscreteCategory o
forall a. [a] -> DiscreteCategory a
DiscreteCategory [o]
objs, tgt :: c
tgt=c
c, omap :: AssociationList (DiscreteObject o) o
omap=(DiscreteObject o -> o)
-> [DiscreteObject o] -> AssociationList (DiscreteObject o) o
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList (\(DiscreteObject o
o) -> o
o) (DiscreteCategory o -> [DiscreteObject o]
forall c m o. FiniteCategory c m o => c -> [o]
ob ([o] -> DiscreteCategory o
forall a. [a] -> DiscreteCategory a
DiscreteCategory [o]
objs)),mmap :: AssociationList (DiscreteIdentity o) m
mmap=(DiscreteIdentity o -> m)
-> [DiscreteIdentity o] -> AssociationList (DiscreteIdentity o) m
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList (\(DiscreteIdentity o
o) -> (c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c o
o)) (DiscreteCategory o -> [DiscreteIdentity o]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows ([o] -> DiscreteCategory o
forall a. [a] -> DiscreteCategory a
DiscreteCategory [o]
objs))}
        | Bool
otherwise = Maybe
  (Diagram
     (DiscreteCategory o) (DiscreteIdentity o) (DiscreteObject o) c m o)
forall a. Maybe a
Nothing
    
    -- | Constructs a diagram that selects no object and no morphism.

    mkSelect0 :: (FiniteCategory c m o, Morphism m o) => c -> Diagram Zero Zero Zero c m o
    mkSelect0 :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Diagram Zero Zero Zero c m o
mkSelect0 c
c = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: Zero
src=Zero
Zero, tgt :: c
tgt=c
c, omap :: AssociationList Zero o
omap=[],mmap :: AssociationList Zero m
mmap=[]}
    
    -- | Constructs a diagram that selects a single object and its identity.

    mkSelect1 :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (Diagram One One One c m o)
    mkSelect1 :: 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
        | o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o
o (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) = Diagram One One One c m o -> Maybe (Diagram One One One c m o)
forall a. a -> Maybe a
Just Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: One
src=One
One, tgt :: c
tgt=c
c, omap :: AssociationList One o
omap=[(One
One,o
o)],mmap :: AssociationList One m
mmap=[(One
One,(c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c o
o))]}
        | Bool
otherwise = Maybe (Diagram One One One c m o)
forall a. Maybe a
Nothing
    
    -- | Constructs a diagram that selects a single arrow.

    mkSelect2 :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Maybe (Diagram Two.Two Two.TwoAr Two.TwoOb c m o)
    mkSelect2 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Maybe (Diagram Two TwoAr TwoOb c m o)
mkSelect2 c
c m
m 
        | Bool
condition = Diagram Two TwoAr TwoOb c m o
-> Maybe (Diagram Two TwoAr TwoOb c m o)
forall a. a -> Maybe a
Just Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: Two
src=Two
Two.Two, tgt :: c
tgt=c
c, omap :: AssociationList TwoOb o
omap=AssociationList TwoOb o
om,mmap :: AssociationList TwoAr m
mmap=(Two
-> c
-> AssociationList TwoOb o
-> AssociationList TwoAr m
-> AssociationList TwoAr m
forall c1 m1 o1 c2 m2 o2.
(GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> AssociationList m1 m2
completeMmap Two
Two.Two c
c AssociationList TwoOb o
om [(TwoAr
Two.F,m
m)])}
        | Bool
otherwise = Maybe (Diagram Two TwoAr TwoOb c m o)
forall a. Maybe a
Nothing
        where
            condition :: Bool
condition = o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
source m
m) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) Bool -> Bool -> Bool
&& o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
target m
m) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) Bool -> Bool -> Bool
&& m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
m (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
m) (m -> o
forall m o. Morphism m o => m -> o
target m
m))
            om :: AssociationList TwoOb o
om = [(TwoOb
Two.A,m -> o
forall m o. Morphism m o => m -> o
source m
m),(TwoOb
Two.B,m -> o
forall m o. Morphism m o => m -> o
target m
m)]
            
    -- | Constructs a diagram that selects a triangle.

    --

    -- > B <-f- A

    -- > |     /

    -- > g   g\@f

    -- > |  /

    -- > v v 

    -- > C

    mkSelect3 :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -- ^ The target category.

                                                                  -> m -- ^ /f/

                                                                  -> m -- ^ /g/

                                                                  -> Maybe (Diagram Three.Three Three.ThreeAr Three.ThreeOb c m o)
    mkSelect3 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o, Eq m) =>
c -> m -> m -> Maybe (Diagram Three ThreeAr ThreeOb c m o)
mkSelect3 c
c m
f m
g
        | Bool
condition = Diagram Three ThreeAr ThreeOb c m o
-> Maybe (Diagram Three ThreeAr ThreeOb c m o)
forall a. a -> Maybe a
Just Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: Three
src=Three
Three.Three, tgt :: c
tgt=c
c, omap :: AssociationList ThreeOb o
omap=AssociationList ThreeOb o
om,mmap :: AssociationList ThreeAr m
mmap=(Three
-> c
-> AssociationList ThreeOb o
-> AssociationList ThreeAr m
-> AssociationList ThreeAr m
forall c1 m1 o1 c2 m2 o2.
(GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> AssociationList m1 m2
completeMmap Three
Three.Three c
c AssociationList ThreeOb o
om [(ThreeAr
Three.F,m
f),(ThreeAr
Three.G,m
g)])}
        | Bool
otherwise = Maybe (Diagram Three ThreeAr ThreeOb c m o)
forall a. Maybe a
Nothing
        where
            condition :: Bool
condition = Bool
obInCat Bool -> Bool -> Bool
&& Bool
arInCat Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
source m
g) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== (m -> o
forall m o. Morphism m o => m -> o
target m
f)
            obInCat :: Bool
obInCat =  o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
source m
f) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) Bool -> Bool -> Bool
&& o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
target m
f) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) Bool -> Bool -> Bool
&& o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
target m
g) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c)
            arInCat :: Bool
arInCat = m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
f (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) (m -> o
forall m o. Morphism m o => m -> o
target m
f)) Bool -> Bool -> Bool
&& m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
g (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
g) (m -> o
forall m o. Morphism m o => m -> o
target m
g))
            om :: AssociationList ThreeOb o
om = [(ThreeOb
Three.A,m -> o
forall m o. Morphism m o => m -> o
source m
f),(ThreeOb
Three.B,m -> o
forall m o. Morphism m o => m -> o
target m
f),(ThreeOb
Three.C,m -> o
forall m o. Morphism m o => m -> o
target m
g)]
            
    -- | Constructs a diagram that selects a triangle. (Alias for `mkSelect3`).

    mkTriangle :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Three.Three Three.ThreeAr Three.ThreeOb c m o)
    mkTriangle :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o, Eq m) =>
c -> m -> m -> Maybe (Diagram Three ThreeAr ThreeOb c m o)
mkTriangle = c -> m -> m -> Maybe (Diagram Three ThreeAr ThreeOb c m o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o, Eq m) =>
c -> m -> m -> Maybe (Diagram Three ThreeAr ThreeOb c m o)
mkSelect3
    
    -- | Constructs a diagram that selects two parallel arrows.

    mkParallel :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Par.Parallel Par.ParallelAr Par.ParallelOb c m o)
    mkParallel :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o, Eq m) =>
c -> m -> m -> Maybe (Diagram Parallel ParallelAr ParallelOb c m o)
mkParallel c
c m
f m
g
        | Bool
condition = Diagram Parallel ParallelAr ParallelOb c m o
-> Maybe (Diagram Parallel ParallelAr ParallelOb c m o)
forall a. a -> Maybe a
Just Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: Parallel
src=Parallel
Par.Parallel, tgt :: c
tgt=c
c, omap :: AssociationList ParallelOb o
omap=AssociationList ParallelOb o
om,mmap :: AssociationList ParallelAr m
mmap=(Parallel
-> c
-> AssociationList ParallelOb o
-> AssociationList ParallelAr m
-> AssociationList ParallelAr m
forall c1 m1 o1 c2 m2 o2.
(GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> AssociationList m1 m2
completeMmap Parallel
Par.Parallel c
c AssociationList ParallelOb o
om [(ParallelAr
Par.F,m
f),(ParallelAr
Par.G,m
g)])}
        | Bool
otherwise = Maybe (Diagram Parallel ParallelAr ParallelOb c m o)
forall a. Maybe a
Nothing
        where
            condition :: Bool
condition = Bool
obInCat Bool -> Bool -> Bool
&& Bool
arInCat Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
source m
f) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== (m -> o
forall m o. Morphism m o => m -> o
source m
g) Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
target m
f) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== (m -> o
forall m o. Morphism m o => m -> o
target m
g)
            obInCat :: Bool
obInCat =  o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
source m
f) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) Bool -> Bool -> Bool
&& o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
target m
f) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c)
            arInCat :: Bool
arInCat = m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
f (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) (m -> o
forall m o. Morphism m o => m -> o
target m
f)) Bool -> Bool -> Bool
&& m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
g (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
g) (m -> o
forall m o. Morphism m o => m -> o
target m
g))
            om :: AssociationList ParallelOb o
om = [(ParallelOb
Par.A,m -> o
forall m o. Morphism m o => m -> o
source m
f), (ParallelOb
Par.B, m -> o
forall m o. Morphism m o => m -> o
target m
f)]
           
    -- | Constructs a diagram that selects a V.

    mkV :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram V.V V.VAr V.VOb c m o)
    mkV :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o, Eq m) =>
c -> m -> m -> Maybe (Diagram V VAr VOb c m o)
mkV c
c m
f m
g
        | Bool
condition = Diagram V VAr VOb c m o -> Maybe (Diagram V VAr VOb c m o)
forall a. a -> Maybe a
Just Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: V
src=V
V.V, tgt :: c
tgt=c
c, omap :: AssociationList VOb o
omap=AssociationList VOb o
om,mmap :: AssociationList VAr m
mmap=(V
-> c
-> AssociationList VOb o
-> AssociationList VAr m
-> AssociationList VAr m
forall c1 m1 o1 c2 m2 o2.
(GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> AssociationList m1 m2
completeMmap V
V.V c
c AssociationList VOb o
om [(VAr
V.F,m
f),(VAr
V.G,m
g)])}
        | Bool
otherwise = Maybe (Diagram V VAr VOb c m o)
forall a. Maybe a
Nothing
        where
            condition :: Bool
condition = Bool
obInCat Bool -> Bool -> Bool
&& Bool
arInCat Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
target m
f) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== (m -> o
forall m o. Morphism m o => m -> o
target m
g)
            obInCat :: Bool
obInCat =  o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
source m
f) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) Bool -> Bool -> Bool
&& o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
target m
f) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c)
            arInCat :: Bool
arInCat = m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
f (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) (m -> o
forall m o. Morphism m o => m -> o
target m
f)) Bool -> Bool -> Bool
&& m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
g (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
g) (m -> o
forall m o. Morphism m o => m -> o
target m
g))
            om :: AssociationList VOb o
om = [(VOb
V.A,m -> o
forall m o. Morphism m o => m -> o
source m
f), (VOb
V.B, m -> o
forall m o. Morphism m o => m -> o
source m
g), (VOb
V.C, m -> o
forall m o. Morphism m o => m -> o
target m
g)]
            
    -- | Constructs a diagram that selects a Hat.

    mkHat :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Hat.Hat Hat.HatAr Hat.HatOb c m o)
    mkHat :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o, Eq m) =>
c -> m -> m -> Maybe (Diagram Hat HatAr HatOb c m o)
mkHat c
c m
f m
g
        | Bool
condition = Diagram Hat HatAr HatOb c m o
-> Maybe (Diagram Hat HatAr HatOb c m o)
forall a. a -> Maybe a
Just Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: Hat
src=Hat
Hat.Hat, tgt :: c
tgt=c
c, omap :: AssociationList HatOb o
omap=AssociationList HatOb o
om,mmap :: AssociationList HatAr m
mmap=(Hat
-> c
-> AssociationList HatOb o
-> AssociationList HatAr m
-> AssociationList HatAr m
forall c1 m1 o1 c2 m2 o2.
(GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> AssociationList m1 m2
completeMmap Hat
Hat.Hat c
c AssociationList HatOb o
om [(HatAr
Hat.F,m
f),(HatAr
Hat.G,m
g)])}
        | Bool
otherwise = Maybe (Diagram Hat HatAr HatOb c m o)
forall a. Maybe a
Nothing
        where
            condition :: Bool
condition = Bool
obInCat Bool -> Bool -> Bool
&& Bool
arInCat Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
source m
f) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== (m -> o
forall m o. Morphism m o => m -> o
source m
g)
            obInCat :: Bool
obInCat =  o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
source m
f) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c) Bool -> Bool -> Bool
&& o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m -> o
forall m o. Morphism m o => m -> o
target m
f) (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
c)
            arInCat :: Bool
arInCat = m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
f (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) (m -> o
forall m o. Morphism m o => m -> o
target m
f)) Bool -> Bool -> Bool
&& m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
g (c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c (m -> o
forall m o. Morphism m o => m -> o
source m
g) (m -> o
forall m o. Morphism m o => m -> o
target m
g))
            om :: AssociationList HatOb o
om = [(HatOb
Hat.A,m -> o
forall m o. Morphism m o => m -> o
source m
f), (HatOb
Hat.B, m -> o
forall m o. Morphism m o => m -> o
target m
f), (HatOb
Hat.C, m -> o
forall m o. Morphism m o => m -> o
target m
g)]