{-| Module  : FiniteCategories
Description : Examples of  __'Ens'__.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of  __'Ens'__.
-}
module Math.FiniteCategories.Ens.Examples
(
    exampleEns,
    exampleEns2,
    exampleDiscreteDiagToSet,
    exampleProductSet,
    exampleCoproductSet,
    exampleParallelDiagramToSet,
    exampleEqualizerSet,
    exampleCoequalizerSet,
    exampleDiagramVToFinSet,
    exampleLimitSet,
    exampleColimitSet,
    exampleExponentialObjectInSet,
)
where
    import Data.WeakSet         (powerSet, Set)
    import Data.WeakSet.Safe
    import Data.WeakMap
    
    import Math.FiniteCategories
    import Math.Categories
    import Math.IO.PrettyPrint
    import Math.FiniteCategory
    import Math.CompleteCategory
    import Math.CocompleteCategory
    import Math.CartesianClosedCategory
    
    -- | An example of 'Ens' containing all subsets of {'A', 'B', 'C'}.

    exampleEns :: Ens Char
    exampleEns :: Ens Char
exampleEns = Set (Set Char) -> Ens Char
forall a. Set (Set a) -> Ens a
ens(Set (Set Char) -> Ens Char)
-> ([Char] -> Set (Set Char)) -> [Char] -> Ens Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set Char -> Set (Set Char)
forall a. Set a -> Set (Set a)
powerSet(Set Char -> Set (Set Char))
-> ([Char] -> Set Char) -> [Char] -> Set (Set Char)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[Char] -> Set Char
forall a. [a] -> Set a
set ([Char] -> Ens Char) -> [Char] -> Ens Char
forall a b. (a -> b) -> a -> b
$ [Char]
"ABC"
    
    -- | An example of 'Ens' containing sets {{},{'A'},{'A','B'},{'A','B','C'}}.

    exampleEns2 :: Ens Char
    exampleEns2 :: Ens Char
exampleEns2 = Set (Set Char) -> Ens Char
forall a. Set (Set a) -> Ens a
ens(Set (Set Char) -> Ens Char)
-> ([Set Char] -> Set (Set Char)) -> [Set Char] -> Ens Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[Set Char] -> Set (Set Char)
forall a. [a] -> Set a
set ([Set Char] -> Ens Char) -> [Set Char] -> Ens Char
forall a b. (a -> b) -> a -> b
$ [[Char] -> Set Char
forall a. [a] -> Set a
set [Char]
"", [Char] -> Set Char
forall a. [a] -> Set a
set [Char]
"A", [Char] -> Set Char
forall a. [a] -> Set a
set [Char]
"AB", [Char] -> Set Char
forall a. [a] -> Set a
set [Char]
"ABC"]
    
    -- | An example of 'discreteDiagram' to 'FinSet'.

    exampleDiscreteDiagToSet :: Diagram (DiscreteCategory Char) (DiscreteMorphism Char) Char (FinSet Int) (Function Int) (Set Int)
    exampleDiscreteDiagToSet :: Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleDiscreteDiagToSet = Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
-> Diagram
     (DiscreteCategory Char)
     (DiscreteMorphism Char)
     Char
     (FinSet Int)
     (Function Int)
     (Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: DiscreteCategory Char
src=Set Char -> DiscreteCategory Char
forall a. Set a -> DiscreteCategory a
discreteCategory ([Char] -> Set Char
forall a. [a] -> Set a
set [Char
'a',Char
'b']), tgt :: FinSet Int
tgt=FinSet Int
forall a. FinSet a
FinSet, omap :: Map Char (Set Int)
omap= (AssociationList Char (Set Int) -> Map Char (Set Int)
forall k v. AssociationList k v -> Map k v
weakMap [(Char
'a',[Int] -> Set Int
forall a. [a] -> Set a
set [Int
1,Int
2]),(Char
'b',[Int] -> Set Int
forall a. [a] -> Set a
set [Int
3,Int
4,Int
5])]), mmap :: Map (DiscreteMorphism Char) (Function Int)
mmap = AssociationList (DiscreteMorphism Char) (Function Int)
-> Map (DiscreteMorphism Char) (Function Int)
forall k v. AssociationList k v -> Map k v
weakMap []}

    -- | An example of product computed in 'FinSet' thanks to the fact that 'FinSet' is complete. Computes {1,2} x {3,4,5}.

    exampleProductSet :: Cone (DiscreteCategory Char) (DiscreteMorphism Char) Char (FinSet (Limit Char Int)) (Function (Limit Char Int)) (Set (Limit Char Int))
    exampleProductSet :: Cone
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet (Limit Char Int))
  (Function (Limit Char Int))
  (Set (Limit Char Int))
exampleProductSet = Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
-> Cone
     (DiscreteCategory Char)
     (DiscreteMorphism Char)
     Char
     (FinSet (Limit Char Int))
     (Function (Limit Char Int))
     (Set (Limit Char Int))
forall c m o cLim mLim oLim oIndex.
HasProducts c m o cLim mLim oLim oIndex =>
Diagram
  (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     cLim
     mLim
     oLim
Math.CompleteCategory.product Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleDiscreteDiagToSet
    
    -- | An example of coproduct computed in 'FinSet' thanks to the fact that 'FinSet' is cocomplete. Computes {1,2} + {3,4,5}.

    exampleCoproductSet :: Cocone (DiscreteCategory Char) (DiscreteMorphism Char) Char (FinSet (Colimit Char Int)) (Function (Colimit Char Int)) (Set (Colimit Char Int))
    exampleCoproductSet :: Cocone
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet (Colimit Char Int))
  (Function (Colimit Char Int))
  (Set (Colimit Char Int))
exampleCoproductSet = Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
-> Cocone
     (DiscreteCategory Char)
     (DiscreteMorphism Char)
     Char
     (FinSet (Colimit Char Int))
     (Function (Colimit Char Int))
     (Set (Colimit Char Int))
forall c m o cLim mLim oLim oIndex.
HasCoproducts c m o cLim mLim oLim oIndex =>
Diagram
  (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     cLim
     mLim
     oLim
coproduct Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleDiscreteDiagToSet
            
    -- | An example of 'parallelDiagram' to 'FinSet', the first function selected is x%2 on {0,1,2,3,4} and the second is (const 0).

    exampleParallelDiagramToSet :: Diagram Parallel ParallelAr ParallelOb (FinSet Int) (Function Int) (Set Int)
    exampleParallelDiagramToSet :: Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleParallelDiagramToSet = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinSet Int)
  (Function Int)
  (Set Int)
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (FinSet Int)
     (Function Int)
     (Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: Parallel
src = Parallel
Parallel, tgt :: FinSet Int
tgt = FinSet Int
forall a. FinSet a
FinSet, omap :: Map ParallelOb (Set Int)
omap = AssociationList ParallelOb (Set Int) -> Map ParallelOb (Set Int)
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map ParallelAr (Function Int)
mmap = AssociationList ParallelAr (Function Int)
-> Map ParallelAr (Function Int)
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelAr
ParallelF,Function{function :: Map Int Int
function = AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
0,Int
0),(Int
1,Int
1),(Int
2,Int
0),(Int
3,Int
1),(Int
4,Int
0)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
0,Int
1]}),(ParallelAr
ParallelG,Function{function :: Map Int Int
function = AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
0,Int
0),(Int
1,Int
0),(Int
2,Int
0),(Int
3,Int
0),(Int
4,Int
0)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
0,Int
1]})]}
    
    -- | An example of equalizer of a 'parallelDiagram' to 'FinSet' thanks to the fact that 'FinSet' is complete.

    --

    -- It equalizes 'exampleParallelDiagramToSet', therefore the apex of the equalizer is {0,2,4}.

    exampleEqualizerSet :: Cone Parallel ParallelAr ParallelOb (FinSet Int) (Function Int) (Set Int)
    exampleEqualizerSet :: Cone
  Parallel
  ParallelAr
  ParallelOb
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleEqualizerSet = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinSet Int)
  (Function Int)
  (Set Int)
-> Cone
     Parallel
     ParallelAr
     ParallelOb
     (FinSet Int)
     (Function Int)
     (Set Int)
forall c m o.
HasEqualizers c m o =>
Diagram Parallel ParallelAr ParallelOb c m o
-> Cone Parallel ParallelAr ParallelOb c m o
equalize Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleParallelDiagramToSet
    
    -- | An example of coequalizer of a 'parallelDiagram' to 'FinSet' thanks to the fact that 'FinSet' is cocomplete.

    --

    -- It equalizes 'exampleParallelDiagramToSet', therefore the nadir of the coequalizer is {0}.

    exampleCoequalizerSet :: Cocone Parallel ParallelAr ParallelOb (FinSet Int) (Function Int) (Set Int)
    exampleCoequalizerSet :: Cocone
  Parallel
  ParallelAr
  ParallelOb
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleCoequalizerSet = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinSet Int)
  (Function Int)
  (Set Int)
-> Cocone
     Parallel
     ParallelAr
     ParallelOb
     (FinSet Int)
     (Function Int)
     (Set Int)
forall c m o.
HasCoequalizers c m o =>
Diagram Parallel ParallelAr ParallelOb c m o
-> Cocone Parallel ParallelAr ParallelOb c m o
coequalize Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleParallelDiagramToSet
    
    
    -- | An example of a diagram from 'V' to 'FinSet'. The two functions selected are identities, the first from {1,2,3,4} to {1,2,3,4,5,6,7,8,9,10} and the second from {3,4,5,6} to {1,2,3,4,5,6,7,8,9,10}.

    exampleDiagramVToFinSet :: Diagram V VAr VOb (FinSet Int) (Function Int) (Set Int)
    exampleDiagramVToFinSet :: Diagram V VAr VOb (FinSet Int) (Function Int) (Set Int)
exampleDiagramVToFinSet = Diagram V VAr VOb (FinSet Int) (Function Int) (Set Int)
-> Diagram V VAr VOb (FinSet Int) (Function Int) (Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: V
src = V
V, tgt :: FinSet Int
tgt = FinSet Int
forall a. FinSet a
FinSet, omap :: Map VOb (Set Int)
omap = AssociationList VOb (Set Int) -> Map VOb (Set Int)
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map VAr (Function Int)
mmap = AssociationList VAr (Function Int) -> Map VAr (Function Int)
forall k v. AssociationList k v -> Map k v
weakMap [(VAr
VF,Function{function :: Map Int Int
function = AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
1,Int
1),(Int
2,Int
2),(Int
3,Int
3),(Int
4,Int
4)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1..Int
10]}),(VAr
VG,Function{function :: Map Int Int
function = AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
3,Int
3),(Int
4,Int
4),(Int
5,Int
5),(Int
6,Int
6)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1..Int
10]})]}
    
    -- | An example of limit computation of a 'Diagram' to 'FinSet' thanks to the fact that 'FinSet' is complete.

    exampleLimitSet :: Cone V VAr VOb (FinSet (Limit VOb Int)) (Function (Limit VOb Int)) (Set (Limit VOb Int))
    exampleLimitSet :: Cone
  V
  VAr
  VOb
  (FinSet (Limit VOb Int))
  (Function (Limit VOb Int))
  (Set (Limit VOb Int))
exampleLimitSet = Diagram V VAr VOb (FinSet Int) (Function Int) (Set Int)
-> Cone
     V
     VAr
     VOb
     (FinSet (Limit VOb Int))
     (Function (Limit VOb Int))
     (Set (Limit VOb Int))
forall c m o cLim mLim oLim cIndex mIndex oIndex.
(CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex,
 FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex c m o
-> Cone cIndex mIndex oIndex cLim mLim oLim
limit Diagram V VAr VOb (FinSet Int) (Function Int) (Set Int)
exampleDiagramVToFinSet
    
    
    
    -- | An example of a diagram from 'Hat' to 'FinSet'. The two functions selected are identities, the first from {3,4} to {1,2,3,4} and the second from {3,4} to {3,4,5,6}.

    exampleDiagramHatToFinSet :: Diagram Hat HatAr HatOb (FinSet Int) (Function Int) (Set Int)
    exampleDiagramHatToFinSet :: Diagram Hat HatAr HatOb (FinSet Int) (Function Int) (Set Int)
exampleDiagramHatToFinSet = Diagram Hat HatAr HatOb (FinSet Int) (Function Int) (Set Int)
-> Diagram Hat HatAr HatOb (FinSet Int) (Function Int) (Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: Hat
src = Hat
Hat, tgt :: FinSet Int
tgt = FinSet Int
forall a. FinSet a
FinSet, omap :: Map HatOb (Set Int)
omap = AssociationList HatOb (Set Int) -> Map HatOb (Set Int)
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map HatAr (Function Int)
mmap = AssociationList HatAr (Function Int) -> Map HatAr (Function Int)
forall k v. AssociationList k v -> Map k v
weakMap [(HatAr
HatF,Function{function :: Map Int Int
function = AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
3,Int
3),(Int
4,Int
4)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1..Int
4]}),(HatAr
HatG,Function{function :: Map Int Int
function = AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
3,Int
3),(Int
4,Int
4)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
3..Int
6]})]}
    
    -- | An example of colimit computation of a 'Diagram' to 'FinSet' thanks to the fact that 'FinSet' is cocomplete.

    --

    -- It is the colimit of 'exampleDiagramHatToFinSet' which computes the union of {1,2,3,4} and {3,4,5,6} where 3 and 4 are identified.

    exampleColimitSet :: Cocone Hat HatAr HatOb (FinSet (Colimit HatOb Int)) (Function (Colimit HatOb Int)) (Set (Colimit HatOb Int))
    exampleColimitSet :: Cocone
  Hat
  HatAr
  HatOb
  (FinSet (Colimit HatOb Int))
  (Function (Colimit HatOb Int))
  (Set (Colimit HatOb Int))
exampleColimitSet = Diagram Hat HatAr HatOb (FinSet Int) (Function Int) (Set Int)
-> Cocone
     Hat
     HatAr
     HatOb
     (FinSet (Colimit HatOb Int))
     (Function (Colimit HatOb Int))
     (Set (Colimit HatOb Int))
forall c m o cLim mLim oLim cIndex mIndex oIndex.
(CocompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex,
 FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex c m o
-> Cocone cIndex mIndex oIndex cLim mLim oLim
colimit Diagram Hat HatAr HatOb (FinSet Int) (Function Int) (Set Int)
exampleDiagramHatToFinSet
    
    -- | An example of exponential object. Computes the internal hom of 'exampleDiscreteDiagToSet', meaning all functions from {1,2} to {3,4,5}.

    exampleExponentialObjectInSet :: Tripod (FinSet (Cartesian Int)) (Function (Cartesian Int)) (Set (Cartesian Int))
    exampleExponentialObjectInSet :: Tripod
  (FinSet (Cartesian Int))
  (Function (Cartesian Int))
  (Set (Cartesian Int))
exampleExponentialObjectInSet = TwoBase (FinSet Int) (Function Int) (Set Int)
-> Tripod
     (FinSet (Cartesian Int))
     (Function (Cartesian Int))
     (Set (Cartesian Int))
forall c m o cLim mLim oLim cLimExp mLimExp oLimExp.
(CartesianClosedCategory
   c m o cLim mLim oLim cLimExp mLimExp oLimExp,
 CompleteCategory
   c m o cLim mLim oLim DiscreteTwo DiscreteTwoOb DiscreteTwoOb) =>
TwoBase c m o -> Tripod cLimExp mLimExp oLimExp
internalHom (TwoBase (FinSet Int) (Function Int) (Set Int)
 -> Tripod
      (FinSet (Cartesian Int))
      (Function (Cartesian Int))
      (Set (Cartesian Int)))
-> TwoBase (FinSet Int) (Function Int) (Set Int)
-> Tripod
     (FinSet (Cartesian Int))
     (Function (Cartesian Int))
     (Set (Cartesian Int))
forall a b. (a -> b) -> a -> b
$ Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleDiscreteDiagToSet Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
-> Diagram
     DiscreteTwo
     DiscreteTwoOb
     DiscreteTwoOb
     (DiscreteCategory Char)
     (DiscreteMorphism Char)
     Char
-> TwoBase (FinSet Int) (Function Int) (Set Int)
forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, Category c2 m2 o2,
 Morphism m2 o2, Eq o2, Eq m2, Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
<-@<- (DiscreteCategory Char
-> Char
-> Char
-> Diagram
     DiscreteTwo
     DiscreteTwoOb
     DiscreteTwoOb
     (DiscreteCategory Char)
     (DiscreteMorphism Char)
     Char
forall t.
Eq t =>
DiscreteCategory t
-> t
-> t
-> Diagram
     DiscreteTwo
     DiscreteTwoOb
     DiscreteTwoOb
     (DiscreteCategory t)
     (DiscreteMorphism t)
     t
insertionDiscreteTwoInDiscreteCategory (Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
-> DiscreteCategory Char
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory Char)
  (DiscreteMorphism Char)
  Char
  (FinSet Int)
  (Function Int)
  (Set Int)
exampleDiscreteDiagToSet) Char
'a' Char
'b')