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
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"
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"]
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 []}
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
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
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]})]}
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
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
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]})]}
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
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]})]}
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
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')