{-| Module  : FiniteCategories
Description : Examples of Kan extensions exported with GraphViz.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of Kan extensions exported with GraphViz.

Export extensions in the directory "OutputGraphViz\/Examples\/Functor\/KanExtension".
-}
module Math.Functors.KanExtension.Example
(
    main
)
where
    import              Math.FiniteCategory
    import              Math.FiniteCategories
    import              Math.Functors.KanExtension
    import              Math.IO.FiniteCategories.ExportGraphViz
    
    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
    
    -- | Examples of Kan extensions exported with GraphViz.

    main :: IO ()
    main :: IO ()
main = do
        String -> IO ()
putStrLn String
"Start of Math.Functors.KanExtension.Example"
        let d1 :: Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
d1 = (Set
  (Diagram
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural)
-> [Diagram
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural]
forall a. Eq a => Set a -> [a]
setToList (Set
   (Diagram
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural)
 -> [Diagram
       (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
       (IsSmallerThan Natural)
       Natural
       (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
       (IsSmallerThan Natural)
       Natural])
-> Set
     (Diagram
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural)
-> [Diagram
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural]
forall a b. (a -> b) -> a -> b
$ FunctorCategory
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> Set
     (Diagram
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural)
forall c m o. FiniteCategory c m o => c -> Set o
ob (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
-> InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
-> FunctorCategory
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Natural
-> InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
numberCategory Natural
2) (Natural
-> InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
numberCategory Natural
4)))[Diagram
   (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
   (IsSmallerThan Natural)
   Natural
   (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
   (IsSmallerThan Natural)
   Natural]
-> Int
-> Diagram
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
forall a. [a] -> Int -> a
!! Int
3
        let d2 :: Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
d2 = (Set
  (Diagram
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural)
-> [Diagram
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural]
forall a. Eq a => Set a -> [a]
setToList (Set
   (Diagram
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural)
 -> [Diagram
       (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
       (IsSmallerThan Natural)
       Natural
       (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
       (IsSmallerThan Natural)
       Natural])
-> Set
     (Diagram
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural)
-> [Diagram
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural
      (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
      (IsSmallerThan Natural)
      Natural]
forall a b. (a -> b) -> a -> b
$ FunctorCategory
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> Set
     (Diagram
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural)
forall c m o. FiniteCategory c m o => c -> Set o
ob (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
-> InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
-> FunctorCategory
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (Natural
-> InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
numberCategory Natural
2) (Natural
-> InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
numberCategory Natural
3)))[Diagram
   (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
   (IsSmallerThan Natural)
   Natural
   (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
   (IsSmallerThan Natural)
   Natural]
-> Int
-> Diagram
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
forall a. [a] -> Int -> a
!! Int
2
        Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
d1 String
"OutputGraphViz/Examples/Functors/KanExtension/F"
        Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
d2 String
"OutputGraphViz/Examples/Functors/KanExtension/X"
        let Just (Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
lk,NaturalTransformation
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
lknat) = (Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> Diagram
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
-> Maybe
     (Diagram
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural,
      NaturalTransformation
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural)
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> Maybe
     (Diagram c2 m2 o2 c3 m3 o3,
      NaturalTransformation c1 m1 o1 c3 m3 o3)
leftKan Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
d1 Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
d2)
        Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
lk String
"OutputGraphViz/Examples/Functors/KanExtension/Lan_F(X)"
        NaturalTransformation
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1, Eq c1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, Eq c2, PrettyPrint m2,
 PrettyPrint o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> String -> IO ()
natToPdf NaturalTransformation
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
lknat String
"OutputGraphViz/Examples/Functors/KanExtension/EtaLan_F(X)"
        let Just (Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
rk,NaturalTransformation
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
rknat) = (Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> Diagram
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
     (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
     (IsSmallerThan Natural)
     Natural
-> Maybe
     (Diagram
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural,
      NaturalTransformation
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural
        (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
        (IsSmallerThan Natural)
        Natural)
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> Maybe
     (Diagram c2 m2 o2 c3 m3 o3,
      NaturalTransformation c1 m1 o1 c3 m3 o3)
rightKan Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
d1 Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
d2)
        Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 Diagram
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
rk String
"OutputGraphViz/Examples/Functors/KanExtension/Ran_F(X)"
        NaturalTransformation
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1, Eq c1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, Eq c2, PrettyPrint m2,
 PrettyPrint o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> String -> IO ()
natToPdf NaturalTransformation
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
  (InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
  (IsSmallerThan Natural)
  Natural
rknat String
"OutputGraphViz/Examples/Functors/KanExtension/RhoRan_F(X)"
        
        let a :: SCG
a = String -> SCG
unsafeReadSCGString String
"2\nA\n"
        SCG -> String -> IO ()
forall o m c.
(Eq o, PrettyPrint o, PrettyPrint m, Morphism m o,
 FiniteCategory c m o) =>
c -> String -> IO ()
catToPdf SCG
a String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/A"
        let b :: SCG
b = String -> SCG
unsafeReadSCGString String
"2\nA -f-> B\n"
        SCG -> String -> IO ()
forall o m c.
(Eq o, PrettyPrint o, PrettyPrint m, Morphism m o,
 FiniteCategory c m o) =>
c -> String -> IO ()
catToPdf SCG
b String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/B"
        let c :: SCG
c = String -> SCG
unsafeReadSCGString String
"2\nA -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n"
        SCG -> String -> IO ()
forall o m c.
(Eq o, PrettyPrint o, PrettyPrint m, Morphism m o,
 FiniteCategory c m o) =>
c -> String -> IO ()
catToPdf SCG
c String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/C"
        let f :: SCGD
f = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\n</SRC>\n<TGT>\n2\nA -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n</TGT>\nA => A"
        SCGD -> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 SCGD
f String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/F"
        let g :: SCGD
g = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\n</SRC>\n<TGT>\n2\nA -f-> B\n</TGT>\nA => A"
        SCGD -> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 SCGD
g String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/G"
        
        let Just (SCGD
lk,NaturalTransformation
  SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
lknat) = (SCGD
-> SCGD
-> Maybe
     (SCGD,
      NaturalTransformation
        SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text)
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> Maybe
     (Diagram c2 m2 o2 c3 m3 o3,
      NaturalTransformation c1 m1 o1 c3 m3 o3)
leftKan SCGD
f SCGD
g)
        SCGD -> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 SCGD
lk String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/Lan_F(G)"
        NaturalTransformation
  SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1, Eq c1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, Eq c2, PrettyPrint m2,
 PrettyPrint o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> String -> IO ()
natToPdf NaturalTransformation
  SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
lknat String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/EtaLan_F(G)"
        
        let Just (SCGD
rk,NaturalTransformation
  SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
rknat) = (SCGD
-> SCGD
-> Maybe
     (SCGD,
      NaturalTransformation
        SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text)
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c3 m3 o3
-> Maybe
     (Diagram c2 m2 o2 c3 m3 o3,
      NaturalTransformation c1 m1 o1 c3 m3 o3)
rightKan SCGD
f SCGD
g)
        SCGD -> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 SCGD
rk String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/Ran_F(G)"
        NaturalTransformation
  SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1, Eq c1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, Eq c2, PrettyPrint m2,
 PrettyPrint o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> String -> IO ()
natToPdf NaturalTransformation
  SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
rknat String
"OutputGraphViz/Examples/Functors/KanExtension/NotPointwise/EpsilonLan_F(G)"
        
        String -> IO ()
putStrLn String
"End of Math.Functors.KanExtension.Example"