module Math.Functors.Adjunction.Example
(
main
)
where
import Math.FiniteCategory
import Math.FiniteCategories.Ens
import Math.FiniteCategories.DiscreteCategory
import Math.Categories.FunctorCategory
import Math.Functors.Adjunction
import Math.Functors.DiagonalFunctor
import Math.IO.PrettyPrint
import Math.FiniteCategory
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
main :: IO ()
main :: IO ()
main = do
String -> IO ()
putStrLn String
"Start of Math.Functors.Adjunction.Example"
let 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], [Int] -> Set Int
forall a. [a] -> Set a
set [Int
3,Int
4]]
let 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,Int
1]
let diagFunct :: Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
diagFunct = DiscreteCategory Int
-> Ens Int
-> Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity 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
let leftAdj :: Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
leftAdj = Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c1 m1 o1
leftAdjoint Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
diagFunct
let rightAdj :: Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
rightAdj = Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c1 m1 o1 -> Diagram c1 m1 o1 c2 m2 o2
rightAdjoint Diagram
(Ens Int)
(Function Int)
(Set Int)
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
diagFunct
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Ens Int -> 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 Ens Int
universe
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ DiscreteCategory Int -> 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 DiscreteCategory Int
indexing
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int)
-> String
forall a. PrettyPrint a => a -> String
pprint ((Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
-> Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int)
forall a b. (a, b) -> a
fst((Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
-> Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
-> (Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> (Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
-> (Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
forall a. Set a -> a
anElement(Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
-> (Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int))
-> (Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> (Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Map
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Set Int)
-> Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet)(Map
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Set Int)
-> Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int))
-> (Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Map
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Map
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Set Int)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap (Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int)
forall a b. (a -> b) -> a -> b
$ Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
leftAdj)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagram One One One (Ens Int) (Function Int) (Set Int) -> String
forall a. PrettyPrint a => a -> String
pprint (Ens Int
-> Set Int
-> Diagram One One One (Ens Int) (Function Int) (Set Int)
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject Ens Int
universe ((Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
-> Set Int
forall a b. (a, b) -> b
snd((Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
-> Set Int)
-> (Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> (Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Set Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
-> (Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
forall a. Set a -> a
anElement(Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
-> (Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int))
-> (Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> (Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Map
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Set Int)
-> Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet)(Map
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Set Int)
-> Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int))
-> (Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Map
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Set Int))
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Set
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int),
Set Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Map
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Set Int)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap (Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Set Int)
-> Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
-> Set Int
forall a b. (a -> b) -> a -> b
$ Diagram
(FunctorCategory
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(NaturalTransformation
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Diagram
(DiscreteCategory Int)
(StarIdentity Int)
Int
(Ens Int)
(Function Int)
(Set Int))
(Ens Int)
(Function Int)
(Set Int)
leftAdj))
String -> IO ()
putStrLn String
"End of Math.Functors.Adjunction.Example"