FiniteCategories-0.6.0.0: src/Math/Categories/FinSketch.hs
{-# 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,
-- * 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 '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.
checkSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e)
checkSketch 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_)) (legsCocone cocone_ <=@<- f)) `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_)) (legsCocone cocone_ <=@<- f)) `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))