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

Examples of Kan extensions.


-}
module Math.Functors.KanExtension.Examples
(
    exampleLeftKanExtension,
    exampleRightKanExtension,
)
where
    import              Math.FiniteCategory
    import              Math.FiniteCategories
    import              Math.Functors.KanExtension

    import              Data.Text                (Text)
    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
    

    -- | An example of left Kan Extension which computes the sum (disjunction) of two booleans variables.

    exampleLeftKanExtension :: Diagram (CompositionGraph Text Text) (CGMorphism Text Text) Text (CompositionGraph Text Text) (CGMorphism Text Text) Text
    exampleLeftKanExtension :: Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
exampleLeftKanExtension = Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
lk
        where
            a :: CompositionGraph Text Text
a = String -> CompositionGraph Text Text
unsafeReadCGString String
"A\nB\n"
            b :: CompositionGraph Text Text
b = String -> CompositionGraph Text Text
unsafeReadCGString String
"A -q1-> C\nB -q2-> C\n"
            c :: CompositionGraph Text Text
c = String -> CompositionGraph Text Text
unsafeReadCGString String
"0 -abs-> 1\n"
            f :: Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
f = String
-> Diagram
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nA -q1-> C\nB -q2-> C\n</TGT>\nA => A\nB => B\n"
            x :: Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
x = String
-> Diagram
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -abs-> 1\n</TGT>\nA => 0\nB => 1"
            Just (Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
lk,NaturalTransformation
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
lknat) = (Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
-> Diagram
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
-> Maybe
     (Diagram
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text,
      NaturalTransformation
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism 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 Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
f Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
x)
        
    -- | An example of right Kan Extension which computes the product (conjonction) of two booleans variables.

    exampleRightKanExtension :: Diagram (CompositionGraph Text Text) (CGMorphism Text Text) Text (CompositionGraph Text Text) (CGMorphism Text Text) Text
    exampleRightKanExtension :: Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
exampleRightKanExtension = Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
rk
        where
            a :: CompositionGraph Text Text
a = String -> CompositionGraph Text Text
unsafeReadCGString String
"A\nB\n"
            b :: CompositionGraph Text Text
b = String -> CompositionGraph Text Text
unsafeReadCGString String
"C -p1-> A\nC -p2-> B\n"
            c :: CompositionGraph Text Text
c = String -> CompositionGraph Text Text
unsafeReadCGString String
"0 -abs-> 1\n"
            f :: Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
f = String
-> Diagram
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nC -p1-> A\nC -p2-> B\n</TGT>\nA => A\nB => B\n"
            x :: Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
x = String
-> Diagram
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -abs-> 1\n</TGT>\nA => 0\nB => 1"
            Just (Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
rk,NaturalTransformation
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
rknat) = (Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
-> Diagram
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
-> Maybe
     (Diagram
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text,
      NaturalTransformation
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism 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 Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
f Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
x)