{-| Module  : FiniteCategories
Description : An example of 'FunctorCategory' pretty printed.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An example of 'FunctorCategory' pretty printed.


-}
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
    
    -- | An example of 'FunctorCategory' pretty printed.

    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"