module Math.FiniteCategories.FunctorCategory.Example
(
main
)
where
import Data.WeakSet.Safe
import Data.WeakMap.Safe
import Math.FiniteCategory
import Math.Categories
import Math.FiniteCategories
import Math.IO.PrettyPrint
import Numeric.Natural
main :: IO ()
main :: IO ()
main = do
String -> IO ()
putStrLn String
"Start of Math.FiniteCategories.FunctorCategory.Example"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ FunctorCategory
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String
forall c m o.
(FiniteCategory c m o, Morphism m o, PrettyPrint c, PrettyPrint m,
PrettyPrint o, Eq m, Eq o) =>
c -> String
pprintFiniteCategory (NumberCategory
-> NumberCategory
-> FunctorCategory
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Natural -> NumberCategory
numberCategory Natural
2) (Natural -> NumberCategory
numberCategory Natural
3))
[IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([IO ()] -> IO [()]) -> [IO ()] -> IO [()]
forall a b. (a -> b) -> a -> b
$ (String -> IO ()
putStrLn(String -> IO ())
-> (Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String)
-> Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint) (Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ())
-> [Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
-> [IO ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set
(Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
-> [Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
forall a. Eq a => Set a -> [a]
setToList (FunctorCategory
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> Set
(Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
forall c m o. FiniteCategory c m o => c -> Set o
ob (NumberCategory
-> NumberCategory
-> FunctorCategory
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Natural -> NumberCategory
numberCategory Natural
2) (Natural -> NumberCategory
numberCategory Natural
3))))
[IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([IO ()] -> IO [()]) -> [IO ()] -> IO [()]
forall a b. (a -> b) -> a -> b
$ (String -> IO ()
putStrLn(String -> IO ())
-> (Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String)
-> Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint) (Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ())
-> [Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
-> [IO ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set
(Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
-> [Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
forall a. Eq a => Set a -> [a]
setToList (FunctorCategory
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> Set
(Diagram
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
forall c m o. FiniteCategory c m o => c -> Set o
ob (NumberCategory
-> NumberCategory
-> FunctorCategory
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Natural -> NumberCategory
numberCategory Natural
2) (Natural -> NumberCategory
numberCategory Natural
3))))
[IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([IO ()] -> IO [()]) -> [IO ()] -> IO [()]
forall a b. (a -> b) -> a -> b
$ (String -> IO ()
putStrLn(String -> IO ())
-> (NaturalTransformation
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String)
-> NaturalTransformation
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint) (NaturalTransformation
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ())
-> [NaturalTransformation
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
-> [IO ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set
(NaturalTransformation
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
-> [NaturalTransformation
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
forall a. Eq a => Set a -> [a]
setToList (FunctorCategory
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> Set
(NaturalTransformation
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (NumberCategory
-> NumberCategory
-> FunctorCategory
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Natural -> NumberCategory
numberCategory Natural
2) (Natural -> NumberCategory
numberCategory Natural
3))))
let diag :: Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
diag = Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
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 Natural
src=Set Natural -> DiscreteCategory Natural
forall a. Set a -> DiscreteCategory a
discreteCategory ([Natural] -> Set Natural
forall a. [a] -> Set a
set [Natural
1,Natural
2]), tgt :: NumberCategory
tgt = (Natural -> NumberCategory
numberCategory Natural
2), omap :: Map Natural Natural
omap=(Natural -> Natural) -> Set Natural -> Map Natural Natural
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Natural -> Natural
forall a. a -> a
id ([Natural] -> Set Natural
forall a. [a] -> Set a
set [Natural
1,Natural
2]), mmap :: Map (StarIdentity Natural) (IsSmallerThan Natural)
mmap = AssociationList (StarIdentity Natural) (IsSmallerThan Natural)
-> Map (StarIdentity Natural) (IsSmallerThan Natural)
forall k v. AssociationList k v -> Map k v
weakMap []}
(String -> IO ()
putStrLn(String -> IO ())
-> (Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String)
-> Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint) (Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ())
-> Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ()
forall a b. (a -> b) -> a -> b
$ Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
diag
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ PrecomposedFunctorCategory
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String
forall c m o.
(FiniteCategory c m o, Morphism m o, PrettyPrint c, PrettyPrint m,
PrettyPrint o, Eq m, Eq o) =>
c -> String
pprintFiniteCategory (Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> NumberCategory
-> PrecomposedFunctorCategory
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c2 m2 o2
-> c3 -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
PrecomposedFunctorCategory Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
diag (Natural -> NumberCategory
numberCategory Natural
3))
[IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([IO ()] -> IO [()]) -> [IO ()] -> IO [()]
forall a b. (a -> b) -> a -> b
$ (String -> IO ()
putStrLn(String -> IO ())
-> (Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String)
-> Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint) (Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ())
-> [Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
-> [IO ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set
(Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
-> [Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
forall a. Eq a => Set a -> [a]
setToList (PrecomposedFunctorCategory
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> Set
(Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> NumberCategory
-> PrecomposedFunctorCategory
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c2 m2 o2
-> c3 -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
PrecomposedFunctorCategory Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
diag (Natural -> NumberCategory
numberCategory Natural
3))))
[IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([IO ()] -> IO [()]) -> [IO ()] -> IO [()]
forall a b. (a -> b) -> a -> b
$ (String -> IO ()
putStrLn(String -> IO ())
-> (NaturalTransformation
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String)
-> NaturalTransformation
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint) (NaturalTransformation
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> IO ())
-> [NaturalTransformation
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
-> [IO ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set
(NaturalTransformation
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
-> [NaturalTransformation
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural]
forall a. Eq a => Set a -> [a]
setToList (PrecomposedFunctorCategory
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> Set
(NaturalTransformation
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
-> NumberCategory
-> PrecomposedFunctorCategory
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c2 m2 o2
-> c3 -> PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
PrecomposedFunctorCategory Diagram
(DiscreteCategory Natural)
(StarIdentity Natural)
Natural
NumberCategory
(IsSmallerThan Natural)
Natural
diag (Natural -> NumberCategory
numberCategory Natural
3))))
String -> IO ()
putStrLn String
"End of Math.FiniteCategories.FunctorCategory.Example"