Copyright	Guillaume Sabbagh 2022
License	GPL-3
Maintainer	guillaumesabbagh@protonmail.com
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Math.Categories.FinSketch

Contents

Types for Sketch
Sketch
Sketch morphism,
The category of finite sketches
Functions for shiny sketches
Ehresmann realization

Description

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.

Synopsis

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)
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
constructTwoConeFromTripod :: (Eq n, Eq e) => n -> n -> TripodSketch n e -> ConeSketch n e
constructTwoConeFromTripodText :: TripodSketch Text Text -> ConeSketch Text Text
data Sketch n e
underlyingCategory :: Sketch n e -> CategorySketch n e
supportSketch :: Sketch n e -> Graph n e
distinguishedCones :: Sketch n e -> Set (ConeSketch n e)
distinguishedCocones :: Sketch n e -> Set (CoconeSketch n e)
distinguishedTripods :: Sketch n e -> Set (TripodSketch n e)
unsafeSketch :: CategorySketch n e -> Set (ConeSketch n e) -> Set (CoconeSketch n e) -> Set (TripodSketch n e) -> Sketch n e
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)
sketchText :: CategorySketch Text Text -> Set (ConeSketch Text Text) -> Set (CoconeSketch Text Text) -> Set (TripodSketch Text Text) -> Either (SketchError Text Text) (Sketch Text Text)
checkSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e)
checkFiniteSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e)
data SketchMorphism n e
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)
underlyingFunctor :: SketchMorphism n e -> FunctorSketch n e
unsafeSketchMorphism :: Sketch n e -> Sketch n e -> FunctorSketch n e -> SketchMorphism n e
sketchMorphism :: (Eq n, Eq e) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Either (SketchMorphismError n e) (SketchMorphism n e)
canFunctorBePromotedIntoSketchMorphism :: (Eq e, Eq n) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Bool
data FinSketch n e = FinSketch
containsLantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
containsSpotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
containsCrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
containsColantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
containsCospotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
containsCocrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)
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
containsLightConstruction :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e)

Types for Sketch

type CategorySketch n e = CompositionGraph n e Source #

type ArrowSketch n e = CGMorphism n e Source #

type ObjectSketch n e = n Source #

type ConeSketch n e = Cone (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) Source #

type CoconeSketch n e = Cocone (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) Source #

type TripodSketch n e = Tripod (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) Source #

data SketchError n e Source #

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.

Constructors

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

Instances

Instances details

(PrettyPrint n, PrettyPrint e, Eq e, Eq n) => PrettyPrint (SketchError n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods pprint :: Int -> SketchError n e -> String Source # pprintWithIndentations :: Int -> Int -> String -> SketchError n e -> String Source # pprintIndent :: Int -> SketchError n e -> String Source #
(Simplifiable n, Simplifiable e, Eq e, Eq n) => Simplifiable (SketchError n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods simplify :: SketchError n e -> SketchError n e #
Generic (SketchError n e) Source #
Instance details Defined in Math.Categories.FinSketch Associated Types type Rep (SketchError n e) :: Type -> Type Methods from :: SketchError n e -> Rep (SketchError n e) x to :: Rep (SketchError n e) x -> SketchError n e
(Show e, Show n) => Show (SketchError n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods showsPrec :: Int -> SketchError n e -> ShowS show :: SketchError n e -> String showList :: [SketchError n e] -> ShowS
(Eq e, Eq n) => Eq (SketchError n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods (==) :: SketchError n e -> SketchError n e -> Bool (/=) :: SketchError n e -> SketchError n e -> Bool
type Rep (SketchError n e) Source #
Instance details Defined in Math.Categories.FinSketch type Rep (SketchError n e) = D1 ('MetaData "SketchError" "Math.Categories.FinSketch" "FiniteCategories-0.6.4.0-inplace" 'False) ((C1 ('MetaCons "BaseOfConeIsNotInUnderlyingCategory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConeSketch n e))) :+: (C1 ('MetaCons "BaseOfCoconeIsNotInUnderlyingCategory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CoconeSketch n e))) :+: C1 ('MetaCons "BaseOfTripodIsNotInUnderlyingCategory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TripodSketch n e))))) :+: (C1 ('MetaCons "TripodTwoConeDoesNotBelongToDistinguishedCones" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TripodSketch n e))) :+: (C1 ('MetaCons "UnderlyingCategoryError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FiniteCategoryError (ArrowSketch n e) (ObjectSketch n e)))) :+: C1 ('MetaCons "TwoSameIndexingObjects" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n)))))

constructTwoConeFromTripod :: (Eq n, Eq e) => n -> n -> TripodSketch n e -> ConeSketch n e Source #

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).

constructTwoConeFromTripodText :: TripodSketch Text Text -> ConeSketch Text Text Source #

Specialized version of constructTwoConeFromTripod for Sketch of Text.

Sketch

data Sketch n e Source #

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).

Instances

Instances details

(PrettyPrint n, PrettyPrint e, Eq n, Eq e) => PrettyPrint (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods pprint :: Int -> Sketch n e -> String Source # pprintWithIndentations :: Int -> Int -> String -> Sketch n e -> String Source # pprintIndent :: Int -> Sketch n e -> String Source #
(Simplifiable n, Simplifiable e, Eq n, Eq e) => Simplifiable (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods simplify :: Sketch n e -> Sketch n e #
Generic (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Associated Types type Rep (Sketch n e) :: Type -> Type Methods from :: Sketch n e -> Rep (Sketch n e) x to :: Rep (Sketch n e) x -> Sketch n e
(Show n, Show e) => Show (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods showsPrec :: Int -> Sketch n e -> ShowS show :: Sketch n e -> String showList :: [Sketch n e] -> ShowS
(Eq n, Eq e) => Eq (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods (==) :: Sketch n e -> Sketch n e -> Bool (/=) :: Sketch n e -> Sketch n e -> Bool
(Eq e, Eq n) => Morphism (SketchMorphism n e) (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods (@) :: SketchMorphism n e -> SketchMorphism n e -> SketchMorphism n e Source # (@?) :: SketchMorphism n e -> SketchMorphism n e -> Maybe (SketchMorphism n e) Source # source :: SketchMorphism n e -> Sketch n e Source # target :: SketchMorphism n e -> Sketch n e Source #
(Eq e, Eq n) => Category (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods identity :: FinSketch n e -> Sketch n e -> SketchMorphism n e Source # ar :: FinSketch n e -> Sketch n e -> Sketch n e -> Set (SketchMorphism n e) Source # genAr :: FinSketch n e -> Sketch n e -> Sketch n e -> Set (SketchMorphism n e) Source # decompose :: FinSketch n e -> SketchMorphism n e -> [SketchMorphism n e] Source #
(Eq e, Eq n) => HasCoequalizers (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods coequalize :: Diagram Parallel ParallelAr ParallelOb (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Cocone Parallel ParallelAr ParallelOb (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
(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 Source #
Instance details Defined in Math.Categories.FinSketch Methods colimit :: Diagram cIndex mIndex oIndex (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Cocone cIndex mIndex oIndex (FinSketch (Colimit oIndex n) (Colimit oIndex e)) (SketchMorphism (Colimit oIndex n) (Colimit oIndex e)) (Sketch (Colimit oIndex n) (Colimit oIndex e)) Source # coprojectBase :: Diagram cIndex mIndex oIndex (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Diagram (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)) Source #
type Rep (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch type Rep (Sketch n e) = D1 ('MetaData "Sketch" "Math.Categories.FinSketch" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "Sketch" 'PrefixI 'True) ((S1 ('MetaSel ('Just "underlyingCategory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CategorySketch n e)) :: S1 ('MetaSel ('Just "distinguishedCones") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set (ConeSketch n e)))) :: (S1 ('MetaSel ('Just "distinguishedCocones") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set (CoconeSketch n e))) :*: S1 ('MetaSel ('Just "distinguishedTripods") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set (TripodSketch n e))))))

Getters

underlyingCategory :: Sketch n e -> CategorySketch n e Source #

supportSketch :: Sketch n e -> Graph n e Source #

The support of a Sketch is the multidigraph generating the underlying category of the Sketch.

distinguishedCones :: Sketch n e -> Set (ConeSketch n e) Source #

distinguishedCocones :: Sketch n e -> Set (CoconeSketch n e) Source #

distinguishedTripods :: Sketch n e -> Set (TripodSketch n e) Source #

Smart constructors

unsafeSketch :: CategorySketch n e -> Set (ConeSketch n e) -> Set (CoconeSketch n e) -> Set (TripodSketch n e) -> Sketch n e Source #

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.

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) Source #

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.

sketchText :: CategorySketch Text Text -> Set (ConeSketch Text Text) -> Set (CoconeSketch Text Text) -> Set (TripodSketch Text Text) -> Either (SketchError Text Text) (Sketch Text Text) Source #

Specialized version of sketch for sketches of Text.

Helpers

checkSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e) Source #

Check wether a Sketch is well formed or not, return a SketchError if it is malformed, Nothing otherwise. Does not check the underlying CompositionGraph.

checkFiniteSketch :: (Eq n, Eq e) => Sketch n e -> Maybe (SketchError n e) Source #

Check wether a finite Sketch is well formed or not, return a SketchError if it is malformed, Nothing otherwise.

Sketch morphism,

data SketchMorphism n e Source #

SketchMorphism is private, use the smart constructor sketchMorphism or unsafeSketchMorphism to construct one.

Instances

Instances details

(PrettyPrint e, PrettyPrint n, Eq e, Eq n) => PrettyPrint (SketchMorphism n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods pprint :: Int -> SketchMorphism n e -> String Source # pprintWithIndentations :: Int -> Int -> String -> SketchMorphism n e -> String Source # pprintIndent :: Int -> SketchMorphism n e -> String Source #
(Simplifiable e, Simplifiable n, Eq e, Eq n) => Simplifiable (SketchMorphism n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods simplify :: SketchMorphism n e -> SketchMorphism n e #
Generic (SketchMorphism n e) Source #
Instance details Defined in Math.Categories.FinSketch Associated Types type Rep (SketchMorphism n e) :: Type -> Type Methods from :: SketchMorphism n e -> Rep (SketchMorphism n e) x to :: Rep (SketchMorphism n e) x -> SketchMorphism n e
(Show e, Show n) => Show (SketchMorphism n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods showsPrec :: Int -> SketchMorphism n e -> ShowS show :: SketchMorphism n e -> String showList :: [SketchMorphism n e] -> ShowS
(Eq e, Eq n) => Eq (SketchMorphism n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods (==) :: SketchMorphism n e -> SketchMorphism n e -> Bool (/=) :: SketchMorphism n e -> SketchMorphism n e -> Bool
(Eq e, Eq n) => Morphism (SketchMorphism n e) (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods (@) :: SketchMorphism n e -> SketchMorphism n e -> SketchMorphism n e Source # (@?) :: SketchMorphism n e -> SketchMorphism n e -> Maybe (SketchMorphism n e) Source # source :: SketchMorphism n e -> Sketch n e Source # target :: SketchMorphism n e -> Sketch n e Source #
(Eq e, Eq n) => Category (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods identity :: FinSketch n e -> Sketch n e -> SketchMorphism n e Source # ar :: FinSketch n e -> Sketch n e -> Sketch n e -> Set (SketchMorphism n e) Source # genAr :: FinSketch n e -> Sketch n e -> Sketch n e -> Set (SketchMorphism n e) Source # decompose :: FinSketch n e -> SketchMorphism n e -> [SketchMorphism n e] Source #
(Eq e, Eq n) => HasCoequalizers (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods coequalize :: Diagram Parallel ParallelAr ParallelOb (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Cocone Parallel ParallelAr ParallelOb (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
(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 Source #
Instance details Defined in Math.Categories.FinSketch Methods colimit :: Diagram cIndex mIndex oIndex (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Cocone cIndex mIndex oIndex (FinSketch (Colimit oIndex n) (Colimit oIndex e)) (SketchMorphism (Colimit oIndex n) (Colimit oIndex e)) (Sketch (Colimit oIndex n) (Colimit oIndex e)) Source # coprojectBase :: Diagram cIndex mIndex oIndex (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Diagram (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)) Source #
type Rep (SketchMorphism n e) Source #
Instance details Defined in Math.Categories.FinSketch type Rep (SketchMorphism n e)

data SketchMorphismError n e Source #

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.

Constructors

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)

Instances

Instances details

(PrettyPrint n, PrettyPrint e, Eq e, Eq n) => PrettyPrint (SketchMorphismError n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods pprint :: Int -> SketchMorphismError n e -> String Source # pprintWithIndentations :: Int -> Int -> String -> SketchMorphismError n e -> String Source # pprintIndent :: Int -> SketchMorphismError n e -> String Source #
(Simplifiable n, Simplifiable e, Eq e, Eq n) => Simplifiable (SketchMorphismError n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods simplify :: SketchMorphismError n e -> SketchMorphismError n e #
Generic (SketchMorphismError n e) Source #
Instance details Defined in Math.Categories.FinSketch Associated Types type Rep (SketchMorphismError n e) :: Type -> Type Methods from :: SketchMorphismError n e -> Rep (SketchMorphismError n e) x to :: Rep (SketchMorphismError n e) x -> SketchMorphismError n e
(Show n, Show e) => Show (SketchMorphismError n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods showsPrec :: Int -> SketchMorphismError n e -> ShowS show :: SketchMorphismError n e -> String showList :: [SketchMorphismError n e] -> ShowS
(Eq n, Eq e) => Eq (SketchMorphismError n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods (==) :: SketchMorphismError n e -> SketchMorphismError n e -> Bool (/=) :: SketchMorphismError n e -> SketchMorphismError n e -> Bool
type Rep (SketchMorphismError n e) Source #
Instance details Defined in Math.Categories.FinSketch type Rep (SketchMorphismError n e) = D1 ('MetaData "SketchMorphismError" "Math.Categories.FinSketch" "FiniteCategories-0.6.4.0-inplace" 'False) ((C1 ('MetaCons "ConeNotSentToACone" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConeSketch n e))) :+: (C1 ('MetaCons "CoconeNotSentToACocone" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CoconeSketch n e))) :+: C1 ('MetaCons "TripodNotSentToATripod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TripodSketch n e))))) :+: (C1 ('MetaCons "UnderlyingFunctorError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (DiagramError (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e) (CategorySketch n e) (ArrowSketch n e) (ObjectSketch n e)))) :+: (C1 ('MetaCons "WrongSource" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CategorySketch n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CategorySketch n e))) :+: C1 ('MetaCons "WrongTarget" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CategorySketch n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CategorySketch n e))))))

Getter

underlyingFunctor :: SketchMorphism n e -> FunctorSketch n e Source #

Underlying functor of a SketchMorphism.

Smart constructors

unsafeSketchMorphism :: Sketch n e -> Sketch n e -> FunctorSketch n e -> SketchMorphism n e Source #

Unsafe constructor for a SketchMorphism. Use with caution, prefer sketch which checks the structure of the SketchMorphism.

sketchMorphism :: (Eq n, Eq e) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Either (SketchMorphismError n e) (SketchMorphism n e) Source #

Smart constructor for a SketchMorphism. It checks wether cones are sent to cones and cocones are sent to cocones.

Other functions

canFunctorBePromotedIntoSketchMorphism :: (Eq e, Eq n) => Sketch n e -> Sketch n e -> FunctorSketch n e -> Bool Source #

Return wether a Functor can be promoted into a SketchMorphism.

The category of finite sketches

data FinSketch n e Source #

Constructors

FinSketch

Instances

Instances details

PrettyPrint (FinSketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods pprint :: Int -> FinSketch n e -> String Source # pprintWithIndentations :: Int -> Int -> String -> FinSketch n e -> String Source # pprintIndent :: Int -> FinSketch n e -> String Source #
Simplifiable (FinSketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods simplify :: FinSketch n e -> FinSketch n e #
Generic (FinSketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Associated Types type Rep (FinSketch n e) :: Type -> Type Methods from :: FinSketch n e -> Rep (FinSketch n e) x to :: Rep (FinSketch n e) x -> FinSketch n e
Show (FinSketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods showsPrec :: Int -> FinSketch n e -> ShowS show :: FinSketch n e -> String showList :: [FinSketch n e] -> ShowS
Eq (FinSketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods (==) :: FinSketch n e -> FinSketch n e -> Bool (/=) :: FinSketch n e -> FinSketch n e -> Bool
(Eq e, Eq n) => Category (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods identity :: FinSketch n e -> Sketch n e -> SketchMorphism n e Source # ar :: FinSketch n e -> Sketch n e -> Sketch n e -> Set (SketchMorphism n e) Source # genAr :: FinSketch n e -> Sketch n e -> Sketch n e -> Set (SketchMorphism n e) Source # decompose :: FinSketch n e -> SketchMorphism n e -> [SketchMorphism n e] Source #
(Eq e, Eq n) => HasCoequalizers (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods coequalize :: Diagram Parallel ParallelAr ParallelOb (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Cocone Parallel ParallelAr ParallelOb (FinSketch n e) (SketchMorphism n e) (Sketch n e) Source #
(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 Source #
Instance details Defined in Math.Categories.FinSketch Methods colimit :: Diagram cIndex mIndex oIndex (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Cocone cIndex mIndex oIndex (FinSketch (Colimit oIndex n) (Colimit oIndex e)) (SketchMorphism (Colimit oIndex n) (Colimit oIndex e)) (Sketch (Colimit oIndex n) (Colimit oIndex e)) Source # coprojectBase :: Diagram cIndex mIndex oIndex (FinSketch n e) (SketchMorphism n e) (Sketch n e) -> Diagram (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)) Source #
type Rep (FinSketch n e) Source #
Instance details Defined in Math.Categories.FinSketch type Rep (FinSketch n e) = D1 ('MetaData "FinSketch" "Math.Categories.FinSketch" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "FinSketch" 'PrefixI 'False) (U1 :: Type -> Type))

Functions for shiny sketches

containsLantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #

Returns a Lantern found in a Sketch if it can.

containsSpotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #

Returns a Spotlight found in a Sketch if it can.

containsCrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #

Returns a CrescentMoon found in a Sketch if it can.

containsColantern :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #

Returns a Colantern found in a Sketch if it can.

containsCospotlight :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #

Returns a Cospotlight found in a Sketch if it can.

containsCocrescentMoon :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #

Returns a CocrescentMoon found in a Sketch if it can.

data LightConstruction n e Source #

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.

Constructors

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

Instances

Instances details

(PrettyPrint n, PrettyPrint e, Eq e, Eq n) => PrettyPrint (LightConstruction n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods pprint :: Int -> LightConstruction n e -> String Source # pprintWithIndentations :: Int -> Int -> String -> LightConstruction n e -> String Source # pprintIndent :: Int -> LightConstruction n e -> String Source #
(Simplifiable n, Simplifiable e, Eq e, Eq n) => Simplifiable (LightConstruction n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods simplify :: LightConstruction n e -> LightConstruction n e #
Generic (LightConstruction n e) Source #
Instance details Defined in Math.Categories.FinSketch Associated Types type Rep (LightConstruction n e) :: Type -> Type Methods from :: LightConstruction n e -> Rep (LightConstruction n e) x to :: Rep (LightConstruction n e) x -> LightConstruction n e
(Show e, Show n) => Show (LightConstruction n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods showsPrec :: Int -> LightConstruction n e -> ShowS show :: LightConstruction n e -> String showList :: [LightConstruction n e] -> ShowS
(Eq e, Eq n) => Eq (LightConstruction n e) Source #
Instance details Defined in Math.Categories.FinSketch Methods (==) :: LightConstruction n e -> LightConstruction n e -> Bool (/=) :: LightConstruction n e -> LightConstruction n e -> Bool
type Rep (LightConstruction n e) Source #
Instance details Defined in Math.Categories.FinSketch type Rep (LightConstruction n e) = D1 ('MetaData "LightConstruction" "Math.Categories.FinSketch" "FiniteCategories-0.6.4.0-inplace" 'False) ((C1 ('MetaCons "Lantern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConeSketch n e)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CGMorphism n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CGMorphism n e)))) :+: (C1 ('MetaCons "Spotlight" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConeSketch n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConeSketch n e)))) :+: C1 ('MetaCons "CrescentMoon" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConeSketch n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConeSketch n e))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map n n)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConeSketch n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n)))))) :+: (C1 ('MetaCons "Colantern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CoconeSketch n e)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CGMorphism n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CGMorphism n e)))) :+: (C1 ('MetaCons "Cospotlight" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CoconeSketch n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CoconeSketch n e)))) :+: C1 ('MetaCons "CocrescentMoon" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CoconeSketch n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CoconeSketch n e))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map n n)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CoconeSketch n e)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n)))))))

containsLightConstruction :: (Eq n, Eq e) => Sketch n e -> Maybe (LightConstruction n e) Source #

Types for Sketch

Instances

Sketch

Instances

Getters

Smart constructors

Helpers

Sketch morphism,

Instances

Instances

Getter

Smart constructors

Other functions

The category of finite sketches

Instances

Functions for shiny sketches

Instances

Ehresmann realization