{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : The category of finite sets.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __FinSet__ category has as objects finite sets and as morphisms maps between them.
It is a full subcategory of the __Set__ category.
It is itself a large category (therefore not a finite one),
we only construct finite subcategories of the mathematical infinite __FinSet__ category.
`FinSet` is the type of full finite subcategories of __FinSet__.

To instantiate it, use the `FinSet` constructor on a list of sets.

For example, see Example.ExampleSet
-}

module Set.FinSet where
    import              Data.List                               (intersect, nub, intercalate, subsequences)
    import              Utils.SetList
    import              Utils.AssociationList
    import              FiniteCategory.FiniteCategory
    import              Utils.CartesianProduct                  ((|^|))
    import              IO.PrettyPrint
    
    import              Diagram.Diagram
    import              ConeCategory.ConeCategory
    import              UsualCategories.One
    
    -- | When constructing a set, the following rules should be respected :

    --

    -- - An elem is always a leaf construct.

    --

    -- - There should be no duplicate in a Collection.

    --

    -- - The root construct is always a Collection.

    --

    -- This set construction does not require the ord constraint.

    data FinSet a =   Elem a
                    | Collection [FinSet a]
                    deriving (Int -> FinSet a -> ShowS
[FinSet a] -> ShowS
FinSet a -> String
(Int -> FinSet a -> ShowS)
-> (FinSet a -> String) -> ([FinSet a] -> ShowS) -> Show (FinSet a)
forall a. Show a => Int -> FinSet a -> ShowS
forall a. Show a => [FinSet a] -> ShowS
forall a. Show a => FinSet a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FinSet a] -> ShowS
$cshowList :: forall a. Show a => [FinSet a] -> ShowS
show :: FinSet a -> String
$cshow :: forall a. Show a => FinSet a -> String
showsPrec :: Int -> FinSet a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FinSet a -> ShowS
Show)
    
    instance (Eq a) => Eq (FinSet a) where
        (Elem a
a) == :: FinSet a -> FinSet a -> Bool
== (Elem a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
        (Collection [FinSet a]
s1) == (Collection [FinSet a]
s2) = [FinSet a] -> [FinSet a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
doubleInclusion [FinSet a]
s1 [FinSet a]
s2
        FinSet a
_ == FinSet a
_ = Bool
False
    
    instance Functor FinSet where
        fmap :: forall a b. (a -> b) -> FinSet a -> FinSet b
fmap a -> b
f (Elem a
a) = b -> FinSet b
forall a. a -> FinSet a
Elem (a -> b
f a
a)
        fmap a -> b
f (Collection [FinSet a]
xs) = [FinSet b] -> FinSet b
forall a. [FinSet a] -> FinSet a
Collection ((a -> b) -> FinSet a -> FinSet b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (FinSet a -> FinSet b) -> [FinSet a] -> [FinSet b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinSet a]
xs)
    
    -- | Constructs the empty set.

    emptyFinSet :: FinSet a
    emptyFinSet :: forall a. FinSet a
emptyFinSet = [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection []
    
    -- | Constructs a singleton set.

    singleton :: a -> FinSet a
    singleton :: forall a. a -> FinSet a
singleton a
x = [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection [a -> FinSet a
forall a. a -> FinSet a
Elem a
x]
    
    -- | Extract a list from a set.

    toList :: FinSet a -> [FinSet a]
    toList :: forall a. FinSet a -> [FinSet a]
toList (Collection [FinSet a]
list) = [FinSet a]
list
    
    -- | Transforms a list of sets into a set.

    fromList :: (Eq a) => [FinSet a] -> FinSet a
    fromList :: forall a. Eq a => [FinSet a] -> FinSet a
fromList [FinSet a]
xs = [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection ([FinSet a] -> FinSet a) -> [FinSet a] -> FinSet a
forall a b. (a -> b) -> a -> b
$ [FinSet a] -> [FinSet a]
forall a. Eq a => [a] -> [a]
nub [FinSet a]
xs
    
    -- | Union of two sets.

    (|||) :: (Eq a) => FinSet a -> FinSet a -> FinSet a
    ||| :: forall a. Eq a => FinSet a -> FinSet a -> FinSet a
(|||) (Collection [FinSet a]
l1) (Collection [FinSet a]
l2) = [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection ([FinSet a] -> FinSet a) -> [FinSet a] -> FinSet a
forall a b. (a -> b) -> a -> b
$ [FinSet a] -> [FinSet a]
forall a. Eq a => [a] -> [a]
nub ([FinSet a]
l1[FinSet a] -> [FinSet a] -> [FinSet a]
forall a. [a] -> [a] -> [a]
++[FinSet a]
l2)
    
    -- | Union of a list of sets.

    union :: (Eq a) => [FinSet a] -> FinSet a
    union :: forall a. Eq a => [FinSet a] -> FinSet a
union [FinSet a]
sets = (FinSet a -> FinSet a -> FinSet a)
-> FinSet a -> [FinSet a] -> FinSet a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr FinSet a -> FinSet a -> FinSet a
forall a. Eq a => FinSet a -> FinSet a -> FinSet a
(|||) FinSet a
forall a. FinSet a
emptyFinSet [FinSet a]
sets
    
    -- | Intersection of two sets.

    (&&&) :: (Eq a) => FinSet a -> FinSet a -> FinSet a
    &&& :: forall a. Eq a => FinSet a -> FinSet a -> FinSet a
(&&&) (Collection [FinSet a]
l1) (Collection [FinSet a]
l2) = [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection ([FinSet a] -> FinSet a) -> [FinSet a] -> FinSet a
forall a b. (a -> b) -> a -> b
$ [FinSet a] -> [FinSet a] -> [FinSet a]
forall a. Eq a => [a] -> [a] -> [a]
intersect [FinSet a]
l1 [FinSet a]
l2
    
    -- | Intersection of a list of sets.

    intersection :: (Eq a) => [FinSet a] -> FinSet a
    intersection :: forall a. Eq a => [FinSet a] -> FinSet a
intersection [] = String -> FinSet a
forall a. HasCallStack => String -> a
error String
"Cannot make an intersection of no set."
    intersection [FinSet a]
sets = (FinSet a -> FinSet a -> FinSet a) -> [FinSet a] -> FinSet a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 FinSet a -> FinSet a -> FinSet a
forall a. Eq a => FinSet a -> FinSet a -> FinSet a
(&&&) [FinSet a]
sets
    
    -- | Returns wether a set is in another one.

    isIn :: (Eq a) => FinSet a -> FinSet a -> Bool
    isIn :: forall a. Eq a => FinSet a -> FinSet a -> Bool
isIn FinSet a
e (Collection [FinSet a]
es) = FinSet a -> [FinSet a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FinSet a
e [FinSet a]
es
    
    -- | Returns wether a set is included in another one.

    includedIn :: (Eq a) => FinSet a -> FinSet a -> Bool
    includedIn :: forall a. Eq a => FinSet a -> FinSet a -> Bool
includedIn (Collection [FinSet a]
l1) (Collection [FinSet a]
l2) = [FinSet a] -> [FinSet a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isIncludedIn [FinSet a]
l1 [FinSet a]
l2
    
    -- | Returns the size of a set.

    card :: FinSet a -> Int
    card :: forall a. FinSet a -> Int
card (Collection [FinSet a]
xs) = [FinSet a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FinSet a]
xs
    
    -- | Generalizes a set of @a@ so that it can contain elements of type @a@ or @b@. 

    generalizeType :: FinSet a -> FinSet (Either a b)
    generalizeType :: forall a b. FinSet a -> FinSet (Either a b)
generalizeType = (a -> Either a b) -> FinSet a -> FinSet (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a b
forall a b. a -> Either a b
Left
    
    instance (PrettyPrintable a) => PrettyPrintable (FinSet a) where
        pprint :: FinSet a -> String
pprint (Elem a
a) = a -> String
forall a. PrettyPrintable a => a -> String
pprint a
a
        pprint (Collection [FinSet a]
elems) = String
"{"String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," (FinSet a -> String
forall a. PrettyPrintable a => a -> String
pprint (FinSet a -> String) -> [FinSet a] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinSet a]
elems)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
    
    -- | `FinMap` is the morphism of the `FinSetCat` category.

    --

    -- We need to keep the codomain because it would not be present in a non-surjective map.

    --

    -- It is represented by an association list and a codomain.

    data FinMap a = FinMap {  forall a. FinMap a -> AssociationList (FinSet a) (FinSet a)
finMap :: (AssociationList (FinSet a) (FinSet a))
                            , forall a. FinMap a -> FinSet a
codomain :: (FinSet a)
                           }
                           deriving (FinMap a -> FinMap a -> Bool
(FinMap a -> FinMap a -> Bool)
-> (FinMap a -> FinMap a -> Bool) -> Eq (FinMap a)
forall a. Eq a => FinMap a -> FinMap a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FinMap a -> FinMap a -> Bool
$c/= :: forall a. Eq a => FinMap a -> FinMap a -> Bool
== :: FinMap a -> FinMap a -> Bool
$c== :: forall a. Eq a => FinMap a -> FinMap a -> Bool
Eq, Int -> FinMap a -> ShowS
[FinMap a] -> ShowS
FinMap a -> String
(Int -> FinMap a -> ShowS)
-> (FinMap a -> String) -> ([FinMap a] -> ShowS) -> Show (FinMap a)
forall a. Show a => Int -> FinMap a -> ShowS
forall a. Show a => [FinMap a] -> ShowS
forall a. Show a => FinMap a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FinMap a] -> ShowS
$cshowList :: forall a. Show a => [FinMap a] -> ShowS
show :: FinMap a -> String
$cshow :: forall a. Show a => FinMap a -> String
showsPrec :: Int -> FinMap a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FinMap a -> ShowS
Show)
    
    instance (Eq a) => Morphism (FinMap a) (FinSet a) where
        @ :: FinMap a -> FinMap a -> FinMap a
(@) FinMap a
g FinMap a
f = FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap {    finMap :: AssociationList (FinSet a) (FinSet a)
finMap = [(FinSet a
k,((FinMap a -> AssociationList (FinSet a) (FinSet a)
forall a. FinMap a -> AssociationList (FinSet a) (FinSet a)
finMap FinMap a
g) AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinSet a
forall a b. Eq a => AssociationList a b -> a -> b
!-! FinSet a
v)) | (FinSet a
k,FinSet a
v) <- (FinMap a -> AssociationList (FinSet a) (FinSet a)
forall a. FinMap a -> AssociationList (FinSet a) (FinSet a)
finMap FinMap a
f)]
                            , codomain :: FinSet a
codomain = (FinMap a -> FinSet a
forall a. FinMap a -> FinSet a
codomain FinMap a
g)
                         }
        source :: FinMap a -> FinSet a
source FinMap a
m = [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection ([FinSet a] -> FinSet a) -> [FinSet a] -> FinSet a
forall a b. (a -> b) -> a -> b
$ [FinSet a] -> [FinSet a]
forall a. Eq a => [a] -> [a]
nub (AssociationList (FinSet a) (FinSet a) -> [FinSet a]
forall a b. AssociationList a b -> [a]
keys (FinMap a -> AssociationList (FinSet a) (FinSet a)
forall a. FinMap a -> AssociationList (FinSet a) (FinSet a)
finMap FinMap a
m))
        target :: FinMap a -> FinSet a
target = FinMap a -> FinSet a
forall a. FinMap a -> FinSet a
codomain
        
    instance (PrettyPrintable a, Eq a) => PrettyPrintable (FinMap a) where
        pprint :: FinMap a -> String
pprint FinMap a
f = FinSet a -> String
forall a. PrettyPrintable a => a -> String
pprint (FinMap a -> FinSet a
forall m o. Morphism m o => m -> o
source FinMap a
f) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FinSet a -> String
forall a. PrettyPrintable a => a -> String
pprint (FinMap a -> FinSet a
forall m o. Morphism m o => m -> o
target FinMap a
f) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ AssociationList (FinSet a) (FinSet a) -> String
forall a. PrettyPrintable a => a -> String
pprint (FinMap a -> AssociationList (FinSet a) (FinSet a)
forall a. FinMap a -> AssociationList (FinSet a) (FinSet a)
finMap FinMap a
f)
    
    -- | `FinSetCat` is the type for the category of `FinSet`.

    -- Its elements are the sets considered in the Set category.

    data FinSetCat a = FinSetCat [FinSet a] deriving (FinSetCat a -> FinSetCat a -> Bool
(FinSetCat a -> FinSetCat a -> Bool)
-> (FinSetCat a -> FinSetCat a -> Bool) -> Eq (FinSetCat a)
forall a. Eq a => FinSetCat a -> FinSetCat a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FinSetCat a -> FinSetCat a -> Bool
$c/= :: forall a. Eq a => FinSetCat a -> FinSetCat a -> Bool
== :: FinSetCat a -> FinSetCat a -> Bool
$c== :: forall a. Eq a => FinSetCat a -> FinSetCat a -> Bool
Eq, Int -> FinSetCat a -> ShowS
[FinSetCat a] -> ShowS
FinSetCat a -> String
(Int -> FinSetCat a -> ShowS)
-> (FinSetCat a -> String)
-> ([FinSetCat a] -> ShowS)
-> Show (FinSetCat a)
forall a. Show a => Int -> FinSetCat a -> ShowS
forall a. Show a => [FinSetCat a] -> ShowS
forall a. Show a => FinSetCat a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FinSetCat a] -> ShowS
$cshowList :: forall a. Show a => [FinSetCat a] -> ShowS
show :: FinSetCat a -> String
$cshow :: forall a. Show a => FinSetCat a -> String
showsPrec :: Int -> FinSetCat a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FinSetCat a -> ShowS
Show)
 
    instance (Eq a) => FiniteCategory (FinSetCat a) (FinMap a) (FinSet a) where
        ob :: FinSetCat a -> [FinSet a]
ob (FinSetCat [FinSet a]
xs) = [FinSet a]
xs
        identity :: Morphism (FinMap a) (FinSet a) =>
FinSetCat a -> FinSet a -> FinMap a
identity FinSetCat a
c FinSet a
s
            | FinSet a -> [FinSet a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FinSet a
s (FinSetCat a -> [FinSet a]
forall c m o. FiniteCategory c m o => c -> [o]
ob FinSetCat a
c) = FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap{ finMap :: AssociationList (FinSet a) (FinSet a)
finMap = [(FinSet a
e,FinSet a
e) | FinSet a
e <- FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList FinSet a
s]
                                    , codomain :: FinSet a
codomain = FinSet a
s
                                    }
            | Bool
otherwise = String -> FinMap a
forall a. HasCallStack => String -> a
error(String
"Trying to get identity of an object not in the Set category.")
        ar :: Morphism (FinMap a) (FinSet a) =>
FinSetCat a -> FinSet a -> FinSet a -> [FinMap a]
ar FinSetCat a
_ FinSet a
s FinSet a
t
            | FinSet a
s FinSet a -> FinSet a -> Bool
forall a. Eq a => a -> a -> Bool
== FinSet a
forall a. FinSet a
emptyFinSet = [FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap{finMap :: AssociationList (FinSet a) (FinSet a)
finMap=[],codomain :: FinSet a
codomain=FinSet a
t}]
            | FinSet a
t FinSet a -> FinSet a -> Bool
forall a. Eq a => a -> a -> Bool
== FinSet a
forall a. FinSet a
emptyFinSet = []
            | Bool
otherwise = (\AssociationList (FinSet a) (FinSet a)
x -> FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap {codomain :: FinSet a
codomain=FinSet a
t, finMap :: AssociationList (FinSet a) (FinSet a)
finMap=AssociationList (FinSet a) (FinSet a)
x}) (AssociationList (FinSet a) (FinSet a) -> FinMap a)
-> [AssociationList (FinSet a) (FinSet a)] -> [FinMap a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[FinSet a] -> [FinSet a] -> AssociationList (FinSet a) (FinSet a)
forall a b. [a] -> [b] -> [(a, b)]
zip [FinSet a]
domain [FinSet a]
i | [FinSet a]
i <- [[FinSet a]]
images] where
                domain :: [FinSet a]
domain = FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList FinSet a
s
                codomain :: [FinSet a]
codomain = FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList FinSet a
t
                images :: [[FinSet a]]
images = ([FinSet a]
codomain [FinSet a] -> Int -> [[FinSet a]]
forall {a}. [a] -> Int -> [[a]]
|^| ([FinSet a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FinSet a]
domain))
          
    instance (Eq a) => GeneratedFiniteCategory (FinSetCat a) (FinMap a) (FinSet a) where
        genAr :: Morphism (FinMap a) (FinSet a) =>
FinSetCat a -> FinSet a -> FinSet a -> [FinMap a]
genAr FinSetCat a
_ FinSet a
s FinSet a
t
            | FinSet a
s FinSet a -> FinSet a -> Bool
forall a. Eq a => a -> a -> Bool
== FinSet a
forall a. FinSet a
emptyFinSet = [FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap{finMap :: AssociationList (FinSet a) (FinSet a)
finMap=[],codomain :: FinSet a
codomain=FinSet a
t}]
            | FinSet a
t FinSet a -> FinSet a -> Bool
forall a. Eq a => a -> a -> Bool
== FinSet a
forall a. FinSet a
emptyFinSet = []
            | FinSet a -> Int
forall a. FinSet a -> Int
card FinSet a
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = [FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap {codomain :: FinSet a
codomain=FinSet a
t, finMap :: AssociationList (FinSet a) (FinSet a)
finMap=AssociationList (FinSet a) (FinSet a)
injectiv}] 
            | FinSet a -> Int
forall a. FinSet a -> Int
card FinSet a
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = [FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap {codomain :: FinSet a
codomain=FinSet a
t, finMap :: AssociationList (FinSet a) (FinSet a)
finMap=AssociationList (FinSet a) (FinSet a)
surjectiv}]
            | FinSet a
s FinSet a -> FinSet a -> Bool
forall a. Eq a => a -> a -> Bool
== FinSet a
t = [FinMap a] -> [FinMap a]
forall a. Eq a => [a] -> [a]
nub ([FinMap a] -> [FinMap a]) -> [FinMap a] -> [FinMap a]
forall a b. (a -> b) -> a -> b
$ (\AssociationList (FinSet a) (FinSet a)
m -> FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap {codomain :: FinSet a
codomain=FinSet a
t, finMap :: AssociationList (FinSet a) (FinSet a)
finMap=AssociationList (FinSet a) (FinSet a)
m}) (AssociationList (FinSet a) (FinSet a) -> FinMap a)
-> [AssociationList (FinSet a) (FinSet a)] -> [FinMap a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AssociationList (FinSet a) (FinSet a)
transpose,AssociationList (FinSet a) (FinSet a)
rotate,AssociationList (FinSet a) (FinSet a)
project]           
            | FinSet a -> Int
forall a. FinSet a -> Int
card FinSet a
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< FinSet a -> Int
forall a. FinSet a -> Int
card FinSet a
t = [FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap {codomain :: FinSet a
codomain=FinSet a
t, finMap :: AssociationList (FinSet a) (FinSet a)
finMap=AssociationList (FinSet a) (FinSet a)
injectiv}] 
            | Bool
otherwise = [FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap {codomain :: FinSet a
codomain=FinSet a
t, finMap :: AssociationList (FinSet a) (FinSet a)
finMap=AssociationList (FinSet a) (FinSet a)
surjectiv}]  
            where
            domain :: [FinSet a]
domain = FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList FinSet a
s
            codomain :: [FinSet a]
codomain = FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList FinSet a
t
            transpose :: AssociationList (FinSet a) (FinSet a)
transpose = [([FinSet a]
domain [FinSet a] -> Int -> FinSet a
forall a. [a] -> Int -> a
!! Int
0, [FinSet a]
domain [FinSet a] -> Int -> FinSet a
forall a. [a] -> Int -> a
!! Int
1),([FinSet a]
domain [FinSet a] -> Int -> FinSet a
forall a. [a] -> Int -> a
!! Int
1, [FinSet a]
domain [FinSet a] -> Int -> FinSet a
forall a. [a] -> Int -> a
!! Int
0)]AssociationList (FinSet a) (FinSet a)
-> AssociationList (FinSet a) (FinSet a)
-> AssociationList (FinSet a) (FinSet a)
forall a. [a] -> [a] -> [a]
++[(FinSet a
o,FinSet a
o) | FinSet a
o <- Int -> [FinSet a] -> [FinSet a]
forall a. Int -> [a] -> [a]
drop Int
2 [FinSet a]
domain]
            rotatedDomain :: [FinSet a]
rotatedDomain = ([FinSet a] -> [FinSet a]
forall a. [a] -> [a]
tail [FinSet a]
domain) [FinSet a] -> [FinSet a] -> [FinSet a]
forall a. [a] -> [a] -> [a]
++ [([FinSet a] -> FinSet a
forall a. [a] -> a
head [FinSet a]
domain)]
            rotate :: AssociationList (FinSet a) (FinSet a)
rotate = [FinSet a] -> [FinSet a] -> AssociationList (FinSet a) (FinSet a)
forall a b. [a] -> [b] -> [(a, b)]
zip [FinSet a]
domain [FinSet a]
rotatedDomain             
            project :: AssociationList (FinSet a) (FinSet a)
project = ([FinSet a]
domain [FinSet a] -> Int -> FinSet a
forall a. [a] -> Int -> a
!! Int
0, [FinSet a]
domain [FinSet a] -> Int -> FinSet a
forall a. [a] -> Int -> a
!! Int
1)(FinSet a, FinSet a)
-> AssociationList (FinSet a) (FinSet a)
-> AssociationList (FinSet a) (FinSet a)
forall a. a -> [a] -> [a]
:[(FinSet a
o,FinSet a
o) | FinSet a
o <- [FinSet a] -> [FinSet a]
forall a. [a] -> [a]
tail [FinSet a]
domain]
            injectiv :: AssociationList (FinSet a) (FinSet a)
injectiv = [FinSet a] -> [FinSet a] -> AssociationList (FinSet a) (FinSet a)
forall a b. [a] -> [b] -> [(a, b)]
zip [FinSet a]
domain [FinSet a]
codomain
            surjectiv :: AssociationList (FinSet a) (FinSet a)
surjectiv = [FinSet a] -> [FinSet a] -> AssociationList (FinSet a) (FinSet a)
forall a b. [a] -> [b] -> [(a, b)]
zip [FinSet a]
domain ((Int -> FinSet a -> [FinSet a]
forall a. Int -> a -> [a]
replicate ((FinSet a -> Int
forall a. FinSet a -> Int
card FinSet a
s)Int -> Int -> Int
forall a. Num a => a -> a -> a
-(FinSet a -> Int
forall a. FinSet a -> Int
card FinSet a
t)Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([FinSet a] -> FinSet a
forall a. [a] -> a
head [FinSet a]
codomain))[FinSet a] -> [FinSet a] -> [FinSet a]
forall a. [a] -> [a] -> [a]
++[FinSet a]
codomain)
        
        decompose :: Morphism (FinMap a) (FinSet a) =>
FinSetCat a -> FinMap a -> [FinMap a]
decompose = FinSetCat a -> FinMap a -> [FinMap a]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [m]
bruteForceDecompose

    instance (PrettyPrintable a) => PrettyPrintable (FinSetCat a) where
        pprint :: FinSetCat a -> String
pprint (FinSetCat [FinSet a]
xs) = String
"FinSetCat "String -> ShowS
forall a. [a] -> [a] -> [a]
++([FinSet a] -> String
forall a. PrettyPrintable a => a -> String
pprint [FinSet a]
xs)

    -- | Returns the `FinSet` category such that every subset of the set given is an object of the category.

    powerFinSet :: FinSet a -> FinSet a
    powerFinSet :: forall a. FinSet a -> FinSet a
powerFinSet (Collection [FinSet a]
xs) = [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection ([FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection ([FinSet a] -> FinSet a) -> [[FinSet a]] -> [FinSet a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinSet a] -> [[FinSet a]]
forall a. [a] -> [[a]]
subsequences [FinSet a]
xs)
                    
    -- | Add a set to the target FinSetCat such that the given diagram has a limit. The diagram must not be the empty diagram from @0@ to @0@.

    --

    -- Returns an insertion functor from the previous set category to the new one, an updated diagram which has a limit, and the new limit object.

    constructLimit :: (FiniteCategory c m o, Morphism m o, Eq a, Eq c, Eq m, Eq o) => Diagram c m o (FinSetCat a) (FinMap a) (FinSet a) -> (Diagram (FinSetCat a) (FinMap a) (FinSet a) (FinSetCat a) (FinMap a) (FinSet a), Diagram c m o (FinSetCat a) (FinMap a) (FinSet a), (FinSet a))
    constructLimit :: forall c m o a.
(FiniteCategory c m o, Morphism m o, Eq a, Eq c, Eq m, Eq o) =>
Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
-> (Diagram
      (FinSetCat a)
      (FinMap a)
      (FinSet a)
      (FinSetCat a)
      (FinMap a)
      (FinSet a),
    Diagram c m o (FinSetCat a) (FinMap a) (FinSet a), FinSet a)
constructLimit Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
diag = (Diagram
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
insertionFunctor, Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
newDiagram, FinSet a
newLimitObject)
        where
            cat :: FinSetCat a
cat@(FinSetCat [FinSet a]
sets) = Diagram c m o (FinSetCat a) (FinMap a) (FinSet a) -> FinSetCat a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
diag
            singletonAlreadyHere :: Bool
singletonAlreadyHere = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (\FinSet a
s -> FinSet a -> Int
forall a. FinSet a -> Int
card FinSet a
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (FinSet a -> Bool) -> [FinSet a] -> [Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinSet a]
sets
            singleton2 :: FinSet a
singleton2 = if Bool
singletonAlreadyHere 
                            then    
                                [FinSet a] -> FinSet a
forall a. [a] -> a
head [FinSet a
s | FinSet a
s <- [FinSet a]
sets, FinSet a -> Int
forall a. FinSet a -> Int
card FinSet a
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1] 
                            else
                                [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection [[FinSet a] -> FinSet a
forall a. [a] -> a
head [FinSet a]
sets] -- we make a singleton out of the first set

            newSetCat :: FinSetCat a
newSetCat = if Bool
singletonAlreadyHere
                            then
                                FinSetCat a
cat
                            else
                                [FinSet a] -> FinSetCat a
forall a. [FinSet a] -> FinSetCat a
FinSetCat (FinSet a
singleton2FinSet a -> [FinSet a] -> [FinSet a]
forall a. a -> [a] -> [a]
:[FinSet a]
sets)
            newDiag :: Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
newDiag = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: c
src = Diagram c m o (FinSetCat a) (FinMap a) (FinSet a) -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
diag, tgt :: FinSetCat a
tgt = FinSetCat a
newSetCat, omap :: AssociationList o (FinSet a)
omap = Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
-> AssociationList o (FinSet a)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
diag, mmap :: AssociationList m (FinMap a)
mmap = Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
-> AssociationList m (FinMap a)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
diag}
            newLimitObject :: FinSet a
newLimitObject = [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection ([FinSet a] -> FinSet a) -> [FinSet a] -> FinSet a
forall a b. (a -> b) -> a -> b
$ [((FinSet a -> FinSet a) -> FinSet a -> [FinSet a]
forall a. (a -> a) -> a -> [a]
iterate (\FinSet a
x -> [FinSet a] -> FinSet a
forall a. [FinSet a] -> FinSet a
Collection [FinSet a
x]) FinSet a
singleton2) [FinSet a] -> Int -> FinSet a
forall a. [a] -> Int -> a
!! Int
i | Int
i <- [Int
1..([Cone c m o (FinSetCat a) (FinMap a) (FinSet a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
-> FinSet a -> [Cone c m o (FinSetCat a) (FinMap a) (FinSet a)]
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> o2 -> [Cone c1 m1 o1 c2 m2 o2]
conesOfApex Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
newDiag FinSet a
singleton2))]]
            newTargetCat :: FinSetCat a
newTargetCat = [FinSet a] -> FinSetCat a
forall a. [FinSet a] -> FinSetCat a
FinSetCat (FinSet a
newLimitObjectFinSet a -> [FinSet a] -> [FinSet a]
forall a. a -> [a] -> [a]
:[FinSet a]
sets)
            insertionFunctor :: Diagram
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
insertionFunctor = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: FinSetCat a
src = FinSetCat a
cat, tgt :: FinSetCat a
tgt = FinSetCat a
newTargetCat, omap :: AssociationList (FinSet a) (FinSet a)
omap = (FinSet a -> FinSet a)
-> [FinSet a] -> AssociationList (FinSet a) (FinSet a)
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList FinSet a -> FinSet a
forall a. a -> a
id (FinSetCat a -> [FinSet a]
forall c m o. FiniteCategory c m o => c -> [o]
ob FinSetCat a
cat)
                , mmap :: AssociationList (FinMap a) (FinMap a)
mmap = (FinMap a -> FinMap a)
-> [FinMap a] -> AssociationList (FinMap a) (FinMap a)
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList FinMap a -> FinMap a
forall a. a -> a
id (FinSetCat a -> [FinMap a]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows FinSetCat a
cat)}
            newDiagram :: Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
newDiagram = Diagram
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
insertionFunctor Diagram
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
-> Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
-> Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, FiniteCategory c3 m3 o3, Morphism m3 o3, Eq m1,
 Eq o1, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
`composeDiag` Diagram c m o (FinSetCat a) (FinMap a) (FinSet a)
diag
                
    -- | Generalizes a set category of @a@ so that it can contain elements of type @a@ or @b@. 

    generalizeTypeSetCat :: FinSetCat a -> FinSetCat (Either a b)
    generalizeTypeSetCat :: forall a b. FinSetCat a -> FinSetCat (Either a b)
generalizeTypeSetCat (FinSetCat [FinSet a]
xs) = [FinSet (Either a b)] -> FinSetCat (Either a b)
forall a. [FinSet a] -> FinSetCat a
FinSetCat ([FinSet (Either a b)] -> FinSetCat (Either a b))
-> [FinSet (Either a b)] -> FinSetCat (Either a b)
forall a b. (a -> b) -> a -> b
$ ((a -> Either a b) -> FinSet a -> FinSet (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a b
forall a b. a -> Either a b
Left) (FinSet a -> FinSet (Either a b))
-> [FinSet a] -> [FinSet (Either a b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FinSet a]
xs