{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : Check the 'FiniteCategory' structure.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Provide a function to test the structure of a 'FiniteCategory'.
-}

module Math.FiniteCategoryError
(
    -- * Check structure

    FiniteCategoryError,
    checkFiniteCategory
)
where
    import              Data.WeakSet               (Set)
    import qualified    Data.WeakSet           as  Set
    import              Data.WeakSet.Safe
    import              Data.Simplifiable
    
    import              Math.FiniteCategory
    import              Math.IO.PrettyPrint

    import              GHC.Generics

    -- | A data type to represent an incoherence inside a finite category.

    data FiniteCategoryError m o =
         CompositionNotAssociative {forall m o. FiniteCategoryError m o -> m
f :: m, forall m o. FiniteCategoryError m o -> m
g :: m, forall m o. FiniteCategoryError m o -> m
h :: m, forall m o. FiniteCategoryError m o -> m
fg_h :: m, forall m o. FiniteCategoryError m o -> m
f_gh :: m} -- ^ @(h\@g)\@f /= h\@(g\@f)@

       | WrongSource {f :: m, forall m o. FiniteCategoryError m o -> o
realSource :: o} -- ^ `f` was found by using @'ar' c s t@ where @s /= 'source' f@.

       | WrongTarget {f :: m, forall m o. FiniteCategoryError m o -> o
realTarget :: o} -- ^ `f` was found by using @'ar' c s t@ where @t /= 'target' f@.

       | IdentityNotLeftNeutral {forall m o. FiniteCategoryError m o -> m
idL :: m, f :: m, forall m o. FiniteCategoryError m o -> m
foidL :: m} -- ^ `idL` is not a valid identity : @f \@ idL /= f@.

       | IdentityNotRightNeutral {f :: m, forall m o. FiniteCategoryError m o -> m
idR :: m, forall m o. FiniteCategoryError m o -> m
idRof :: m} -- ^ `idR` is not a valid identity : @idR \@ f /= f@.

       | MorphismsShouldNotBeEqual {f :: m, g :: m} -- ^ @f == g@ even though they don'y share the same source or target.

       | NotTransitive {f :: m, g :: m} -- ^ @f\@g@ is not an element of @ar c (source g) (target g)@.

       | GeneratorIsNotAMorphism {f :: m} -- ^ `f` is a generator but not a morphism.

       | MorphismDoesntDecomposesIntoGenerators {f :: m, forall m o. FiniteCategoryError m o -> [m]
decomp :: [m], forall m o. FiniteCategoryError m o -> m
notGen :: m} -- ^ The morphism `f` decomposes into `decomp` where `notGen` is a non generating morphism.

       | WrongDecomposition {f :: m, decomp :: [m], forall m o. FiniteCategoryError m o -> m
comp :: m} -- ^ @compose (decompose c f) /= f@.

       deriving (FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
(FiniteCategoryError m o -> FiniteCategoryError m o -> Bool)
-> (FiniteCategoryError m o -> FiniteCategoryError m o -> Bool)
-> Eq (FiniteCategoryError m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall m o.
(Eq o, Eq m) =>
FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
$c== :: forall m o.
(Eq o, Eq m) =>
FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
== :: FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
$c/= :: forall m o.
(Eq o, Eq m) =>
FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
/= :: FiniteCategoryError m o -> FiniteCategoryError m o -> Bool
Eq, Int -> FiniteCategoryError m o -> ShowS
[FiniteCategoryError m o] -> ShowS
FiniteCategoryError m o -> String
(Int -> FiniteCategoryError m o -> ShowS)
-> (FiniteCategoryError m o -> String)
-> ([FiniteCategoryError m o] -> ShowS)
-> Show (FiniteCategoryError m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall m o.
(Show o, Show m) =>
Int -> FiniteCategoryError m o -> ShowS
forall m o. (Show o, Show m) => [FiniteCategoryError m o] -> ShowS
forall m o. (Show o, Show m) => FiniteCategoryError m o -> String
$cshowsPrec :: forall m o.
(Show o, Show m) =>
Int -> FiniteCategoryError m o -> ShowS
showsPrec :: Int -> FiniteCategoryError m o -> ShowS
$cshow :: forall m o. (Show o, Show m) => FiniteCategoryError m o -> String
show :: FiniteCategoryError m o -> String
$cshowList :: forall m o. (Show o, Show m) => [FiniteCategoryError m o] -> ShowS
showList :: [FiniteCategoryError m o] -> ShowS
Show, (forall x.
 FiniteCategoryError m o -> Rep (FiniteCategoryError m o) x)
-> (forall x.
    Rep (FiniteCategoryError m o) x -> FiniteCategoryError m o)
-> Generic (FiniteCategoryError m o)
forall x.
Rep (FiniteCategoryError m o) x -> FiniteCategoryError m o
forall x.
FiniteCategoryError m o -> Rep (FiniteCategoryError m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall m o x.
Rep (FiniteCategoryError m o) x -> FiniteCategoryError m o
forall m o x.
FiniteCategoryError m o -> Rep (FiniteCategoryError m o) x
$cfrom :: forall m o x.
FiniteCategoryError m o -> Rep (FiniteCategoryError m o) x
from :: forall x.
FiniteCategoryError m o -> Rep (FiniteCategoryError m o) x
$cto :: forall m o x.
Rep (FiniteCategoryError m o) x -> FiniteCategoryError m o
to :: forall x.
Rep (FiniteCategoryError m o) x -> FiniteCategoryError m o
Generic, FiniteCategoryError m o -> FiniteCategoryError m o
(FiniteCategoryError m o -> FiniteCategoryError m o)
-> Simplifiable (FiniteCategoryError m o)
forall a. (a -> a) -> Simplifiable a
forall m o.
(Simplifiable m, Simplifiable o) =>
FiniteCategoryError m o -> FiniteCategoryError m o
$csimplify :: forall m o.
(Simplifiable m, Simplifiable o) =>
FiniteCategoryError m o -> FiniteCategoryError m o
simplify :: FiniteCategoryError m o -> FiniteCategoryError m o
Simplifiable, Int -> Int -> String -> FiniteCategoryError m o -> String
Int -> FiniteCategoryError m o -> String
(Int -> FiniteCategoryError m o -> String)
-> (Int -> Int -> String -> FiniteCategoryError m o -> String)
-> (Int -> FiniteCategoryError m o -> String)
-> PrettyPrint (FiniteCategoryError m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall m o.
(PrettyPrint m, PrettyPrint o) =>
Int -> Int -> String -> FiniteCategoryError m o -> String
forall m o.
(PrettyPrint m, PrettyPrint o) =>
Int -> FiniteCategoryError m o -> String
$cpprint :: forall m o.
(PrettyPrint m, PrettyPrint o) =>
Int -> FiniteCategoryError m o -> String
pprint :: Int -> FiniteCategoryError m o -> String
$cpprintWithIndentations :: forall m o.
(PrettyPrint m, PrettyPrint o) =>
Int -> Int -> String -> FiniteCategoryError m o -> String
pprintWithIndentations :: Int -> Int -> String -> FiniteCategoryError m o -> String
$cpprintIndent :: forall m o.
(PrettyPrint m, PrettyPrint o) =>
Int -> FiniteCategoryError m o -> String
pprintIndent :: Int -> FiniteCategoryError m o -> String
PrettyPrint)

    -- | Checks the category axioms for a 'FiniteCategory'.

    --

    -- If an error is found in the category, 'Just' a `FiniteCategoryError` is returned.

    -- Otherwise, 'Nothing' is returned.

    checkFiniteCategory :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Maybe (FiniteCategoryError m o)
    checkFiniteCategory :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkFiniteCategory c
c
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m)] -> Bool) -> [(m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m)]
incoherentEq = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just MorphismsShouldNotBeEqual {f :: m
f=((m, m) -> m
forall a b. (a, b) -> a
fst((m, m) -> m) -> ([(m, m)] -> (m, m)) -> [(m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> (m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m)]
incoherentEq, g :: m
g=((m, m) -> m
forall a b. (a, b) -> b
snd((m, m) -> m) -> ([(m, m)] -> (m, m)) -> [(m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> (m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m)]
incoherentEq}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, o)] -> Bool) -> [(m, o)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, o)]
wrongSource = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just WrongSource {f :: m
f = ((m, o) -> m
forall a b. (a, b) -> a
fst((m, o) -> m) -> ([(m, o)] -> (m, o)) -> [(m, o)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> (m, o)
forall a. HasCallStack => [a] -> a
head) [(m, o)]
wrongSource, realSource :: o
realSource = ((m, o) -> o
forall a b. (a, b) -> b
snd((m, o) -> o) -> ([(m, o)] -> (m, o)) -> [(m, o)] -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> (m, o)
forall a. HasCallStack => [a] -> a
head) [(m, o)]
wrongSource}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, o)] -> Bool) -> [(m, o)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, o)]
wrongTarget = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just WrongTarget {f :: m
f = ((m, o) -> m
forall a b. (a, b) -> a
fst((m, o) -> m) -> ([(m, o)] -> (m, o)) -> [(m, o)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> (m, o)
forall a. HasCallStack => [a] -> a
head) [(m, o)]
wrongTarget, realTarget :: o
realTarget = ((m, o) -> o
forall a b. (a, b) -> b
snd((m, o) -> o) -> ([(m, o)] -> (m, o)) -> [(m, o)] -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, o)] -> (m, o)
forall a. HasCallStack => [a] -> a
head) [(m, o)]
wrongTarget}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m, m)] -> Bool) -> [(m, m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m, m)]
idNotLNeutral = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just IdentityNotLeftNeutral {idL :: m
idL=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
idNotLNeutral, f :: m
f=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
idNotLNeutral,foidL :: m
foidL=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
idNotLNeutral} 
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m, m)] -> Bool) -> [(m, m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m, m)]
idNotRNeutral = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just IdentityNotRightNeutral {f :: m
f=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
idNotRNeutral, idR :: m
idR=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
idNotRNeutral,idRof :: m
idRof=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
idNotRNeutral} 
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m, m)] -> Bool) -> [(m, m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m, m)]
notAssociative = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just CompositionNotAssociative {f :: m
f=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
notAssociative,g :: m
g=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
notAssociative,h :: m
h=((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m, m)]
notAssociative, fg_h :: m
fg_h=((((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head)[(m, m, m)]
notAssociative) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head)[(m, m, m)]
notAssociative)) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head)[(m, m, m)]
notAssociative),
                        f_gh :: m
f_gh=(((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head)[(m, m, m)]
notAssociative) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ ((((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head)[(m, m, m)]
notAssociative) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (((m, m, m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, m, m) -> m) -> ([(m, m, m)] -> (m, m, m)) -> [(m, m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m, m)] -> (m, m, m)
forall a. HasCallStack => [a] -> a
head)[(m, m, m)]
notAssociative))}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, m)] -> Bool) -> [(m, m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, m)]
notTransitive = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just NotTransitive {f :: m
f=((m, m) -> m
forall a b. (a, b) -> a
fst((m, m) -> m) -> ([(m, m)] -> (m, m)) -> [(m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> (m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m)]
notTransitive, g :: m
g=((m, m) -> m
forall a b. (a, b) -> b
snd((m, m) -> m) -> ([(m, m)] -> (m, m)) -> [(m, m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, m)] -> (m, m)
forall a. HasCallStack => [a] -> a
head) [(m, m)]
notTransitive}
        | (Bool -> Bool
not(Bool -> Bool) -> (Set m -> Bool) -> Set m -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set m -> Bool
forall a. Set a -> Bool
Set.null)) Set m
genNotMorph = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just GeneratorIsNotAMorphism {f :: m
f=[m] -> m
forall a. HasCallStack => [a] -> a
head([m] -> m) -> (Set m -> [m]) -> Set m -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set m -> [m]
forall a. Eq a => Set a -> [a]
setToList (Set m -> m) -> Set m -> m
forall a b. (a -> b) -> a -> b
$ Set m
genNotMorph}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, [m], m)] -> Bool) -> [(m, [m], m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, [m], m)]
decompIntoComposite = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just MorphismDoesntDecomposesIntoGenerators {f :: m
f=((m, [m], m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, [m], m) -> m)
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. HasCallStack => [a] -> a
head) [(m, [m], m)]
decompIntoComposite, decomp :: [m]
decomp=((m, [m], m) -> [m]
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, [m], m) -> [m])
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> [m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. HasCallStack => [a] -> a
head) [(m, [m], m)]
decompIntoComposite, notGen :: m
notGen=((m, [m], m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, [m], m) -> m)
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. HasCallStack => [a] -> a
head) [(m, [m], m)]
decompIntoComposite}
        | (Bool -> Bool
not(Bool -> Bool) -> ([(m, [m], m)] -> Bool) -> [(m, [m], m)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(m, [m], m)]
wrongDecomp = FiniteCategoryError m o -> Maybe (FiniteCategoryError m o)
forall a. a -> Maybe a
Just WrongDecomposition {f :: m
f=((m, [m], m) -> m
forall {a} {b} {c}. (a, b, c) -> a
fst3((m, [m], m) -> m)
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. HasCallStack => [a] -> a
head) [(m, [m], m)]
wrongDecomp, decomp :: [m]
decomp=((m, [m], m) -> [m]
forall {a} {b} {c}. (a, b, c) -> b
snd3((m, [m], m) -> [m])
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> [m]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. HasCallStack => [a] -> a
head) [(m, [m], m)]
wrongDecomp, comp :: m
comp=((m, [m], m) -> m
forall {a} {b} {c}. (a, b, c) -> c
trd3((m, [m], m) -> m)
-> ([(m, [m], m)] -> (m, [m], m)) -> [(m, [m], m)] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(m, [m], m)] -> (m, [m], m)
forall a. HasCallStack => [a] -> a
head) [(m, [m], m)]
wrongDecomp}
        | Bool
otherwise = Maybe (FiniteCategoryError m o)
forall a. Maybe a
Nothing
        where
            incoherentEq :: [(m, m)]
incoherentEq = Set (m, m) -> [(m, m)]
forall a. Eq a => Set a -> [a]
setToList (Set (m, m) -> [(m, m)]) -> Set (m, m) -> [(m, m)]
forall a b. (a -> b) -> a -> b
$ ((m, m) -> Bool) -> Set (m, m) -> Set (m, m)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(m
f,m
g) -> m
f m -> m -> Bool
forall a. Eq a => a -> a -> Bool
== m
g 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)) (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c Set m -> Set m -> Set (m, m)
forall a b. Set a -> Set b -> Set (a, b)
|*| c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c)
            wrongSource :: [(m, o)]
wrongSource = [(m
f,o
s) | o
s <- 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, o
t <- 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
f <- 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
s o
t, m -> o
forall m o. Morphism m o => m -> o
source m
f o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= o
s]
            wrongTarget :: [(m, o)]
wrongTarget = [(m
f,o
t) | o
s <- 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, o
t <- 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
f <- 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
s o
t, m -> o
forall m o. Morphism m o => m -> o
target m
f o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= o
t]
            idNotLNeutral :: [(m, m, m)]
idNotLNeutral = [(c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f),m
f,m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f)) | m
f <- 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 -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c, m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
source m
f) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
/= m
f]
            idNotRNeutral :: [(m, m, m)]
idNotRNeutral = [(m
f,c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f), c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f) | m
f <- 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 -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c, c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c (m -> o
forall m o. Morphism m o => m -> o
target m
f) 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
f]
            notAssociative :: [(m, m, m)]
notAssociative = [(m
x,m
y,m
z) | m
z <- 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 -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c, m
y <- 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
arFrom c
c (m -> o
forall m o. Morphism m o => m -> o
target m
z), m
x <- 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
arFrom c
c (m -> o
forall m o. Morphism m o => m -> o
target m
y), (m
x m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
y) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
z m -> m -> Bool
forall a. Eq a => a -> a -> Bool
/= m
x m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (m
y m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
z)]
            notTransitive :: [(m, m)]
notTransitive = [(m
f,m
g) | 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 -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c, m
f <- 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
arFrom c
c (m -> o
forall m o. Morphism m o => m -> o
target m
g), Bool -> Bool
not ((m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
g) m -> Set m -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (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
source m
g) (m -> o
forall m o. Morphism m o => m -> o
target m
f)))]
            genNotMorph :: Set m
genNotMorph = c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows c
c Set m -> Set m -> Set m
forall a. Eq a => Set a -> Set a -> Set a
|-| c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c
            decompIntoComposite :: [(m, [m], m)]
decompIntoComposite = [(m
m,c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
c m
m,m
f) | m
m <- 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 -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c, m
f <- c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
c m
m, Bool -> Bool
not (m
f m -> Set m -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr 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)))]
            wrongDecomp :: [(m, [m], m)]
wrongDecomp = [(m
f,c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
c m
f, [m] -> m
forall m o. Morphism m o => [m] -> m
compose (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
c m
f)) | m
f <- 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 -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c, [m] -> m
forall m o. Morphism m o => [m] -> m
compose (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
c m
f) m -> m -> Bool
forall a. Eq a => a -> a -> Bool
/= m
f]
            fst3 :: (a, b, c) -> a
fst3 (a
x,b
_,c
_) = a
x
            snd3 :: (a, b, c) -> b
snd3 (a
_,b
x,c
_) = b
x
            trd3 :: (a, b, c) -> c
trd3 (a
_,b
_,c
x) = c
x