module Math.Functors.DiagonalFunctor.Examples
(
exampleDiagonalFunctor,
)
where
import Math.FiniteCategory
import Math.FiniteCategories
import Math.Categories
import Math.Functors.DiagonalFunctor
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
exampleDiagonalFunctor :: Diagram (Ens Int) (Function Int) (Set Int) (FunctorCategory (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (NaturalTransformation (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int)) (Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int (Ens Int) (Function Int) (Set Int))
exampleDiagonalFunctor :: Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
exampleDiagonalFunctor = DiscreteCategory Int
-> Ens Int
-> Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(Ens Int)
(Function Int)
(Set Int))
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
Morphism m2 o2) =>
c1
-> c2
-> Diagram
c2
m2
o2
(FunctorCategory c1 m1 o1 c2 m2 o2)
(NaturalTransformation c1 m1 o1 c2 m2 o2)
(Diagram c1 m1 o1 c2 m2 o2)
diagonalFunctor DiscreteCategory Int
indexing Ens Int
universe
where
universe :: Ens Int
universe = Set (Set Int) -> Ens Int
forall a. Set (Set a) -> Ens a
ens (Set (Set Int) -> Ens Int) -> Set (Set Int) -> Ens Int
forall a b. (a -> b) -> a -> b
$ [Set Int] -> Set (Set Int)
forall a. [a] -> Set a
set [[Int] -> Set Int
forall a. [a] -> Set a
set [Int
1], [Int] -> Set Int
forall a. [a] -> Set a
set [Int
3,Int
4]]
indexing :: DiscreteCategory Int
indexing = Set Int -> DiscreteCategory Int
forall a. Set a -> DiscreteCategory a
discreteCategory (Set Int -> DiscreteCategory Int)
-> Set Int -> DiscreteCategory Int
forall a b. (a -> b) -> a -> b
$ [Int] -> Set Int
forall a. [a] -> Set a
set [Int
0,Int
1]