{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies  #-}

{-| Module  : FiniteCategories
Description : A 'FiniteCategory' is a 'Category' where the objects can be enumerated.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'FiniteCategory' is a 'Category' where the objects can be enumerated.

This module exports Math.Category so that you only have to import one of them.
-}

module Math.FiniteCategory
(
    -- * FiniteCategory

    FiniteCategory(..),
    -- ** Morphism enumeration

    arrows,
    arFrom,
    arTo,
    arFrom2,
    arTo2,
    identities,
    -- ** Morphism predicates

    isEpic,
    isMonic,
    -- ** Object predicates

    isTerminal,
    isInitial,
    -- ** Find special objects

    terminalObjects,
    initialObjects,
    -- * Generated finite category

    -- ** Generator enumeration

    genArrows,
    genArFrom,
    genArTo,
    genArFrom2,
    genArTo2,
    -- ** Helper

    bruteForceDecompose,
    module Math.Category
)
where
    import              Data.WeakSet                (Set)
    import qualified    Data.WeakSet           as   Set
    import              Data.WeakSet.Safe
    import              Data.List                   (elemIndex)
    
    import              Math.Category
    
    import              Control.Monad               (join)
    
        
    -- | A 'FiniteCategory' is a 'Category' which allows to enumerate its objects.

    --

    -- It is assumed that the set of objects of the category is finite.

    class (Category c m o) => FiniteCategory c m o | c -> m, m -> o where
        -- | `ob` should return a set of objects.

        ob :: c -> Set o
            
    -- | `arrows` returns the set of all unique morphisms of a category.

    arrows :: (FiniteCategory c m o, Morphism m o) => c -> Set m
    arrows :: forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c (o -> o -> Set m) -> Set o -> Set (o -> Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c Set (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c
        
    -- | `arTo` returns the set of morphisms going to a specified target.

    arTo :: (FiniteCategory c m o, Morphism m o) => c -> o -> Set m
    arTo :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arTo c
c o
t = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ (\o
s -> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s o
t) (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c

    -- | `arTo2` same as `arTo` but for multiple targets.

    arTo2 :: (FiniteCategory c m o, Morphism m o) => c -> Set o -> Set m
    arTo2 :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Set o -> Set m
arTo2 c
c Set o
ts = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c (o -> o -> Set m) -> Set o -> Set (o -> Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c Set (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set o
ts

    -- | `arFrom` returns the list of unique morphisms going from a specified source.

    arFrom :: (FiniteCategory c m o, Morphism m o) => c -> o -> Set m
    arFrom :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arFrom c
c o
s = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c

    -- | `arFrom2` same as `arFrom` but for multiple sources.

    arFrom2 :: (FiniteCategory c m o, Morphism m o) => c -> Set o -> Set m
    arFrom2 :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Set o -> Set m
arFrom2 c
c Set o
ss = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c (o -> o -> Set m) -> Set o -> Set (o -> Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set o
ss Set (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c

    -- | Same as `arrows` but only returns the generators. @genArrows c@ should be included in @arrows c@.  

    genArrows :: (FiniteCategory c m o, Morphism m o) => c -> Set m
    genArrows :: forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows c
c = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c (o -> o -> Set m) -> Set o -> Set (o -> Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c Set (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c

    -- | Same as `arTo` but only returns the generators. @genArTo c t@ should be included in @arTo c t@.       

    genArTo :: (FiniteCategory c m o, Morphism m o) => c -> o -> Set m
    genArTo :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArTo c
c o
t = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ (\o
s -> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c o
s o
t) (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c 
        
    -- | Same as `arTo2` but only returns the generators. @genArTo2 c (set [t])@ should be included in @arTo2 c (set [t])@.  

    genArTo2 :: (FiniteCategory c m o, Morphism m o) => c -> Set o -> Set m
    genArTo2 :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Set o -> Set m
genArTo2 c
c Set o
ts = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ (c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c) (o -> o -> Set m) -> Set o -> Set (o -> Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c Set (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set o
ts 
        
    -- | Same as `arFrom` but only returns the generators. @genArFrom c s@ should be included in @arFrom c s@.  

    genArFrom :: (FiniteCategory c m o, Morphism m o) => c -> o -> Set m
    genArFrom :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom c
c o
s = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ (c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c o
s) (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c 
        
    -- | Same as `arFrom2` but only returns the generators. @genArFrom2 c (set [s])@ should be included in @arFrom2 c (set [s])@.  

    genArFrom2 :: (FiniteCategory c m o, Morphism m o) => c -> Set o -> Set m
    genArFrom2 :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Set o -> Set m
genArFrom2 c
c Set o
ss = Set (Set m) -> Set m
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Set (Set m) -> Set m) -> Set (Set m) -> Set m
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c (o -> o -> Set m) -> Set o -> Set (o -> Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set o
ss Set (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c 

    -- | `identities` returns all the identities of a category.

    identities :: (FiniteCategory c m o, Morphism m o) => c -> Set m
    identities :: forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
identities c
c = c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c (o -> m) -> Set o -> Set m
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c
    
    -- | Return wether an object is initial in the category.

    isInitial :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> o -> Bool
    isInitial :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Bool
isInitial c
cat o
obj = let
                            morphisms :: o -> [a]
morphisms o
t = Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList (Set a -> [a]) -> Set a -> [a]
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set a
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
cat o
obj o
t
                            condition :: o -> Bool
condition o
t = (Bool -> Bool
not(Bool -> Bool) -> ([a] -> Bool) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a] -> Bool) -> [a] -> Bool
forall a b. (a -> b) -> a -> b
$ o -> [a]
forall {a}. (Eq a, Category c a o, Morphism a o) => o -> [a]
morphisms o
t) Bool -> Bool -> Bool
&& ([a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null([a] -> Bool) -> ([a] -> [a]) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[a] -> [a]
forall a. [a] -> [a]
tail ([a] -> Bool) -> [a] -> Bool
forall a b. (a -> b) -> a -> b
$ o -> [a]
forall {a}. (Eq a, Category c a o, Morphism a o) => o -> [a]
morphisms o
t) -- we avoid the usage of cardinal to test that the size of (ar cat obj t) is 1 for speed purposes

                        in
                            Set Bool -> Bool
Set.and (Set Bool -> Bool) -> Set Bool -> Bool
forall a b. (a -> b) -> a -> b
$ o -> Bool
forall {a}. (Category c a o, Eq a, Morphism a o) => o -> Bool
condition (o -> Bool) -> Set o -> Set Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat 
    
    -- | Return the set of intial objects in a category.

    initialObjects :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o
    initialObjects :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
initialObjects c
cat = (o -> Bool) -> Set o -> Set o
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> o -> Bool
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Bool
isInitial c
cat) (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat)
    
    -- | Return wether an object is terminal in the category.

    isTerminal :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> o -> Bool
    isTerminal :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Bool
isTerminal c
cat o
obj = let
                            morphisms :: o -> [a]
morphisms o
s = Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList (Set a -> [a]) -> Set a -> [a]
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set a
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
cat o
s o
obj
                            condition :: o -> Bool
condition o
s = (Bool -> Bool
not(Bool -> Bool) -> ([a] -> Bool) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a] -> Bool) -> [a] -> Bool
forall a b. (a -> b) -> a -> b
$ o -> [a]
forall {a}. (Eq a, Category c a o, Morphism a o) => o -> [a]
morphisms o
s) Bool -> Bool -> Bool
&& ([a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null([a] -> Bool) -> ([a] -> [a]) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[a] -> [a]
forall a. [a] -> [a]
tail ([a] -> Bool) -> [a] -> Bool
forall a b. (a -> b) -> a -> b
$ o -> [a]
forall {a}. (Eq a, Category c a o, Morphism a o) => o -> [a]
morphisms o
s) -- we avoid the usage of cardinal to test that the size of (ar cat s obj) is 1 for speed purposes

                        in
                            Set Bool -> Bool
Set.and (Set Bool -> Bool) -> Set Bool -> Bool
forall a b. (a -> b) -> a -> b
$ o -> Bool
forall {a}. (Category c a o, Eq a, Morphism a o) => o -> Bool
condition (o -> Bool) -> Set o -> Set Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat 
        
    -- | Return the set of terminal objects in a category.

    terminalObjects :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o
    terminalObjects :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
terminalObjects c
cat = (o -> Bool) -> Set o -> Set o
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> o -> Bool
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Bool
isTerminal c
cat) (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat)
    
    -- | Return wether a morphism is a monomorphism.

    isMonic :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isMonic :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isMonic c
c m
f = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
g m -> m -> Bool
forall a. Eq a => a -> a -> Bool
/= m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
h Bool -> Bool -> Bool
|| m
g m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== m
h| o
x <- Set o -> [o]
forall a. Eq a => Set a -> [a]
setToList (Set o -> [o]) -> Set o -> [o]
forall a b. (a -> b) -> a -> b
$ c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c, m
g <- Set m -> [m]
forall a. Eq a => Set a -> [a]
setToList (Set m -> [m]) -> Set m -> [m]
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
x (m -> o
forall m o. Morphism m o => m -> o
source m
f), m
h <- Set m -> [m]
forall a. Eq a => Set a -> [a]
setToList (Set m -> [m]) -> Set m -> [m]
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
x (m -> o
forall m o. Morphism m o => m -> o
source m
f)]
    
    -- | Return wether a morphism is an epimorphism.

    isEpic :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isEpic :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isEpic c
c m
f = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [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
/= m
h m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f Bool -> Bool -> Bool
|| m
g m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== m
h | o
x <- Set o -> [o]
forall a. Eq a => Set a -> [a]
setToList (Set o -> [o]) -> Set o -> [o]
forall a b. (a -> b) -> a -> b
$ c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c, m
g <- Set m -> [m]
forall a. Eq a => Set a -> [a]
setToList (Set m -> [m]) -> Set m -> [m]
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f) o
x, m
h <- Set m -> [m]
forall a. Eq a => Set a -> [a]
setToList (Set m -> [m]) -> Set m -> [m]
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f) o
x]
    
    -- | Helper function for `bruteForceDecompose`.

    bruteForce :: (FiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [[m]] -> [m]
    bruteForce :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [[m]] -> [m]
bruteForce c
c m
m [[m]]
l = if Maybe Int
index Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Int
forall a. Maybe a
Nothing then c -> m -> [[m]] -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [[m]] -> [m]
bruteForce c
c m
m ([[[m]]] -> [[m]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([m] -> [[m]]
forall {a} {a}.
(Eq a, FiniteCategory c a a, Morphism a a) =>
[a] -> [[a]]
pathToAugmentedPaths ([m] -> [[m]]) -> [[m]] -> [[[m]]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[m]]
l)) else [[m]]
l [[m]] -> Int -> [m]
forall a. [a] -> Int -> a
!! Int
i where
        index :: Maybe Int
index = m -> [m] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex m
m ([m] -> m
forall m o. Morphism m o => [m] -> m
compose ([m] -> m) -> [[m]] -> [m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[m]]
l)
        Just Int
i = Maybe Int
index
        leavingMorph :: [b] -> [a]
leavingMorph [b]
path = (Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList(Set a -> [a]) -> (a -> Set a) -> a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(c -> a -> Set a
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom c
c)) (a -> [a]) -> a -> [a]
forall a b. (a -> b) -> a -> b
$ b -> a
forall m o. Morphism m o => m -> o
target(b -> a) -> ([b] -> b) -> [b] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[b] -> b
forall a. [a] -> a
head ([b] -> a) -> [b] -> a
forall a b. (a -> b) -> a -> b
$ [b]
path
        pathToAugmentedPaths :: [a] -> [[a]]
pathToAugmentedPaths [a]
path = ([a] -> [a]
forall {a} {a} {b}.
(Eq a, FiniteCategory c a a, Morphism a a, Morphism b a) =>
[b] -> [a]
leavingMorph [a]
path) [a] -> (a -> [[a]]) -> [[a]]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a
x -> [(a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
path)] )   
    
    -- | If `genAr` is implemented, we can find the decomposition of a morphism by bruteforce search (we compose every arrow until we get the morphism we want).

    --

    -- This method is meant to be used temporarly until a proper decompose method is implemented. (It is very slow.)

    bruteForceDecompose :: (FiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [m]
    bruteForceDecompose :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [m]
bruteForceDecompose c
c m
m = c -> m -> [[m]] -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [[m]] -> [m]
bruteForce c
c m
m ((m -> [m] -> [m]
forall a. a -> [a] -> [a]
:[]) (m -> [m]) -> [m] -> [[m]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set m -> [m]
forall a. Eq a => Set a -> [a]
setToList (Set m -> [m]) -> Set m -> [m]
forall a b. (a -> b) -> a -> b
$ c -> o -> Set m
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom c
c (m -> o
forall m o. Morphism m o => m -> o
source m
m)))