module Math.Functors.KanExtension.Example
(
main
)
where
import Math.FiniteCategory
import Math.FiniteCategories
import Math.Functors.KanExtension
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.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. HasCallStack => [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. HasCallStack => [a] -> Int -> a
!! Int
2
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagram
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint Diagram
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
d1
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagram
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint Diagram
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
d2
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)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagram
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint Diagram
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
lk
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ NaturalTransformation
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint NaturalTransformation
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
lknat
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)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagram
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint Diagram
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
rk
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ NaturalTransformation
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
-> String
forall a. PrettyPrint a => a -> String
pprint NaturalTransformation
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
(InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural)
(IsSmallerThan Natural)
Natural
rknat
let a :: SCG
a = String -> SCG
unsafeReadSCGString String
"2\nA\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
a
let b :: SCG
b = String -> SCG
unsafeReadSCGString String
"2\nA -f-> B\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
b
let c :: SCG
c = String -> SCG
unsafeReadSCGString String
"2\nA -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
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"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
f
let g :: SCGD
g = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\n</SRC>\n<TGT>\n2\nA -f-> B\n</TGT>\nA => A"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
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)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
lk
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
-> String
forall a. PrettyPrint a => a -> String
pprint NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
lknat
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)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
rk
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
-> String
forall a. PrettyPrint a => a -> String
pprint NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
rknat
let a :: SCG
a = String -> SCG
unsafeReadSCGString String
"2\nA\nB\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
a
let b :: SCG
b = String -> SCG
unsafeReadSCGString String
"2\nC -p1-> A\nC -p2-> B\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
b
let c :: SCG
c = String -> SCG
unsafeReadSCGString String
"2\n0 -abs-> 1\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
c
let f :: SCGD
f = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\nC -p1-> A\nC -p2-> B\n</TGT>\nA => A\nB => B\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
f
let x :: SCGD
x = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\n0 -abs-> 1\n</TGT>\nA => 1\nB => 1"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
x
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
x)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
rk
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
-> String
forall a. PrettyPrint a => a -> String
pprint NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
rknat
let a :: SCG
a = String -> SCG
unsafeReadSCGString String
"2\nA\nB\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
a
let b :: SCG
b = String -> SCG
unsafeReadSCGString String
"2\nA -q1-> C\nB -q2-> C\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
b
let c :: SCG
c = String -> SCG
unsafeReadSCGString String
"2\n0 -abs-> 1\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
c
let f :: SCGD
f = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\nA -q1-> C\nB -q2-> C\n</TGT>\nA => A\nB => B\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
f
let x :: SCGD
x = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\n0 -abs-> 1\n</TGT>\nA => 1\nB => 1"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
x
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
x)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
lk
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
-> String
forall a. PrettyPrint a => a -> String
pprint NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
lknat
let a :: SCG
a = String -> SCG
unsafeReadSCGString String
"2\nA\nB\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
a
let b :: SCG
b = String -> SCG
unsafeReadSCGString String
"2\nA -f-> C\nB -g-> C\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
b
let c :: SCG
c = String -> SCG
unsafeReadSCGString String
"2\n0 -f-> 1\n1 -g-> 2\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCG -> 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 SCG
c
let f :: SCGD
f = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\nA -f-> C\nB -g-> C\n</TGT>\nA => A\nB => B\n"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
f
let x :: SCGD
x = String -> SCGD
unsafeReadSCGDString String
"<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\n0 -f-> 1\n1 -g-> 2\n</TGT>\nA => 1\nB => 1"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
x
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
x)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
lk
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
-> String
forall a. PrettyPrint a => a -> String
pprint NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
lknat
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
x)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SCGD -> String
forall a. PrettyPrint a => a -> String
pprint SCGD
rk
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
-> String
forall a. PrettyPrint a => a -> String
pprint NaturalTransformation
SCG (SCGMorphism Text Text) Text SCG (SCGMorphism Text Text) Text
rknat
String -> IO ()
putStrLn String
"End of Math.Functors.KanExtension.Example"