{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
module Math.FiniteCategory
(
FiniteCategory(..),
arrows,
arFrom,
arTo,
arFrom2,
arTo2,
identities,
isEpic,
isMonic,
isTerminal,
isInitial,
terminalObjects,
initialObjects,
genArrows,
genArFrom,
genArTo,
genArFrom2,
genArTo2,
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)
class (Category c m o) => FiniteCategory c m o | c -> m, m -> o where
ob :: c -> Set o
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 :: (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 :: (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 :: (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 :: (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
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
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
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
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
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 :: (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
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)
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
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)
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)
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
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)
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)]
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]
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)] )
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)))