{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, MonadComprehensions  #-}

{-| Module  : FiniteCategories
Description : __'FinCat'__ is the category of finite categories, 'FinFunctor's are the morphisms of __'FinCat'__.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __FinCat__ category has as objects finite categories and as morphisms homogeneous functors between them.

Functors must be homogeneous because otherwise we would not be able to compose them with the 'Morphism' typeclass.

The 'FinCat' datatype should not be confused with the `FiniteCategory` typeclass. The `FiniteCategory` typeclass describes axioms a structure should follow to be considered a finite category. The 'FinCat' type is itself a 'Category'.

A 'FinFunctor' is a 'Diagram' where the source and target category are the same. The source category of a 'FinFunctor' should be finite.
-}

module Math.Categories.FinCat
(
    -- * Homogeneous functor

    FinFunctor(..),
    -- * __FinCat__

    FinCat(..)
)
where
    import              Data.WeakSet             (Set)
    import qualified    Data.WeakSet           as Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap             (Map)
    import qualified    Data.WeakMap           as Map
    import              Data.WeakMap.Safe
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.Categories.FunctorCategory
    import              Math.IO.PrettyPrint
    
    -- | A `FinFunctor` /funct/ between two categories is a map between objects and a map between arrows of the two categories such that :

    --

    -- prop> funct ->$ (source f) == source (funct ->£ f)

    -- prop> funct ->$ (target f) == target (funct ->£ f)

    -- prop> funct ->£ (f @ g) = (funct ->£ f) @ (funct ->£ g)

    -- prop> funct ->£ (identity a) = identity (funct ->$ a)

    --

    -- A 'FinFunctor' is a type of 'Diagram'.

    --

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

    --

    -- See 'Diagram' in Math.Categories.FunctorCategory for heterogeneous ones.

    type FinFunctor c m o = Diagram c m o c m o
    
    instance (Eq c, Eq m, Eq o) => Morphism (Diagram c m o c m o) c where
        @? :: Diagram c m o c m o
-> Diagram c m o c m o -> Maybe (Diagram c m o c m o)
(@?) Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c
s2,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c
t2,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o o
om2,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m m
fm2} Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c
s1,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c
t1,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o o
om1,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m m
fm1}
            | c
t1 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
/= c
s2 = Maybe (Diagram c m o c m o)
forall a. Maybe a
Nothing
            | Bool
otherwise = Diagram c m o c m o -> Maybe (Diagram c m o c m o)
forall a. a -> Maybe a
Just Diagram{src :: c
src=c
s1,tgt :: c
tgt=c
t2,omap :: Map o o
omap=Map o o
om2Map o o -> Map o o -> Map o o
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.|Map o o
om1,mmap :: Map m m
mmap=Map m m
fm2Map m m -> Map m m -> Map m m
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.|Map m m
fm1}
        source :: Diagram c m o c m o -> c
source = Diagram c m o c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src
        target :: Diagram c m o c m o -> c
target = Diagram c m o c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt
          
    -- | The __'FinCat'__ category has as objects finite categories and as morphisms homogeneous functors between them.

    data FinCat c m o = FinCat deriving (FinCat c m o -> FinCat c m o -> Bool
(FinCat c m o -> FinCat c m o -> Bool)
-> (FinCat c m o -> FinCat c m o -> Bool) -> Eq (FinCat c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o. FinCat c m o -> FinCat c m o -> Bool
$c== :: forall c m o. FinCat c m o -> FinCat c m o -> Bool
== :: FinCat c m o -> FinCat c m o -> Bool
$c/= :: forall c m o. FinCat c m o -> FinCat c m o -> Bool
/= :: FinCat c m o -> FinCat c m o -> Bool
Eq, Int -> FinCat c m o -> ShowS
[FinCat c m o] -> ShowS
FinCat c m o -> String
(Int -> FinCat c m o -> ShowS)
-> (FinCat c m o -> String)
-> ([FinCat c m o] -> ShowS)
-> Show (FinCat c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o. Int -> FinCat c m o -> ShowS
forall c m o. [FinCat c m o] -> ShowS
forall c m o. FinCat c m o -> String
$cshowsPrec :: forall c m o. Int -> FinCat c m o -> ShowS
showsPrec :: Int -> FinCat c m o -> ShowS
$cshow :: forall c m o. FinCat c m o -> String
show :: FinCat c m o -> String
$cshowList :: forall c m o. [FinCat c m o] -> ShowS
showList :: [FinCat c m o] -> ShowS
Show)
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (FinCat c m o) (Diagram c m o c m o) c where
        identity :: Morphism (Diagram c m o c m o) c =>
FinCat c m o -> c -> Diagram c m o c m o
identity FinCat c m o
_ c
cat = Diagram{src :: c
src=c
cat,tgt :: c
tgt=c
cat,omap :: Map o o
omap=(o -> o) -> Set o -> Map o o
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction o -> o
forall a. a -> a
id (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat),mmap :: Map m m
mmap=(m -> m) -> Set m -> Map m m
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction m -> m
forall a. a -> a
id (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
cat)}
        ar :: Morphism (Diagram c m o c m o) c =>
FinCat c m o -> c -> c -> Set (Diagram c m o c m o)
ar FinCat c m o
_ c
s c
t = (Set (DiagramError c m o c m o), Set (Diagram c m o c m o))
-> Set (Diagram c m o c m o)
forall a b. (a, b) -> b
snd((Set (DiagramError c m o c m o), Set (Diagram c m o c m o))
 -> Set (Diagram c m o c m o))
-> (Set (Either (DiagramError c m o c m o) (Diagram c m o c m o))
    -> (Set (DiagramError c m o c m o), Set (Diagram c m o c m o)))
-> Set (Either (DiagramError c m o c m o) (Diagram c m o c m o))
-> Set (Diagram c m o c m o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set (Either (DiagramError c m o c m o) (Diagram c m o c m o))
-> (Set (DiagramError c m o c m o), Set (Diagram c m o c m o))
forall a b. Set (Either a b) -> (Set a, Set b)
Set.catEither) (Set (Either (DiagramError c m o c m o) (Diagram c m o c m o))
 -> Set (Diagram c m o c m o))
-> Set (Either (DiagramError c m o c m o) (Diagram c m o c m o))
-> Set (Diagram c m o c m o)
forall a b. (a -> b) -> a -> b
$ [c
-> c
-> Map o o
-> Map m m
-> Either (DiagramError c m o c m o) (Diagram c m o c m o)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
c1
-> c2
-> Map o1 o2
-> Map m1 m2
-> Either
     (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
diagram c
s c
t Map o o
appO Map m m
appF | Map o o
appO <- Set (Map o o)
appObj, Map m m
appF <- ((([Map m m] -> Map m m) -> Set [Map m m] -> Set (Map m m)
forall a b. (a -> b) -> Set a -> Set b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Map m m] -> Map m m) -> Set [Map m m] -> Set (Map m m))
-> ([Map m m] -> Map m m) -> Set [Map m m] -> Set (Map m m)
forall a b. (a -> b) -> a -> b
$ ([Map m m] -> Map m m
forall k a. Eq k => [Map k a] -> Map k a
Map.unions))(Set [Map m m] -> Set (Map m m))
-> ([Set (Map m m)] -> Set [Map m m])
-> [Set (Map m m)]
-> Set (Map m m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[Set (Map m m)] -> Set [Map m m]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets) [o -> o -> Map o o -> Set (Map m m)
twoObjToMaps o
a o
b Map o o
appO| o
a <- (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
s), o
b <- (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
s)]]
            where
                appObj :: Set (Map o o)
appObj = Set o -> Set o -> Set (Map o o)
forall a b. (Eq a, Eq b) => Set a -> Set b -> Set (Map a b)
Map.enumerateMaps (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
s) (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
t)
                twoObjToMaps :: o -> o -> Map o o -> Set (Map m m)
twoObjToMaps o
a o
b Map o o
appO = Set m -> Set m -> Set (Map m m)
forall a b. (Eq a, Eq b) => Set a -> Set b -> Set (Map a b)
Map.enumerateMaps (c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
s o
a o
b) (c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
t (Map o o
appO Map o o -> o -> o
forall k v. Eq k => Map k v -> k -> v
|!| o
a) (Map o o
appO Map o o -> o -> o
forall k v. Eq k => Map k v -> k -> v
|!| o
b))
                    
    instance PrettyPrint (FinCat c m o) where
        pprint :: FinCat c m o -> String
pprint = FinCat c m o -> String
forall a. Show a => a -> String
show