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

{-| Module  : FiniteCategories
Description : A 'Sketch' is a category equipped with distinguished cones, cocones and tripods.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'Sketch' is a category equipped with distinguished cones, cocones and tripods. (In litterature, a mixed sketch only distinguishes cones and cocones but we add exponential objects to model second-order logical structures.)

The category is represented by a composition graph.

-}

module Math.Categories.FinSketch
(
    -- * Types for Sketch
    CategorySketch(..),
    ArrowSketch(..),
    ObjectSketch(..),
    ConeSketch(..),
    CoconeSketch(..),
    TripodSketch(..),
    SketchError(..),
    constructTwoConeFromTripod,
    constructTwoConeFromTripodText,
    -- * Sketch
    Sketch,
    -- ** Getters
    underlyingCategory,
    supportSketch,
    distinguishedCones,
    distinguishedCocones,
    distinguishedTripods,
    -- ** Smart constructors
    unsafeSketch,
    sketch,
    sketchText,
    -- ** Helpers
    checkSketch,
    checkFiniteSketch,
    -- * Sketch morphism,
    SketchMorphism,
    SketchMorphismError(..),
    -- ** Getter
    underlyingFunctor,
    -- ** Smart constructors
    unsafeSketchMorphism,
    sketchMorphism,
    -- ** Other functions
    canFunctorBePromotedIntoSketchMorphism,
    
    -- * The category of finite sketches
    FinSketch(..),
    
    -- * Functions for shiny sketches
    -- Lantern(..),
    containsLantern,
    -- Spotlight(..),
    containsSpotlight,
    -- CrescentMoon(..),
    containsCrescentMoon,
    -- Colantern(..),
    containsColantern,
    -- Cospotlight(..),
    containsCospotlight,
    -- CocrescentMoon(..),
    containsCocrescentMoon,
    LightConstruction(..),
    containsLightConstruction,
    
    -- * Ehresmann realization
    -- factorsCone,
    -- factorsCocone,
    -- lonelyCones,
    -- lonelyCocones,
    -- crowdedCones,
    -- crowdedCocones,
    -- createLonelyConeCorrectionArrow,
    -- createLonelyCoconeCorrectionArrow,
    -- addLonelinessCorrectionArrows,
    -- quotientArrows,
    -- stepRealization,
    -- stepRealizationText,
)

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.Text            (Text, pack)
    import              Data.Simplifiable
    import              Data.Maybe           (isJust, isNothing, fromJust)
    import              Data.Either          (isLeft)

    import              Math.FiniteCategory
    import              Math.CocompleteCategory
    import              Math.CartesianClosedCategory
    import              Math.FiniteCategories.Parallel
    import              Math.FiniteCategories.CompositionGraph
    import              Math.FiniteCategories.ColimitCategory
    import              Math.FiniteCategories.DiscreteTwo
    import              Math.Categories.FunctorCategory
    import              Math.Categories.CommaCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.FinCat
    import              Math.Categories.FinGrph
    import              Math.FiniteCategoryError
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics

    type CategorySketch n e = CompositionGraph n e
    type ArrowSketch n e = CGMorphism n e
    type ObjectSketch n e = n
     
    type ConeSketch n e = Cone (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)
    type CoconeSketch n e = Cocone (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)
    type TripodSketch n e = Tripod (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)

    type FunctorSketch n e = FinFunctor (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)
    
   
    -- | Construct a 2-cone selecting the power object and the internal domain of a 'Tripod'. This 2-cone can then be added to the distinguished cones of a 'Sketch'. The two first arguments are arbitrary distinct objects of type n (they will be the objects of the indexing category of the 2-cone).
    constructTwoConeFromTripod :: (Eq n, Eq e) => n -> n -> TripodSketch n e -> ConeSketch n e
    constructTwoConeFromTripod a b t
        | a == b = error "constructTwoConeFromTripod with two same indexing objects."
        | otherwise = unsafeCone (apex $ twoCone $ t) nat
        where
            indexingCategory = unsafeCompositionGraph (unsafeGraph (set [a,b]) (set [])) (weakMap [])
            srcDiag = constantDiagram indexingCategory (universeCategoryTripod t) (apex $ twoCone $ t)
            tgtDiag = completeDiagram $ Diagram{src = indexingCategory, tgt = universeCategoryTripod t, omap = weakMap [(a, powerObject t),(b, internalDomain t)], mmap = weakMap []}
            nat = unsafeNaturalTransformation srcDiag tgtDiag (weakMap [(a, (legsCone $ twoCone t) =>$ A),(b, (legsCone $ twoCone t) =>$ B)])
   
    -- | Specialized version of 'constructTwoConeFromTripod' for 'Sketch' of 'Text'.
    constructTwoConeFromTripodText :: TripodSketch Text Text -> ConeSketch Text Text
    constructTwoConeFromTripodText = constructTwoConeFromTripod (pack "A") (pack "B")
   

    -- | Sketch is private, use the smart constructor 'sketch' or 'unsafeSketch' to construct one. Note that for each distinguished 'Tripod', the 2-cone of the 'Tripod' should belong to the distinguished 'cones' (the 2-cone can be constructed with 'constructTwoConeFromTripod').
    data Sketch n e = Sketch {
        underlyingCategory :: CategorySketch n e,
        distinguishedCones :: Set (ConeSketch n e),
        distinguishedCocones :: Set (CoconeSketch n e),
        distinguishedTripods :: Set (TripodSketch n e)
    } deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
    
    -- | The support of a 'Sketch' is the multidigraph generating the underlying category of the 'Sketch'.
    supportSketch :: Sketch n e -> Graph n e
    supportSketch = support.underlyingCategory
    
    -- | Unsafe constructor for a 'Sketch'. Use with caution, prefer 'sketch' which checks the structure of the 'Sketch.
    --
    --  Note that for each distinguished 'Tripod', the 2-cone of the 'Tripod' should belong to the distinguished 'cones'.
    unsafeSketch :: CategorySketch n e -> Set (ConeSketch n e) -> Set (CoconeSketch n e) -> Set (TripodSketch n e) -> Sketch n e
    unsafeSketch uc c cc t = Sketch{underlyingCategory = uc, distinguishedCones = c, distinguishedCocones = cc, distinguishedTripods= t }

    -- | A 'SketchError' could be a cone with a base outside the underlying category, a cocone with base outside the underlying category, a tripod with a base outside the underlying category, a tripod where the 2-cone does not belong to the distinguished cones of the sketch or an error in the underlying category.
    data SketchError n e = BaseOfConeIsNotInUnderlyingCategory (ConeSketch n e)
                     | BaseOfCoconeIsNotInUnderlyingCategory (CoconeSketch n e)
                     | BaseOfTripodIsNotInUnderlyingCategory (TripodSketch n e)
                     | TripodTwoConeDoesNotBelongToDistinguishedCones (TripodSketch n e)
                     | UnderlyingCategoryError (FiniteCategoryError (ArrowSketch n e) (ObjectSketch n e))
                     | TwoSameIndexingObjects n
        deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)


    -- | Find the first occurence which evaluates to true.
    find :: (Eq a) => (a -> Bool) -> Set a -> Maybe a
    find p s = if Set.null filtered then Nothing else Just (anElement filtered)
        where
            filtered = Set.filter p s

    -- | Smart constructor for a finite 'Sketch'. Note that for each distinguished 'Tripod', the 2-cone of the 'Tripod' is added to the distinguished 'cones' of the sketch. The two first arguments are arbitrary distinct objects of type n which will be the indexing objects of the new 2-cones.
    sketch :: (Eq n, Eq e) => n -> n -> CategorySketch n e -> (Set (ConeSketch n e)) -> (Set (CoconeSketch n e)) -> (Set (TripodSketch n e)) -> Either (SketchError n e) (Sketch n e)
    sketch a b cat c cc t
        | not $ null $ errCat = Left $ UnderlyingCategoryError $ fromJust errCat
        | not $ null $ faultyCone = Left $ BaseOfConeIsNotInUnderlyingCategory (fromJust faultyCone) 
        | not $ null $ faultyCocone = Left $ BaseOfCoconeIsNotInUnderlyingCategory (fromJust faultyCocone)
        | not $ null $ faultyTripod = Left $ BaseOfTripodIsNotInUnderlyingCategory (fromJust faultyTripod)
        | a == b = Left $ TwoSameIndexingObjects a
        | otherwise = Right s
        where   
            errCat = checkFiniteCategory cat
            fromJust (Just x) = x
            newCones = constructTwoConeFromTripod a b <$> t
            s = Sketch{underlyingCategory = cat, distinguishedCones = c ||| newCones, distinguishedCocones = cc, distinguishedTripods = t}
            faultyCone = find (\x -> universeCategoryCone x /= cat) c
            faultyCocone = find (\x -> universeCategoryCocone x /= cat) cc
            faultyTripod = find (\x -> universeCategoryTripod x /= cat) t
       
    -- | Specialized version of 'sketch' for sketches of 'Text'.
    sketchText :: CategorySketch Text Text -> (Set (ConeSketch Text Text)) -> (Set (CoconeSketch Text Text)) -> (Set (TripodSketch Text Text)) -> Either (SketchError Text Text) (Sketch Text Text)
    sketchText = sketch (pack "A") (pack "B")
       
    -- | Check wether a 'Sketch' is well formed or not, return a 'SketchError' if it is malformed, Nothing otherwise. Does not check the underlying 'CompositionGraph'.
    checkSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e)
    checkSketch Sketch{underlyingCategory = cat, distinguishedCones = c, distinguishedCocones = cc, distinguishedTripods = t}
        | not $ null $ faultyCone = BaseOfConeIsNotInUnderlyingCategory <$> faultyCone 
        | not $ null $ faultyCocone = BaseOfCoconeIsNotInUnderlyingCategory <$> faultyCocone
        | not $ null $ faultyTripod = BaseOfTripodIsNotInUnderlyingCategory <$> faultyTripod
        | not $ null $ faultyTripod2 = TripodTwoConeDoesNotBelongToDistinguishedCones <$> faultyTripod2
        | otherwise = Nothing
        where
            faultyCone = find (\x -> universeCategoryCone x /= cat) c
            faultyCocone = find (\x -> universeCategoryCocone x /= cat) cc
            faultyTripod = find (\x -> universeCategoryTripod x /= cat) t
            faultyTripod2 = find (\x -> not $ Set.or [apex cone == (apex $ twoCone x) && (cardinal $ ob $ indexingCategoryCone cone) == 2 && (cardinal $ arrows $ indexingCategoryCone cone) == 2 && (target <$> Map.values (components $ legsCone cone)) == set [powerObject x, internalDomain x] | cone <- c]) t
       
    -- | Check wether a finite 'Sketch' is well formed or not, return a 'SketchError' if it is malformed, Nothing otherwise.
    checkFiniteSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e)
    checkFiniteSketch Sketch{underlyingCategory = cat, distinguishedCones = c, distinguishedCocones = cc, distinguishedTripods = t}
        | not $ null $ errCat = UnderlyingCategoryError <$> errCat
        | not $ null $ faultyCone = BaseOfConeIsNotInUnderlyingCategory <$> faultyCone 
        | not $ null $ faultyCocone = BaseOfCoconeIsNotInUnderlyingCategory <$> faultyCocone
        | not $ null $ faultyTripod = BaseOfTripodIsNotInUnderlyingCategory <$> faultyTripod
        | not $ null $ faultyTripod2 = TripodTwoConeDoesNotBelongToDistinguishedCones <$> faultyTripod2
        | otherwise = Nothing
        where
            errCat = checkFiniteCategory cat
            faultyCone = find (\x -> universeCategoryCone x /= cat) c
            faultyCocone = find (\x -> universeCategoryCocone x /= cat) cc
            faultyTripod = find (\x -> universeCategoryTripod x /= cat) t
            faultyTripod2 = find (\x -> not $ Set.or [apex cone == (apex $ twoCone x) && (cardinal $ ob $ indexingCategoryCone cone) == 2 && (cardinal $ arrows $ indexingCategoryCone cone) == 2 && (target <$> Map.values (components $ legsCone cone)) == set [powerObject x, internalDomain x] | cone <- c]) t
            

    -- | SketchMorphism is private, use the smart constructor 'sketchMorphism' or 'unsafeSketchMorphism' to construct one.
    data SketchMorphism n e = SketchMorphism {
                                underlyingFunctor :: FunctorSketch n e, -- ^ Underlying functor of a 'SketchMorphism'.
                                sourceSketch :: Sketch n e, -- ^ The source of a 'SketchMorphism'. We have to store this to implement the source function of the 'Morphism' typeclass. This getter is not exported as you can get the source of the 'SketchMorphism' using the 'source' function.
                                targetSketch :: Sketch n e -- ^ The target of a 'SketchMorphism'. See 'sourceSketch'.
                            } deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
    
    -- | A 'SketchError' could be a cone not sent to a cone, a cocone not sent to a cocone or an error in the underlying functor.
    data SketchMorphismError n e = ConeNotSentToACone (ConeSketch n e)
                                 | CoconeNotSentToACocone (CoconeSketch n e)
                                 | TripodNotSentToATripod (TripodSketch n e)
                                 | UnderlyingFunctorError (DiagramError (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e))
                                 | WrongSource (CategorySketch n e) (CategorySketch n e)
                                 | WrongTarget (CategorySketch n e) (CategorySketch n e)
                                 deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
    
    -- | Unsafe constructor for a 'SketchMorphism'. Use with caution, prefer 'sketch' which checks the structure of the 'SketchMorphism'.
    unsafeSketchMorphism :: Sketch n e -> Sketch n e -> FunctorSketch n e -> SketchMorphism n e
    unsafeSketchMorphism s t f = SketchMorphism{underlyingFunctor = f, sourceSketch = s, targetSketch = t}
    
    -- | Smart constructor for a 'SketchMorphism'. It checks wether cones are sent to cones and cocones are sent to cocones.
    sketchMorphism :: (Eq n, Eq e) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Either (SketchMorphismError n e) (SketchMorphism n e)
    sketchMorphism s t f
        | not $ null errFunct = Left $ UnderlyingFunctorError $ fromJust $ errFunct
        | not $ null faultyCone = Left $ ConeNotSentToACone (fromJust faultyCone) 
        | not $ null faultyCocone = Left $ CoconeNotSentToACocone (fromJust faultyCocone)
        | not $ null faultyTripod = Left $ TripodNotSentToATripod (fromJust faultyTripod)
        | src f /= underlyingCategory s = Left $ WrongSource (src f) (underlyingCategory s)
        | tgt f /= underlyingCategory t = Left $ WrongTarget (tgt f) (underlyingCategory t)
        | otherwise = Right $ SketchMorphism{underlyingFunctor = f, sourceSketch = s, targetSketch = t}
        where
            errFunct = checkDiagram f
            fromJust (Just x) = x
            faultyCone = find (\cone_ -> not $ (unsafeCone (f ->$ (apex cone_)) (f <-@<= legsCone cone_)) `Set.isIn` (distinguishedCones t)) (distinguishedCones s)
            faultyCocone = find (\cocone_ -> not $ (unsafeCocone (f ->$ (nadir cocone_)) (f <-@<= legsCocone cocone_)) `Set.isIn` (distinguishedCocones t)) (distinguishedCocones s)
            faultyTripod = find (\tripod_ -> not $ (unsafeTripod (unsafeCone (f ->$ (apex (twoCone tripod_))) (f <-@<= legsCone (twoCone tripod_))) (f ->£ (evalMap tripod_))) `Set.isIn` (distinguishedTripods t)) (distinguishedTripods s)
            

    -- | Return wether a 'Functor' can be promoted into a 'SketchMorphism'.
    canFunctorBePromotedIntoSketchMorphism :: (Eq e, Eq n) => Sketch n e -> Sketch n e -> (FunctorSketch n e) -> Bool
    canFunctorBePromotedIntoSketchMorphism s t f = null faultyCone && null faultyCocone && null faultyTripod
        where
            faultyCone = find (\cone_ -> not $ (unsafeCone (f ->$ (apex cone_)) (f <-@<= legsCone cone_)) `Set.isIn` (distinguishedCones t)) (distinguishedCones s)
            faultyCocone = find (\cocone_ -> not $ (unsafeCocone (f ->$ (nadir cocone_)) (f <-@<= legsCocone cocone_)) `Set.isIn` (distinguishedCocones t)) (distinguishedCocones s)
            faultyTripod = find (\tripod_ -> not $ (unsafeTripod (unsafeCone (f ->$ (apex (twoCone tripod_))) (f <-@<= legsCone (twoCone tripod_))) (f ->£ (evalMap tripod_))) `Set.isIn` (distinguishedTripods t)) (distinguishedTripods s)


    instance (Eq e, Eq n) => Morphism (SketchMorphism n e) (Sketch n e) where
        source = sourceSketch
        target = targetSketch
        sm2 @ sm1 = SketchMorphism{underlyingFunctor = (underlyingFunctor sm2) @ (underlyingFunctor sm1), sourceSketch = sourceSketch sm1, targetSketch = targetSketch sm2}


    data FinSketch n e = FinSketch deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    instance (Eq e, Eq n) => Category (FinSketch n e) (SketchMorphism n e) (Sketch n e) where
        identity _ s = SketchMorphism{underlyingFunctor = identity FinCat (underlyingCategory s), sourceSketch = s, targetSketch = s}
        
        ar _ s t = unsafeSketchMorphism s t <$> Set.filter (canFunctorBePromotedIntoSketchMorphism s t) (ar FinCat (underlyingCategory s) (underlyingCategory t))
        
    instance (Eq e, Eq n) => 
        HasCoequalizers (FinSketch n e) (SketchMorphism n e) (Sketch n e) where
        coequalize parallelDiag = unsafeCocone nadirSketch legs
            where
                parallelDiagOfCg = Diagram{src = Parallel, tgt = FinCat, omap = underlyingCategory <$> omap parallelDiag, mmap = underlyingFunctor <$> mmap parallelDiag}
                coeqCg = coequalize parallelDiagOfCg
                transformCone c = unsafeCone (((legsCocone coeqCg) =>$ ParallelB) ->$ (apex c)) (((legsCocone coeqCg) =>$ ParallelB) <-@<= (legsCone c))
                transformCocone cc = unsafeCocone (((legsCocone coeqCg) =>$ ParallelB) ->$ (nadir cc)) (((legsCocone coeqCg) =>$ ParallelB) <-@<=(legsCocone cc))
                transformTripod t = unsafeTripod (transformCone (twoCone t)) (((legsCocone coeqCg) =>$ ParallelB) ->£ (evalMap t))
                nadirSketch = Sketch{underlyingCategory = nadir coeqCg, distinguishedCones = transformCone <$> distinguishedCones (parallelDiag ->$ ParallelB), distinguishedCocones = transformCocone <$> distinguishedCocones (parallelDiag ->$ ParallelB), distinguishedTripods = transformTripod <$> distinguishedTripods (parallelDiag ->$ ParallelB)}
                leg1 = SketchMorphism{sourceSketch = parallelDiag ->$ ParallelA, targetSketch = nadirSketch, underlyingFunctor = (legsCocone coeqCg) =>$ ParallelA}
                leg2 = SketchMorphism{sourceSketch = parallelDiag ->$ ParallelB, targetSketch = nadirSketch, underlyingFunctor = (legsCocone coeqCg) =>$ ParallelB}
                legs = unsafeNaturalTransformation parallelDiag (constantDiagram Parallel FinSketch nadirSketch) (weakMap [(ParallelA, leg1),(ParallelB, leg2)])
                
        
    instance (Eq e, Eq n, Eq oIndex, Eq mIndex, Morphism mIndex oIndex, FiniteCategory cIndex mIndex oIndex) => CocompleteCategory (FinSketch n e) (SketchMorphism n e) (Sketch n e) (FinSketch (Colimit oIndex n) (Colimit oIndex e)) (SketchMorphism (Colimit oIndex n) (Colimit oIndex e)) (Sketch (Colimit oIndex n) (Colimit oIndex e)) cIndex mIndex oIndex where
        colimit diagOfSketches = unsafeCocone nadirSketch legs
            where
                indexingCategory = src diagOfSketches
                diagOfCG = Diagram{src = indexingCategory, tgt = FinCat, omap = Map.weakMapFromSet [(i,underlyingCategory (diagOfSketches ->$ i)) | i <- ob indexingCategory], mmap = Map.weakMapFromSet [(f,underlyingFunctor (diagOfSketches ->£ f)) | f <- genArrows indexingCategory]}
                colimitCG = colimitOfCompositionGraphs diagOfCG
                coprojBase = coprojectBaseCompositionGraphs diagOfCG
                transformCone i c = unsafeCone (((legsCocone colimitCG) =>$ i) ->$ (apex c)) (((legsCocone colimitCG) =>$ i) <-@<= (legsCone c))
                transformCocone i cc = unsafeCocone (((legsCocone colimitCG) =>$ i) ->$ (nadir cc)) (((legsCocone colimitCG) =>$ i) <-@<=(legsCocone cc))
                transformTripod i t = unsafeTripod (transformCone i (twoCone t)) (((legsCocone colimitCG) =>$ i) ->£ (evalMap t))
                nadirSketch = Sketch{underlyingCategory = (nadir colimitCG), distinguishedCones = Set.unions [transformCone i <$> distinguishedCones (newBase ->$ i)| i <- Set.setToList $ ob $ src newBase], distinguishedCocones = Set.unions [transformCocone i <$> distinguishedCocones (newBase ->$ i)| i <- Set.setToList $ ob $ src newBase], distinguishedTripods = Set.unions [transformTripod i <$> distinguishedTripods (newBase ->$ i)| i <- Set.setToList $ ob $ src newBase]}
                newBase = coprojectBase diagOfSketches <-@<- diagOfSketches
                legs = unsafeNaturalTransformation newBase (constantDiagram indexingCategory FinSketch nadirSketch) (Map.weakMapFromSet [(i,SketchMorphism{sourceSketch = newBase ->$ i, targetSketch = nadirSketch, underlyingFunctor = (legsCocone colimitCG) =>$ i}) | i <- ob indexingCategory])
                
        coprojectBase diag = Diagram{src = FinSketch, tgt = FinSketch, omap = Map.weakMapFromSet [(diag ->$ i,coprojectSketch $  diag ->$ i) | i <- ob $ src diag], mmap = Map.weakMapFromSet [(diag ->£ f,coprojectSketchMorphism $ diag ->£ f) | f <- arrows $ src diag]}
            where
                coprojectArrow a = Arrow{sourceArrow = Coprojection $ sourceArrow a, targetArrow = Coprojection $ targetArrow a, labelArrow = Coprojection $ labelArrow a}
                coprojectGraph g = unsafeGraph ((Coprojection) <$> nodes g) ((coprojectArrow) <$> edges g)
                coprojectLaw cl = Map.weakMapFromSet [(coprojectArrow <$> rp1, coprojectArrow <$> rp2) | (rp1,rp2) <- Map.mapToSet cl]
                coprojectCG cg = unsafeCompositionGraph (coprojectGraph $ support cg) (coprojectLaw $ law cg)
                coprojectCGMorphism CGMorphism{path = (a, rp),compositionLaw = cl} = CGMorphism{path = (Coprojection a, coprojectArrow <$> rp), compositionLaw = coprojectLaw cl}
                coprojectDiag d = Diagram{src = coprojectCG $ src d, tgt = coprojectCG $ tgt d, omap = (\(x,y) -> (Coprojection x, Coprojection y)) <|$|> omap d, mmap = (\(x,y) -> (coprojectCGMorphism x, coprojectCGMorphism y)) <|$|> mmap d}              
                coprojectNat nat = unsafeNaturalTransformation (coprojectDiag (source nat)) (coprojectDiag (target nat)) ((\(x,y) -> (Coprojection x, coprojectCGMorphism y)) <|$|> components nat)
                coprojectCone cone = unsafeCone (Coprojection $ apex cone) (coprojectNat $ legsCone cone)
                coprojectCocone cocone = unsafeCocone (Coprojection $ nadir cocone) (coprojectNat $ legsCocone cocone)
                coprojectDiag2 d = Diagram{src = src d, tgt = coprojectCG $ tgt d, omap = Coprojection <$> omap d, mmap = coprojectCGMorphism <$> mmap d}    
                coprojectNat2 nat = unsafeNaturalTransformation (coprojectDiag2 (source nat)) (coprojectDiag2 (target nat)) (coprojectCGMorphism <$> components nat)
                coprojectCone2 cone = unsafeCone (Coprojection $ apex cone) (coprojectNat2 $ legsCone cone)
                coprojectTripod tripod = unsafeTripod (coprojectCone2 (twoCone tripod)) (coprojectCGMorphism (evalMap tripod))
                coprojectSketch s = Sketch{underlyingCategory = coprojectCG $ underlyingCategory s, distinguishedCocones = coprojectCocone <$> distinguishedCocones s, distinguishedCones = coprojectCone <$> distinguishedCones s, distinguishedTripods = coprojectTripod <$> distinguishedTripods s}
                coprojectSketchMorphism sm = SketchMorphism{sourceSketch = coprojectSketch $ sourceSketch sm, targetSketch = coprojectSketch $ targetSketch sm, underlyingFunctor = coprojectDiag $ underlyingFunctor sm}


    
    -- | Returns a 'Lantern' found in a 'Sketch' if it can.
    containsLantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
    containsLantern s = Set.setToMaybe lanterns
        where
            lanterns = [Lantern dinstinguishedCone (bindingMorphismCone f) (bindingMorphismCone g) | dinstinguishedCone <- distinguishedCones s, cone <- ob (coneCategory (baseCone dinstinguishedCone)), f <- ar (coneCategory (baseCone dinstinguishedCone)) cone dinstinguishedCone, g <- ar (coneCategory (baseCone dinstinguishedCone)) cone dinstinguishedCone, f /= g]
            
    
    -- | Returns a 'Spotlight' found in a 'Sketch' if it can.    
    containsSpotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
    containsSpotlight s = Set.setToMaybe spotlights
        where
            spotlights = [Spotlight dinstinguishedCone i j cone | dinstinguishedCone <- distinguishedCones s, i <- ob (indexingCategoryCone dinstinguishedCone), j <- ob (indexingCategoryCone dinstinguishedCone), i /= j, (legsCone dinstinguishedCone) =>$ i == (legsCone dinstinguishedCone) =>$ j, cone <- ob (coneCategory (baseCone dinstinguishedCone)), (legsCone cone) =>$ i /= (legsCone cone) =>$ j]
    
    -- | Returns a 'CrescentMoon' found in a 'Sketch' if it can. 
    containsCrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
    containsCrescentMoon s = Set.setToMaybe crescentMoons
        where
            atLeastTwo x
                | Set.null x = False
                | Set.null (Set.filter (/= (anElement x)) x) = False
                | otherwise = True
            crescentMoons = [CrescentMoon dc1 dc2 inj c x | dc1 <- distinguishedCones s, dc2 <- distinguishedCones s, inj <- dc1 `topInjectionsCone` dc2, c <- ob (coneCategory (baseCone dc1)), x <- ob (indexingCategoryCone dc2), not ((Just $ (baseCone dc2) ->$ x) `isIn` ((fmap (baseCone dc2 ->$)) <$> ((inj |?|) <$> (ob (indexingCategoryCone dc1))))), atLeastTwo $ ar (underlyingCategory s) (apex c) (baseCone dc2 ->$ x)]
            

    -- | Returns a 'Colantern' found in a 'Sketch' if it can.
    containsColantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
    containsColantern s = Set.setToMaybe colanterns
        where
            colanterns = [Colantern dinstinguishedCocone (bindingMorphismCocone f) (bindingMorphismCocone g) | dinstinguishedCocone <- distinguishedCocones s, cocone <- ob (coconeCategory (baseCocone dinstinguishedCocone)), f <- ar (coconeCategory (baseCocone dinstinguishedCocone)) dinstinguishedCocone cocone, g <- ar (coconeCategory (baseCocone dinstinguishedCocone)) dinstinguishedCocone cocone, f /= g]
            
    
    -- | Returns a 'Cospotlight' found in a 'Sketch' if it can.    
    containsCospotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
    containsCospotlight s = Set.setToMaybe cospotlights
        where
            cospotlights = [Cospotlight dinstinguishedCocone i j cocone | dinstinguishedCocone <- distinguishedCocones s, i <- ob (indexingCategoryCocone dinstinguishedCocone), j <- ob (indexingCategoryCocone dinstinguishedCocone), i /= j, (legsCocone dinstinguishedCocone) =>$ i == (legsCocone dinstinguishedCocone) =>$ j, cocone <- ob (coconeCategory (baseCocone dinstinguishedCocone)), (legsCocone cocone) =>$ i /= (legsCocone cocone) =>$ j]
    
    -- | Returns a 'CocrescentMoon' found in a 'Sketch' if it can. 
    containsCocrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
    containsCocrescentMoon s = Set.setToMaybe cocrescentMoons
        where
            atLeastTwo x
                | Set.null x = False
                | Set.null (Set.filter (/= (anElement x)) x) = False
                | otherwise = True
            cocrescentMoons = [CocrescentMoon dcc1 dcc2 inj cc x | dcc1 <- distinguishedCocones s, dcc2 <- distinguishedCocones s, inj <- dcc1 `bottomInjectionsCocone` dcc2, cc <- ob (coconeCategory (baseCocone dcc1)), x <- ob (indexingCategoryCocone dcc2), not ((Just $ (baseCocone dcc2) ->$ x) `isIn` ((fmap (baseCocone dcc2 ->$)) <$> ((inj |?|) <$> (ob (indexingCategoryCocone dcc1))))), atLeastTwo $ ar (underlyingCategory s) (baseCocone dcc2 ->$ x) (nadir cc)]
            
    
    -- | A 'LightConstruction' is either a 'Lantern', a 'Spotlight', a 'CrescentMoon', a 'Colantern', a 'Cospotlight' or a 'CocrescentMoon'.
    --
    -- A 'Lantern' is a distinguished cone c1, and two different morphisms m1 m2 such that c1 precomposed with m1 and m2 yield the same cone.
    --
    -- A 'Spotlight' is a distinguished cone c1, two different indexing objects o1 o2 and a cone c2 such that the legs of c1 at index o1 and o2 are equal and the legs of c2 at index o1 and o2 are different.
    --
    -- A 'CrescentMoon' is a distinguished cone c1, a distinguished cone c2 such that c1 is contained in c2, a cone c with same base as c1, an indexing object x of the base of c2 not in the base of c1 such that there are at least two arrows from the apex of c to x. 
    --
    -- A 'Colantern' is a distinguished cocone c1, and two different morphisms m1 m2 such that c1 postcomposed with m1 and m2 yield the same cocone.
    --
    -- A 'Cospotlight' is a distinguished cocone c1, two different indexing objects o1 o2 and a cocone c2 such that the legs of c1 at index o1 and o2 are equal and the legs of c2 at index o1 and o2 are different.
    --
    -- A 'CocrescentMoon' is a distinguished cocone c1, a distinguished cocone c2 such that c1 is contained in c2, a cocone c with same base as c1, an indexing object x of the base of c2 not in the base of c1 such that there are at least two arrows from x to the nadir of c.
    data LightConstruction n e = 
        Lantern (ConeSketch n e) (CGMorphism n e) (CGMorphism n e) |
        Spotlight (ConeSketch n e) n n (ConeSketch n e) |
        CrescentMoon (ConeSketch n e) (ConeSketch n e) (Map n n) (ConeSketch n e) n |
        Colantern (CoconeSketch n e) (CGMorphism n e) (CGMorphism n e) |
        Cospotlight (CoconeSketch n e) n n (CoconeSketch n e) |
        CocrescentMoon (CoconeSketch n e) (CoconeSketch n e) (Map n n) (CoconeSketch n e) n
        deriving (Eq, Show, Generic, PrettyPrint, Simplifiable) 
    
    containsLightConstruction :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
    containsLightConstruction s
        | not $ null $ lant = lant
        | not $ null $ spot = spot
        | not $ null $ moon = moon
        | not $ null $ colant = colant
        | not $ null $ cospot = cospot
        | not $ null $ comoon = comoon
        | otherwise = Nothing
        where
            lant = containsLantern s
            spot = containsSpotlight s
            moon = containsCrescentMoon s
            colant = containsColantern s
            cospot = containsCospotlight s
            comoon = containsCocrescentMoon s
            
            
    
    -- -- | Return all binding morphisms from a cone to another cone with same base. If the two cones have different base, return an empty set.
    -- factorsCone :: (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) => 
        -- Cone c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2 -> Set m2
    -- factorsCone c1 c2
        -- | baseCone c1 /= baseCone c2 = set []
        -- | otherwise = [bindingMorphismCone f | f <- ar (coneCategory (baseCone c1)) c1 c2]
        
    -- -- | Return all binding morphisms from a cocone to another cocone with same base. If the two cocones have different base, return an empty set.
    -- factorsCocone :: (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) => 
        -- Cocone c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2 -> Set m2
    -- factorsCocone c1 c2
        -- | baseCocone c1 /= baseCocone c2 = set []
        -- | otherwise = [bindingMorphismCocone f | f <- ar (coconeCategory (baseCocone c1)) c1 c2]
        
    
    -- -- | Given a cone c1, return all cones c2 with same base as c1 with no factor from c1 to c2.
    -- lonelyCones :: (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) => 
        -- Cone c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
    -- lonelyCones c1 = [c2 | c2 <- ob (coneCategory (baseCone c1)), Set.null (factorsCone c2 c1)]
    
    -- -- | Given a cocone c1, return all cocones c2 with same base as c1 with no factor from c2 to c1.
    -- lonelyCocones :: (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) => 
        -- Cocone c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)
    -- lonelyCocones c1 = [c2 | c2 <- ob (coconeCategory (baseCocone c1)), Set.null (factorsCocone c1 c2)]
    
    -- -- | Return wether a set has at least two elements.
    -- atLeastTwoElement :: (Eq a) => Set a -> Bool
    -- atLeastTwoElement s = (not $ Set.null s) && (Set.or ((anElement s /=) <$> s))
    
    -- -- | Given a cone c1, return all cones c2 with same base as c1 with two or more factors from c1 to c2.
    -- crowdedCones :: (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) => 
        -- Cone c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
    -- crowdedCones c1 = [c2 | c2 <- ob (coneCategory (baseCone c1)), atLeastTwoElement (factorsCone c2 c1)]
    
    -- -- | Given a cocone c1, return all cocones c2 with same base as c1 with two or more factors from c2 to c1.
    -- crowdedCocones :: (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) => 
        -- Cocone c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)
    -- crowdedCocones c1 = [c2 | c2 <- ob (coconeCategory (baseCocone c1)), atLeastTwoElement (factorsCocone c1 c2)]
    
    -- createLonelyConeCorrectionArrow :: (ConeSketch n e -> ConeSketch n e -> e) -> ConeSketch n e -> ConeSketch n e -> Arrow n e
    -- createLonelyConeCorrectionArrow createEdge dc lc = Arrow{sourceArrow = apex lc, targetArrow = apex dc, labelArrow = createEdge dc lc}
    
    -- createLonelyCoconeCorrectionArrow :: (CoconeSketch n e -> CoconeSketch n e -> e) -> CoconeSketch n e -> CoconeSketch n e -> Arrow n e
    -- createLonelyCoconeCorrectionArrow createEdge dcc lcc = Arrow{sourceArrow = nadir dcc, targetArrow = nadir lcc, labelArrow = createEdge dcc lcc}
    
    -- -- | Add lonely cone and cocone correction arrows to a 'Sketch', return the insertion 'SketchMorphism' from the original 'Sketch' to the new 'Sketch'.
    -- addLonelinessCorrectionArrows :: (Eq n, Eq e) => (ConeSketch n e -> ConeSketch n e -> e) -> (CoconeSketch n e -> CoconeSketch n e -> e) -> Sketch n e -> SketchMorphism n e
    -- addLonelinessCorrectionArrows createEdgeCone createEdgeCocone s = SketchMorphism{sourceSketch = s, targetSketch = newSketch, underlyingFunctor = insertionFunctor}
        -- where
            -- originalCg = underlyingCategory s
            -- newCg = unsafeCompositionGraph (unsafeGraph (ob originalCg) ((edges (support originalCg)) ||| [createLonelyConeCorrectionArrow createEdgeCone dc lc | dc <- distinguishedCones s, lc <- lonelyCones dc] ||| [createLonelyCoconeCorrectionArrow createEdgeCocone dcc lcc | dcc <- distinguishedCocones s, lcc <- lonelyCocones dcc] )) (law originalCg)
            -- insertionFunctor = Diagram{src = originalCg, tgt = newCg, omap = memorizeFunction id (ob originalCg), mmap = memorizeFunction id (arrows originalCg)}
            -- newSketch = Sketch{underlyingCategory = newCg, distinguishedCones = distinguishedCones s, distinguishedCocones = distinguishedCocones s, distinguishedTripods = distinguishedTripods s}
            
    -- -- -- -- -- | Quotient arrows in the free category generated by the new graph. Return the quotient morphism.
    -- -- -- -- quotientArrows :: (Eq e, Eq n) => (ConeSketch n e -> ConeSketch n e -> e) -> (CoconeSketch n e -> CoconeSketch n e -> e) -> Sketch n e -> SketchMorphism n e
    -- -- -- -- quotientArrows createEdgeCone createEdgeCocone s = SketchMorphism{sourceSketch = s, targetSketch = newSketch, underlyingFunctor = quotientFunctor}
        -- -- -- -- where
            -- -- -- -- originalCg = underlyingCategory s
            -- -- -- -- rLonelyCones = Map.weakMapFromSet [((snd.path $ (legsCone dc) =>$ x)++[createLonelyConeCorrectionArrow createEdgeCone dc lc],(snd.path $ (legsCone lc) =>$ x)) | dc <- distinguishedCones s, lc <- lonelyCones dc, x <- ob (indexingCategoryCone dc)]
            -- -- -- -- rLonelyCocones = Map.weakMapFromSet [([createLonelyCoconeCorrectionArrow createEdgeCocone dcc lcc] ++ (snd.path $ (legsCocone dcc) =>$ x),(snd.path $ (legsCocone lcc) =>$ x)) | dcc <- distinguishedCocones s, lcc <- lonelyCocones dcc, x <- ob (indexingCategoryCocone dcc)]
            -- -- -- -- bestFactor factors = Set.minimumBy (\f g -> (length.snd.path $ f) `compare` (length.snd.path $ g)) factors
            -- -- -- -- rCrowdedCones = Map.weakMapFromSet [((snd.path $ f), (snd.path $ bestFactor (factorsCone cc dc)))| dc <- distinguishedCones s, cc <- crowdedCones dc, f <- factorsCone cc dc, f /= bestFactor (factorsCone cc dc)]
            -- -- -- -- rCrowdedCocones = Map.weakMapFromSet [((snd.path $ f), (snd.path $ bestFactor (factorsCocone dcc ccc)))| dcc <- distinguishedCocones s, ccc <- crowdedCocones dcc, f <- factorsCocone dcc ccc, f /= bestFactor (factorsCocone dcc ccc)]
            -- -- -- -- newLaw = rCrowdedCocones `Map.union` rCrowdedCones `Map.union` rLonelyCocones `Map.union` rLonelyCones -- `Map.union` (law originalCg)
            
            
            
            -- newCg = unsafeCompositionGraph (support originalCg) newLaw
            -- transformCGMorphism m
                -- | isIdentity originalCg m = identity newCg (source m)
                -- | otherwise = compose $ (unsafeArrowToCGMorphism newCg) <$> (snd $ path m) 
            -- quotientFunctor = Diagram{src = originalCg, tgt = newCg, omap = memorizeFunction id (ob originalCg), mmap = memorizeFunction transformCGMorphism (arrows originalCg)}
            -- transformDiagram d = Diagram{src = src d, tgt = newCg, omap = omap d, mmap = transformCGMorphism <$> mmap d}
            -- transformNat n = unsafeNaturalTransformation (transformDiagram $ source n) (transformDiagram $ target n) (transformCGMorphism <$> components n)
            -- transformCone c = unsafeCone (apex c) (transformNat (legsCone c))
            -- transformCocone cc = unsafeCocone (nadir cc) (transformNat (legsCocone cc))
            -- transformTripod t = unsafeTripod (transformCone (twoCone t)) (transformCGMorphism $ evalMap t)
            -- newSketch = Sketch{underlyingCategory = newCg, distinguishedCones = transformCone <$> distinguishedCones s, distinguishedCocones = transformCocone <$> distinguishedCocones s, distinguishedTripods = transformTripod <$> distinguishedTripods s}
            
            -- problème car on identifie deux flèches génératrices dans la loi de composition
            
    -- -- | A step of the Ehresmann realization algorithm.
    -- stepRealization :: (Eq e, Eq n) => (ConeSketch n e -> ConeSketch n e -> e) -> (CoconeSketch n e -> CoconeSketch n e -> e) -> Sketch n e -> SketchMorphism n e
    -- stepRealization createEdgeCone createEdgeCocone s = quotient @ addArr
        -- where
            -- addArr = addLonelinessCorrectionArrows createEdgeCone createEdgeCocone s
            -- quotient = quotientArrows createEdgeCone createEdgeCocone (target addArr)
    
    -- -- | Specialized version of 'stepRealization' for 'Text' sketches.
    -- stepRealizationText :: Sketch Text Text -> SketchMorphism Text Text
    -- stepRealizationText = stepRealization (curry (pack.show)) (curry (pack.show))