{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : __PartialFinCat__ is the category of finite categories, partial functors are the morphisms of __FinCat__.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __PartialFinCat__ category has as objects finite categories and as morphisms partial functors between them.

A partial functor is a functor where the object map and the morphism map can be partial functions.

It is itself a large category (therefore not a finite one),
we only construct finite full subcategories of the mathematical infinite __PartialFinCat__ category.
`PartialFinCat` is the type of full finite subcategories of __PartialFinCat__.

To instantiate it, use the `PartialFinCat` constructor on a list of categories.

To convert a `PartialFunctor` into any other kind of functor, see @Diagram.Conversion@.

For example, see @ExampleCat.ExamplePartialFinCat@.
-}

module Cat.PartialFinCat
(
    PartialFunctor(..),
    PartialFinCat(..),
    domainObjects,
    domainArrows,
    codomainObjects,
    codomainArrows,
    objectsNotMapped,
    arrowsNotMapped,
    objectsNotMappedTo,
    arrowsNotMappedTo
)
where
    import FiniteCategory.FiniteCategory
    import Cat.FinCat
    import Utils.EnumerateMaps
    import Utils.CartesianProduct
    import Utils.AssociationList
    import IO.PrettyPrint
    import IO.Show
    import Utils.SetList
    import Data.List ((\\), nub)
    
    -- | A `PartialFunctor` /F/ between two categories is a partial map between objects and a partial map between arrows of the two categories such that :

    --

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

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

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

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

    --

    -- It is meant to be a morphism between categories within `PartialFinCat`, it is homogeneous, the type of the source category must be the same as the type of the target category.

    --

    -- To convert a `PartialFunctor` into any other kind of functor, see @Diagram.Conversion@.

    data PartialFunctor c m o = PartialFunctor {forall c m o. PartialFunctor c m o -> c
srcPF :: c, forall c m o. PartialFunctor c m o -> c
tgtPF :: c, forall c m o. PartialFunctor c m o -> AssociationList o o
omapPF :: AssociationList o o, forall c m o. PartialFunctor c m o -> AssociationList m m
mmapPF :: AssociationList m m} deriving (PartialFunctor c m o -> PartialFunctor c m o -> Bool
(PartialFunctor c m o -> PartialFunctor c m o -> Bool)
-> (PartialFunctor c m o -> PartialFunctor c m o -> Bool)
-> Eq (PartialFunctor c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq c, Eq o, Eq m) =>
PartialFunctor c m o -> PartialFunctor c m o -> Bool
/= :: PartialFunctor c m o -> PartialFunctor c m o -> Bool
$c/= :: forall c m o.
(Eq c, Eq o, Eq m) =>
PartialFunctor c m o -> PartialFunctor c m o -> Bool
== :: PartialFunctor c m o -> PartialFunctor c m o -> Bool
$c== :: forall c m o.
(Eq c, Eq o, Eq m) =>
PartialFunctor c m o -> PartialFunctor c m o -> Bool
Eq, Int -> PartialFunctor c m o -> ShowS
[PartialFunctor c m o] -> ShowS
PartialFunctor c m o -> String
(Int -> PartialFunctor c m o -> ShowS)
-> (PartialFunctor c m o -> String)
-> ([PartialFunctor c m o] -> ShowS)
-> Show (PartialFunctor c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show c, Show o, Show m) =>
Int -> PartialFunctor c m o -> ShowS
forall c m o.
(Show c, Show o, Show m) =>
[PartialFunctor c m o] -> ShowS
forall c m o.
(Show c, Show o, Show m) =>
PartialFunctor c m o -> String
showList :: [PartialFunctor c m o] -> ShowS
$cshowList :: forall c m o.
(Show c, Show o, Show m) =>
[PartialFunctor c m o] -> ShowS
show :: PartialFunctor c m o -> String
$cshow :: forall c m o.
(Show c, Show o, Show m) =>
PartialFunctor c m o -> String
showsPrec :: Int -> PartialFunctor c m o -> ShowS
$cshowsPrec :: forall c m o.
(Show c, Show o, Show m) =>
Int -> PartialFunctor c m o -> ShowS
Show)
    
    instance (Eq c, Eq m, Eq o) => Morphism (PartialFunctor c m o) c where
        @ :: PartialFunctor c m o
-> PartialFunctor c m o -> PartialFunctor c m o
(@) PartialFunctor{srcPF :: forall c m o. PartialFunctor c m o -> c
srcPF=c
s2,tgtPF :: forall c m o. PartialFunctor c m o -> c
tgtPF=c
t2,omapPF :: forall c m o. PartialFunctor c m o -> AssociationList o o
omapPF=AssociationList o o
om2,mmapPF :: forall c m o. PartialFunctor c m o -> AssociationList m m
mmapPF=AssociationList m m
fm2} PartialFunctor{srcPF :: forall c m o. PartialFunctor c m o -> c
srcPF=c
s1,tgtPF :: forall c m o. PartialFunctor c m o -> c
tgtPF=c
t1,omapPF :: forall c m o. PartialFunctor c m o -> AssociationList o o
omapPF=AssociationList o o
om1,mmapPF :: forall c m o. PartialFunctor c m o -> AssociationList m m
mmapPF=AssociationList m m
fm1}
            | c
t1 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
/= c
s2 = String -> PartialFunctor c m o
forall a. HasCallStack => String -> a
error String
"Illegal composition of PartialFunctors."
            | Bool
otherwise = PartialFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> PartialFunctor c m o
PartialFunctor{srcPF :: c
srcPF=c
s1,tgtPF :: c
tgtPF=c
t2,omapPF :: AssociationList o o
omapPF=AssociationList o o
om2 AssociationList o o -> AssociationList o o -> AssociationList o o
forall a b c.
(Eq a, Eq b) =>
AssociationList b c -> AssociationList a b -> AssociationList a c
!-. AssociationList o o
om1,mmapPF :: AssociationList m m
mmapPF=AssociationList m m
fm2 AssociationList m m -> AssociationList m m -> AssociationList m m
forall a b c.
(Eq a, Eq b) =>
AssociationList b c -> AssociationList a b -> AssociationList a c
!-. AssociationList m m
fm1}
        source :: PartialFunctor c m o -> c
source = PartialFunctor c m o -> c
forall c m o. PartialFunctor c m o -> c
srcPF
        target :: PartialFunctor c m o -> c
target = PartialFunctor c m o -> c
forall c m o. PartialFunctor c m o -> c
tgtPF
            
    instance (FiniteCategory c m o, Morphism m o, PrettyPrintable c, PrettyPrintable m, PrettyPrintable o, Eq m, Eq o) =>
              PrettyPrintable (PartialFunctor c m o) where
        pprint :: PartialFunctor c m o -> String
pprint PartialFunctor{srcPF :: forall c m o. PartialFunctor c m o -> c
srcPF=c
s,tgtPF :: forall c m o. PartialFunctor c m o -> c
tgtPF=c
t,omapPF :: forall c m o. PartialFunctor c m o -> AssociationList o o
omapPF=AssociationList o o
om,mmapPF :: forall c m o. PartialFunctor c m o -> AssociationList m m
mmapPF=AssociationList m m
fm} = String
"PartialFunctor ("String -> ShowS
forall a. [a] -> [a] -> [a]
++c -> String
forall a. PrettyPrintable a => a -> String
pprint c
sString -> ShowS
forall a. [a] -> [a] -> [a]
++String
") -> ("String -> ShowS
forall a. [a] -> [a] -> [a]
++c -> String
forall a. PrettyPrintable a => a -> String
pprint c
tString -> ShowS
forall a. [a] -> [a] -> [a]
++String
")\n\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++AssociationList o o -> String
forall a. PrettyPrintable a => a -> String
pprint AssociationList o o
omString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"\n\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++AssociationList m m -> String
forall a. PrettyPrintable a => a -> String
pprint AssociationList m m
fm
        
    -- -- | Checks wether the properties of a functor are respected.

    checkPartialFunctoriality :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => PartialFunctor c m o -> Bool
    checkPartialFunctoriality :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
PartialFunctor c m o -> Bool
checkPartialFunctoriality PartialFunctor {srcPF :: forall c m o. PartialFunctor c m o -> c
srcPF=c
s,tgtPF :: forall c m o. PartialFunctor c m o -> c
tgtPF=c
t,omapPF :: forall c m o. PartialFunctor c m o -> AssociationList o o
omapPF=AssociationList o o
om,mmapPF :: forall c m o. PartialFunctor c m o -> AssociationList m m
mmapPF=AssociationList m m
fm}
        | Bool -> Bool
not ((AssociationList o o -> [o]
forall a b. AssociationList a b -> [a]
keys AssociationList o o
om) [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
s)) = Bool
False
        | Bool -> Bool
not ((AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm) [m] -> [m] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isIncludedIn` (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
s)) = Bool
False
        | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
imSrcExists) = Bool
False
        | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
imTgtExists) = Bool
False
        | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
idMapped) = Bool
False
        | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
imIdNotId) = Bool
False
        | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
compNotMapped) = Bool
False
        | Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
errFunct) = Bool
False
        | Bool
otherwise = Bool
True
        where
            imSrcExists :: [Bool]
imSrcExists = [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) (AssociationList o o -> [o]
forall a b. AssociationList a b -> [a]
keys AssociationList o o
om) | m
f <- AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm]
            imTgtExists :: [Bool]
imTgtExists = [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) (AssociationList o o -> [o]
forall a b. AssociationList a b -> [a]
keys AssociationList o o
om) | m
f <- AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm]
            idMapped :: [Bool]
idMapped = [m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
s o
o) (AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm) | o
o <- AssociationList o o -> [o]
forall a b. AssociationList a b -> [a]
keys AssociationList o o
om]
            imIdNotId :: [Bool]
imIdNotId = [AssociationList m m
fm AssociationList m m -> m -> m
forall a b. Eq a => AssociationList a b -> a -> b
!-! (c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
s o
a) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
t (AssociationList o o
om AssociationList o o -> o -> o
forall a b. Eq a => AssociationList a b -> a -> b
!-! o
a) | o
a <- AssociationList o o -> [o]
forall a b. AssociationList a b -> [a]
keys AssociationList o o
om]
            compNotMapped :: [Bool]
compNotMapped = [m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (m
g m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f) (AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm) | m
f <- (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
s), m
g <- (c -> o -> [m]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arFrom c
s (m -> o
forall m o. Morphism m o => m -> o
target m
f)), m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
f (AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm), m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
g (AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm)]
            errFunct :: [Bool]
errFunct = [AssociationList m m
fm AssociationList m m -> m -> m
forall a b. Eq a => AssociationList a b -> a -> b
!-! (m
g m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== (AssociationList m m
fm AssociationList m m -> m -> m
forall a b. Eq a => AssociationList a b -> a -> b
!-! m
g) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (AssociationList m m
fm AssociationList m m -> m -> m
forall a b. Eq a => AssociationList a b -> a -> b
!-! m
f) | m
f <- (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
s), m
g <- (c -> o -> [m]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> [m]
arFrom c
s (m -> o
forall m o. Morphism m o => m -> o
target m
f)), m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
f (AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm), m -> [m] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem m
g (AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm)]
      
    -- | An instance of `PartialFinCat` is a list of categories of interest.

    --

    -- Listing all arrows between two objects (i.e. listing PartialFunctors between two categories) is slow (there are a lot of candidates).

    newtype PartialFinCat c m o = PartialFinCat [c]
    
    -- We are forced to use the language extension FlexibleInstances because of this instance declaration :

    -- The category 'c' could be itself a `FinCat` category therefore not respecting the uniqueness rule of instanciation.

    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (PartialFinCat c m o) (PartialFunctor c m o) c where
        ob :: PartialFinCat c m o -> [c]
ob (PartialFinCat [c]
xs) = [c]
xs
        identity :: Morphism (PartialFunctor c m o) c =>
PartialFinCat c m o -> c -> PartialFunctor c m o
identity (PartialFinCat [c]
xs) c
catObj
            | c -> [c] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem c
catObj [c]
xs = PartialFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> PartialFunctor c m o
PartialFunctor {srcPF :: c
srcPF=c
catObj,tgtPF :: c
tgtPF=c
catObj,omapPF :: AssociationList o o
omapPF=[o] -> AssociationList o o
forall a. [a] -> AssociationList a a
mkAssocListIdentity (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
catObj),mmapPF :: AssociationList m m
mmapPF=[m] -> AssociationList m m
forall a. [a] -> AssociationList a a
mkAssocListIdentity (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
catObj)}
            | Bool
otherwise = String -> PartialFunctor c m o
forall a. HasCallStack => String -> a
error String
"Category not in PartialFinCat"
        ar :: Morphism (PartialFunctor c m o) c =>
PartialFinCat c m o -> c -> c -> [PartialFunctor c m o]
ar (PartialFinCat [c]
xs) c
cat1 c
cat2
            | c -> [c] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem c
cat1 [c]
xs Bool -> Bool -> Bool
&& c -> [c] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem c
cat2 [c]
xs = [PartialFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> PartialFunctor c m o
PartialFunctor{srcPF :: c
srcPF=c
cat1,tgtPF :: c
tgtPF=c
cat2,mmapPF :: AssociationList m m
mmapPF=AssociationList m m
appF, omapPF :: AssociationList o o
omapPF=AssociationList o o
appO} | AssociationList o o
appO <- [AssociationList o o]
appObj, AssociationList m m
appF <- [AssociationList m m]
appMorph, PartialFunctor c m o -> Bool
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
PartialFunctor c m o -> Bool
checkPartialFunctoriality PartialFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> PartialFunctor c m o
PartialFunctor{srcPF :: c
srcPF=c
cat1,tgtPF :: c
tgtPF=c
cat2,mmapPF :: AssociationList m m
mmapPF=AssociationList m m
appF, omapPF :: AssociationList o o
omapPF=AssociationList o o
appO}]
            | Bool
otherwise = String -> [PartialFunctor c m o]
forall a. HasCallStack => String -> a
error String
"Category not in PartialFinCat"
            where
                appObj :: [AssociationList o o]
appObj = [[AssociationList o o]] -> [AssociationList o o]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[AssociationList o o]] -> [AssociationList o o])
-> [[AssociationList o o]] -> [AssociationList o o]
forall a b. (a -> b) -> a -> b
$ (\[o]
x -> [o] -> [o] -> [AssociationList o o]
forall a b. [a] -> [b] -> [AssociationList a b]
enumAssocLists [o]
x (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat2)) ([o] -> [AssociationList o o]) -> [[o]] -> [[AssociationList o o]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([o] -> [[o]]
forall a. Eq a => [a] -> [[a]]
powerList (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat1))
                appMorph :: [AssociationList m m]
appMorph = [[AssociationList m m]] -> [AssociationList m m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[AssociationList m m]] -> [AssociationList m m])
-> [[AssociationList m m]] -> [AssociationList m m]
forall a b. (a -> b) -> a -> b
$ (\[m]
x -> [m] -> [m] -> [AssociationList m m]
forall a b. [a] -> [b] -> [AssociationList a b]
enumAssocLists [m]
x (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
cat2)) ([m] -> [AssociationList m m]) -> [[m]] -> [[AssociationList m m]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([m] -> [[m]]
forall a. Eq a => [a] -> [[a]]
powerList (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
cat1))
                    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => GeneratedFiniteCategory (PartialFinCat c m o) (PartialFunctor c m o) c where
        genAr :: Morphism (PartialFunctor c m o) c =>
PartialFinCat c m o -> c -> c -> [PartialFunctor c m o]
genAr = PartialFinCat c m o -> c -> c -> [PartialFunctor c m o]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
defaultGenAr
        decompose :: Morphism (PartialFunctor c m o) c =>
PartialFinCat c m o
-> PartialFunctor c m o -> [PartialFunctor c m o]
decompose = PartialFinCat c m o
-> PartialFunctor c m o -> [PartialFunctor c m o]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
defaultDecompose
    
    -- | Returns the objects mapped by a partial functor.

    domainObjects :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [o]
    domainObjects :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [o]
domainObjects PartialFunctor c m o
funct = AssociationList o o -> [o]
forall a b. AssociationList a b -> [a]
keys (PartialFunctor c m o -> AssociationList o o
forall c m o. PartialFunctor c m o -> AssociationList o o
omapPF PartialFunctor c m o
funct)
    
    -- | Returns the objects not mapped by a partial functor.

    objectsNotMapped :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [o]
    objectsNotMapped :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [o]
objectsNotMapped PartialFunctor c m o
funct = (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob (PartialFunctor c m o -> c
forall m o. Morphism m o => m -> o
source PartialFunctor c m o
funct))[o] -> [o] -> [o]
forall a. Eq a => [a] -> [a] -> [a]
\\(PartialFunctor c m o -> [o]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [o]
domainObjects PartialFunctor c m o
funct)
    
    -- | Returns the arrows mapped by a partial functor.

    domainArrows :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [m]
    domainArrows :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [m]
domainArrows PartialFunctor c m o
funct = AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys (PartialFunctor c m o -> AssociationList m m
forall c m o. PartialFunctor c m o -> AssociationList m m
mmapPF PartialFunctor c m o
funct)
    
    -- | Returns the arrows not mapped by a partial functor.

    arrowsNotMapped :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [m]
    arrowsNotMapped :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [m]
arrowsNotMapped PartialFunctor c m o
funct = (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows (PartialFunctor c m o -> c
forall m o. Morphism m o => m -> o
source PartialFunctor c m o
funct))[m] -> [m] -> [m]
forall a. Eq a => [a] -> [a] -> [a]
\\(PartialFunctor c m o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [m]
domainArrows PartialFunctor c m o
funct)

    -- | Returns the objects mapped onto by a partial functor.

    codomainObjects :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [o]
    codomainObjects :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [o]
codomainObjects PartialFunctor c m o
funct = [o] -> [o]
forall a. Eq a => [a] -> [a]
nub ([o] -> [o]) -> [o] -> [o]
forall a b. (a -> b) -> a -> b
$ AssociationList o o -> [o]
forall a b. AssociationList a b -> [b]
values (PartialFunctor c m o -> AssociationList o o
forall c m o. PartialFunctor c m o -> AssociationList o o
omapPF PartialFunctor c m o
funct)

    -- | Returns the objects not mapped onto by a partial functor.

    objectsNotMappedTo :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [o]
    objectsNotMappedTo :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [o]
objectsNotMappedTo PartialFunctor c m o
funct = (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob (PartialFunctor c m o -> c
forall m o. Morphism m o => m -> o
target PartialFunctor c m o
funct))[o] -> [o] -> [o]
forall a. Eq a => [a] -> [a] -> [a]
\\(PartialFunctor c m o -> [o]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [o]
codomainObjects PartialFunctor c m o
funct)
    
    -- | Returns the arrows mapped onto by a partial functor.

    codomainArrows :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [m]
    codomainArrows :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [m]
codomainArrows PartialFunctor c m o
funct = [m] -> [m]
forall a. Eq a => [a] -> [a]
nub ([m] -> [m]) -> [m] -> [m]
forall a b. (a -> b) -> a -> b
$ AssociationList m m -> [m]
forall a b. AssociationList a b -> [b]
values (PartialFunctor c m o -> AssociationList m m
forall c m o. PartialFunctor c m o -> AssociationList m m
mmapPF PartialFunctor c m o
funct)

    -- | Returns the arrows not mapped onto by a partial functor.

    arrowsNotMappedTo :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [m]
    arrowsNotMappedTo :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [m]
arrowsNotMappedTo PartialFunctor c m o
funct = (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows (PartialFunctor c m o -> c
forall m o. Morphism m o => m -> o
target PartialFunctor c m o
funct))[m] -> [m] -> [m]
forall a. Eq a => [a] -> [a] -> [a]
\\(PartialFunctor c m o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
PartialFunctor c m o -> [m]
codomainArrows PartialFunctor c m o
funct)