{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : ('FinCat' 'ExponentialCategory') is the category in which live the exponential objects of 'FinCat' with the original categories.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

('FinCat' 'ExponentialCategory') is the category in which live the exponential objects of 'FinCat' with the original categories. To compute exponential objects in a usual category, see Math.CartesianClosedCategory. To compute exponential objects in a custom 'FiniteCategory', see 'exponentialObjects' in Math.CartesianClosedCategory.
-}

module Math.FiniteCategories.ExponentialCategory
(
    -- * Exponential category
    -- ** Object
    ExponentialCategoryObject(..),
    -- ** Morphism
    ExponentialCategoryMorphism(..),
    -- ** Category
    ExponentialCategory(..),
    -- * Cartesian category type
    -- ** Object
    CartesianObject(..),
    -- ** Morphism
    CartesianMorphism(..),
    -- ** Category
    CartesianCategory(..),
)
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              Data.List               (intercalate)
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.FiniteCategories.DiscreteTwo
    import              Math.FiniteCategories.LimitCategory
    import              Math.CompleteCategory
    import              Math.CartesianClosedCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.FinCat
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    -- | An object in an 'ExponentialCategory'. It is either a 'ExprojectedObject' in an original category or a 'ExponentialElementObject'.
    data ExponentialCategoryObject c m o = ExprojectedObject o -- ^ An 'ExprojectedObject' is an object o.
                                         | ExponentialElementObject (FinFunctor c m o) -- ^ The exponential elemets in Cat are functors.
        deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
       
       
    -- | A morphism in an 'ExponentialCategory'. It is either a 'ExprojectedMorphism' in an original category or an 'ExponentialElementMorphism'.
    data ExponentialCategoryMorphism c m o = ExprojectedMorphism m -- ^ An 'ExprojectedMorphism' is a morphism m.
                                           | ExponentialElementMorphism (NaturalTransformation c m o c m o) -- ^ A 'NaturalTransformation' is a morphism in the 'ExponentialCategory'.
        deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)        
        
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Morphism (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) where
        source (ExprojectedMorphism m) = ExprojectedObject (source m)
        source (ExponentialElementMorphism nat) = ExponentialElementObject (source nat)
        target (ExprojectedMorphism m) = ExprojectedObject (target m)
        target (ExponentialElementMorphism nat) = ExponentialElementObject (target nat)
        (ExprojectedMorphism m2) @ (ExprojectedMorphism m1) = ExprojectedMorphism $ m2 @ m1
        (ExponentialElementMorphism nat2) @ (ExponentialElementMorphism nat1) = ExponentialElementMorphism $ nat2 @ nat1
        _ @ _ = error "Incompatible composition of ExponentialCategory morphisms."
    
    
    
    -- | An 'ExponentialCategory' is either an 'ExprojectedCategory' (an original category) or an 'ExponentialCategory'.
    data ExponentialCategory c m o = ExprojectedCategory c -- ^ An original category in 'FinCat'.
                                   | ExponentialCategory (FunctorCategory c m o c m o)     -- ^ The exponential category of a given 2-base is a 'FunctorCategory'.
        deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) where
        identity (ExprojectedCategory c) (ExprojectedObject o) = ExprojectedMorphism $ identity c o
        identity (ExponentialCategory _) (ExprojectedObject _) = error "Identity in an exponential category on an exprojected object."
        identity (ExprojectedCategory _) (ExponentialElementObject _) = error "Identity in an exprojected category on a exponential element."
        identity (ExponentialCategory functCat) (ExponentialElementObject funct) = ExponentialElementMorphism $ identity functCat funct
        ar (ExprojectedCategory functCat) (ExprojectedObject s) (ExprojectedObject t) = ExprojectedMorphism <$> ar functCat s t
        ar (ExprojectedCategory _) (ExprojectedObject _) (ExponentialElementObject _) = error "Ar in an exprojected category where the target is an exponential element."
        ar (ExprojectedCategory _) (ExponentialElementObject _) (ExprojectedObject _) = error "Ar in an exprojected category where the source is an exponential element."
        ar (ExprojectedCategory _) (ExponentialElementObject _) (ExponentialElementObject _) = error "Ar in an exprojected category where the source and the target are exponential elements."
        ar (ExponentialCategory _) (ExprojectedObject _) (ExprojectedObject _) = error "Ar in an exponential category where the source and target are exprojected objects."
        ar (ExponentialCategory _) (ExprojectedObject _) (ExponentialElementObject _) = error "Ar in an exponential category where the source is an exprojected object."
        ar (ExponentialCategory _) (ExponentialElementObject _) (ExprojectedObject _) = error "Ar in an exponential category where the target is an exprojected object."
        ar (ExponentialCategory functCat) (ExponentialElementObject s) (ExponentialElementObject t) = ExponentialElementMorphism <$> ar functCat s t
            
            
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) where
        ob (ExprojectedCategory cat) = ExprojectedObject <$> ob cat
        ob (ExponentialCategory functCat) = ExponentialElementObject <$> ob functCat
    
    type TwoProductOfCategories c m o = FinCat (LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o) (Limit DiscreteTwoOb m) (Limit DiscreteTwoOb o)
    type TwoProductOfCategoriesMorphism c m o = FinFunctor (LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o) (Limit DiscreteTwoOb m) (Limit DiscreteTwoOb o)
    type TwoProductOfCategoriesObject c m o = LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o
    
    -- | The type of the category containing categories and their exponential objects.
    type CartesianCategory c m o = TwoProductOfCategories (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
    
    -- | A morphism in 'CartesianCategory'.
    type CartesianMorphism c m o = TwoProductOfCategoriesMorphism (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
    
    -- | An object in 'CartesianCategory'.
    type CartesianObject c m o = TwoProductOfCategoriesObject (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => CartesianClosedCategory (FinCat c m o) (FinFunctor c m o) c (TwoProductOfCategories c m o) (TwoProductOfCategoriesMorphism c m o) (TwoProductOfCategoriesObject c m o) (CartesianCategory c m o) (CartesianMorphism c m o) (CartesianObject c m o) where
        internalHom twoBase = unsafeTripod twoLimit evalMap_
            where
                powerObject = ExponentialCategory (FunctorCategory (twoBase ->$ A) (twoBase ->$ B))
                baseTwoCone = twoDiagram FinCat powerObject (ExprojectedCategory (twoBase ->$ A))
                twoLimit = limit baseTwoCone
                evalOb (ProductElement tuple) = Projection (ExprojectedObject $ funct ->$ x)
                    where
                        (ExponentialElementObject funct) = tuple |!| A
                        (ExprojectedObject x)  = tuple |!| B
                evalAr (ProductElement tuple) = Projection (ExprojectedMorphism $ ((target nat) ->£ f) @ (nat =>$ (source f)))
                    where
                        (ExponentialElementMorphism nat) = tuple |!| A
                        (ExprojectedMorphism f)  = tuple |!| B
                finalInternalCodomain = Projection $ (Exprojection $ twoBase ->$ A)
                newInternalCodomain = ProjectedCategory $ ExprojectedCategory $ (twoBase ->$ B)
                evalMap_ = Diagram{src = apex twoLimit, tgt = newInternalCodomain, omap = memorizeFunction evalOb (ob $ apex twoLimit), mmap = memorizeFunction evalAr (arrows $ apex twoLimit)}