{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}

{-| 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,
    arrowsWithoutId,
    arFromWithoutId,
    arToWithoutId,
    arFrom2WithoutId,
    arTo2WithoutId,
    identities,
    -- ** Morphism predicates

    isEpic,
    isMonic,
    -- ** Object predicates

    isTerminal,
    isInitial,
    -- ** Find special objects

    terminalObjects,
    initialObjects,
    -- * Generated finite category

    -- ** Generator enumeration

    genArrows,
    genArFrom,
    genArTo,
    genArFrom2,
    genArTo2,
    genArrowsWithoutId,
    genArFromWithoutId,
    genArToWithoutId,
    genArFrom2WithoutId,
    genArTo2WithoutId,
    
    -- ** Helper

    bruteForceDecompose,
    pprintFiniteCategory,
    module Math.Category
)
where
    import              Data.WeakSet                (Set)
    import qualified    Data.WeakSet           as   Set
    import              Data.WeakSet.Safe
    import              Data.List                   (elemIndex, intercalate)
    
    import              Math.Category
    import              Math.IO.PrettyPrint
    
    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 a b. Set (a -> b) -> Set a -> Set b
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 a b. Set (a -> b) -> Set a -> Set b
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 a b. Set (a -> b) -> Set a -> Set b
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 without identities.  

    arrowsWithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set m
    arrowsWithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
arrowsWithoutId c
c = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c) (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c)

    -- | Same as `arTo` but without identities. 

    arToWithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> o -> Set m
    arToWithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Set m
arToWithoutId c
c o
t = ((m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c)) (Set m -> Set m) -> Set m -> Set 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
arTo c
c o
t
        
    -- | Same as `arTo2` but without identities. 

    arTo2WithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o -> Set m
    arTo2WithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o -> Set m
arTo2WithoutId c
c Set o
ts = ((m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> Set o -> Set m
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Set o -> Set m
arTo2 c
c Set o
ts
        
    -- | Same as `arFrom` but without identities. 

    arFromWithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> o -> Set m
    arFromWithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Set m
arFromWithoutId c
c o
s = ((m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c)) (Set m -> Set m) -> Set m -> Set 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
arFrom c
c o
s
        
    -- | Same as `arFrom2` but without identities.

    arFrom2WithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o -> Set m
    arFrom2WithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o -> Set m
arFrom2WithoutId c
c Set o
ss = ((m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> Set o -> Set m
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Set o -> Set m
arFrom2 c
c Set o
ss

    -- | 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 a b. Set (a -> b) -> Set a -> Set b
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 a b. Set (a -> b) -> Set a -> Set b
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 a b. Set (a -> b) -> Set a -> Set b
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 `genArrows` but without identities.  

    genArrowsWithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set m
    genArrowsWithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId c
c = (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c) (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows c
c)

    -- | Same as `genArTo` but without identities. 

    genArToWithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> o -> Set m
    genArToWithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Set m
genArToWithoutId c
c o
t = ((m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c)) (Set m -> Set m) -> Set m -> Set 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
genArTo c
c o
t
        
    -- | Same as `genArTo2` but without identities. 

    genArTo2WithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o -> Set m
    genArTo2WithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o -> Set m
genArTo2WithoutId c
c Set o
ts = ((m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> Set o -> Set m
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Set o -> Set m
genArTo2 c
c Set o
ts
        
    -- | Same as `genArFrom` but without identities. 

    genArFromWithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> o -> Set m
    genArFromWithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Set m
genArFromWithoutId c
c o
s = ((m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c)) (Set m -> Set m) -> Set m -> Set 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 o
s
        
    -- | Same as `genArFrom2` but without identities.

    genArFrom2WithoutId :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o -> Set m
    genArFrom2WithoutId :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o -> Set m
genArFrom2WithoutId c
c Set o
ss = ((m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
c)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> Set o -> Set m
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Set o -> Set m
genArFrom2 c
c Set o
ss
    
    



    -- | `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 -> Set m
morphisms o
t = c -> o -> o -> Set m
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) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ o -> Set m
morphisms o
t) Bool -> Bool -> Bool
&& (Set Bool -> Bool
Set.and ((Set m -> m
forall a. Set a -> a
anElement (o -> Set m
morphisms o
t) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
==) (m -> Bool) -> Set m -> Set Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> o -> Set m
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
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 -> Set m
morphisms 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
cat o
s o
obj
                            condition :: o -> Bool
condition o
s = (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ o -> Set m
morphisms o
s) Bool -> Bool -> Bool
&& (Set Bool -> Bool
Set.and ((Set m -> m
forall a. Set a -> a
anElement (o -> Set m
morphisms o
s) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
==) (m -> Bool) -> Set m -> Set Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> o -> Set m
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
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]]
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. HasCallStack => [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] -> [m]
leavingMorph [b]
path = (Set m -> [m]
forall a. Eq a => Set a -> [a]
setToList(Set m -> [m]) -> (o -> Set m) -> o -> [m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(c -> o -> Set m
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom c
c)) (o -> [m]) -> o -> [m]
forall a b. (a -> b) -> a -> b
$ b -> o
forall m o. Morphism m o => m -> o
target(b -> o) -> ([b] -> b) -> [b] -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[b] -> b
forall a. HasCallStack => [a] -> a
head ([b] -> o) -> [b] -> o
forall a b. (a -> b) -> a -> b
$ [b]
path
        pathToAugmentedPaths :: [m] -> [[m]]
pathToAugmentedPaths [m]
path = ([m] -> [m]
forall {b}. Morphism b o => [b] -> [m]
leavingMorph [m]
path) [m] -> (m -> [[m]]) -> [[m]]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\m
x -> [(m
xm -> [m] -> [m]
forall a. a -> [a] -> [a]
:[m]
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))) 
    
    
    -- | Pretty print a category by enumerating all objects, and then all arrows. The first argument is the verbosity of the pretty print.

    pprintFiniteCategory :: (FiniteCategory c m o, Morphism m o, PrettyPrint c, PrettyPrint m, PrettyPrint o, Eq m, Eq o) => Int -> c -> String
    pprintFiniteCategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, PrettyPrint c, PrettyPrint m,
 PrettyPrint o, Eq m, Eq o) =>
Int -> c -> String
pprintFiniteCategory Int
v c
c = String
"Category : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> c -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v c
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\nObjects :\n\n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" (Set String -> [String]
forall a. Eq a => Set a -> [a]
setToList (Set String -> [String]) -> Set String -> [String]
forall a b. (a -> b) -> a -> b
$ Int -> o -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v (o -> String) -> Set o -> Set String
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)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\nArrows :\n\n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" (Set String -> [String]
forall a. Eq a => Set a -> [a]
setToList (Set String -> [String]) -> Set String -> [String]
forall a b. (a -> b) -> a -> b
$ Int -> m -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v (m -> String) -> Set m -> Set String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c))