{-# LANGUAGE MonadComprehensions, MultiParamTypeClasses  #-}
{-| Module  : FiniteCategories
Description : Kan extensions for arbitrary functors.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Kan extensions for arbitrary functors. See 'Math.Functors.SetValued' for Kan extensions for set-valued functors.
-}

module Math.Functors.KanExtension 
(
    leftKan,
    rightKan,
)
where
    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

    import              Math.FiniteCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.CommaCategory
    
    
    -- | KanObject is either a functor X : A -> C or a functor to be precomposed called RL : B -> C (R or L).
    data KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3 = X (Diagram c1 m1 o1 c3 m3 o3) | RL (Diagram c2 m2 o2 c3 m3 o3) deriving (Eq, Show)
    
    -- | RightKanMorphism is a natural transformation Delta between functors to be precomposed or a natural transformation Mu to X.
    data RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 = Delta (NaturalTransformation c2 m2 o2 c3 m3 o3) (Diagram c1 m1 o1 c2 m2 o2) | Mu (NaturalTransformation c1 m1 o1 c3 m3 o3) deriving (Eq, Show)
    
    instance (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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
              Morphism (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        (@?) (Delta nat1 diag1) (Delta nat2 diag2)
            | diag1 == diag2 = (\x -> Delta x diag1) <$> (nat1 @? nat2)
            | otherwise = Nothing
        (@?) (Mu nat2) (Delta nat1 diag) = Mu <$> (nat2 @? (nat1 <=@<- diag))
        (@?) (Mu nat1) (Mu nat2) = Mu <$> (nat1 @? nat2)
        (@?) _ _ = Nothing
    
        source (Delta nat _) = RL (source nat)
        source (Mu nat) = X (source nat)
        
        target (Delta nat _) = RL (target nat)
        target (Mu nat) = X (target nat)
        
    -- | RightKanCategory is the category in which we want to take a comma category to find the terminal object.
    data RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = RightKanCategory (Diagram c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c3 m3 o3) deriving (Eq, Show)
    
    instance (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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        Category (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
            identity (RightKanCategory _ _) (X diag) = Mu (identity (FunctorCategory (src diag) (tgt diag)) diag)
            identity (RightKanCategory f _) (RL diag) = Delta (identity (FunctorCategory (src diag) (tgt diag)) diag) f
            
            ar (RightKanCategory _ _) (X diag1) (X diag2) = Mu <$> ar (FunctorCategory (src diag1) (tgt diag1)) diag1 diag2
            ar (RightKanCategory f _) (RL diag1) (RL diag2) = (\x -> Delta x f) <$> ar (FunctorCategory (src diag1) (tgt diag1)) diag1 diag2
            ar (RightKanCategory f _) (RL diag1) (X diag2) = Mu <$> ar (FunctorCategory (src diag2) (tgt diag2)) (diag1 <-@<- f) diag2
            ar (RightKanCategory _ _) (X _) (RL _) = set []
            
    instance (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) =>
        FiniteCategory (RightKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (RightKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        
            ob (RightKanCategory f x) = Set.insert (X x) (RL <$> ob (FunctorCategory (tgt f) (tgt x)))
    
    
    -- | Right Kan extension for two arbitrary functors.
    
    -- rightKan f x is the right Kan extension of x along f.
    rightKan ::  (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 f x = if Set.null terminals then Nothing else Just (terminalFunctor, terminalNat)
        where
            kanCat = RightKanCategory f x
            functCat = FunctorCategory (tgt f) (tgt x)
            t = Diagram{src=functCat, tgt=kanCat, omap=memorizeFunction RL (ob functCat), mmap = memorizeFunction (\x -> Delta x f) (arrows functCat)}
            commaCat = CommaCategory{leftDiagram=t, rightDiagram=selectObject kanCat (X x)}
            terminals = terminalObjects commaCat
            aTerminal = anElement terminals
            terminalFunctor = indexSource aTerminal
            Mu terminalNat = selectedArrow aTerminal
            
            
    
    
    
    
    
    -- | LeftKanMorphism is a natural transformation Sigma between functors to be precomposed or a natural transformation Alpha from X.
    data LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3 = Sigma (NaturalTransformation c2 m2 o2 c3 m3 o3) (Diagram c1 m1 o1 c2 m2 o2) | Alpha (NaturalTransformation c1 m1 o1 c3 m3 o3) deriving (Eq, Show)
    
    instance (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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
              Morphism (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        (@?) (Sigma nat1 diag1) (Sigma nat2 diag2)
            | diag1 == diag2 = (\x -> Sigma x diag1) <$> (nat1 @? nat2)
            | otherwise = Nothing
        (@?) (Sigma nat1 diag) (Alpha nat2) = Alpha <$> ((nat1 <=@<- diag) @? nat2)
        (@?) (Alpha nat1) (Alpha nat2) = Alpha <$> (nat1 @? nat2)
        (@?) _ _ = Nothing
    
        source (Sigma nat _) = RL (source nat)
        source (Alpha nat) = X (source nat)
        
        target (Sigma nat _) = RL (target nat)
        target (Alpha nat) = X (target nat)
        
    -- | LeftKanCategory is the category in which we want to take a comma category to find the initial object.
    data LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = LeftKanCategory (Diagram c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c3 m3 o3) deriving (Eq, Show)
    
    instance (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,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        Category (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
            identity (LeftKanCategory _ _) (X diag) = Alpha (identity (FunctorCategory (src diag) (tgt diag)) diag)
            identity (LeftKanCategory f _) (RL diag) = Sigma (identity (FunctorCategory (src diag) (tgt diag)) diag) f
            
            ar (LeftKanCategory _ _) (X diag1) (X diag2) = Alpha <$> ar (FunctorCategory (src diag1) (tgt diag1)) diag1 diag2
            ar (LeftKanCategory f _) (RL diag1) (RL diag2) = (\x -> Sigma x f) <$> ar (FunctorCategory (src diag1) (tgt diag1)) diag1 diag2
            ar (LeftKanCategory f _) (X diag2) (RL diag1)= Alpha <$> ar (FunctorCategory (src diag2) (tgt diag2)) diag2 (diag1 <-@<- f)
            ar _ _ _ = set []
            
    instance (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) =>
        FiniteCategory (LeftKanCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (LeftKanMorphism c1 m1 o1 c2 m2 o2 c3 m3 o3) (KanObject c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        
            ob (LeftKanCategory f x) = Set.insert (X x) (RL <$> ob (FunctorCategory (tgt f) (tgt x)))
    
    
    -- | Left Kan extension for two arbitrary functors.
    
    -- leftKan f x is the left Kan extension of x along f.
    leftKan ::  (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 f x = if Set.null initials then Nothing else Just (initialFunctor, initialNat)
        where
            kanCat = LeftKanCategory f x
            functCat = FunctorCategory (tgt f) (tgt x)
            t = Diagram{src=functCat, tgt=kanCat, omap=memorizeFunction RL (ob functCat), mmap = memorizeFunction (\x -> Sigma x f) (arrows functCat)}
            commaCat = CommaCategory{leftDiagram=selectObject kanCat (X x), rightDiagram=t}
            initials = initialObjects commaCat
            aInitial = anElement initials
            initialFunctor = indexTarget aInitial
            Alpha initialNat = selectedArrow aInitial