{-| Module  : FiniteCategories
Description : Examples of 'ConeCategory'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of 'ConeCategory' and example of (co)limits computation.
-}
module Math.FiniteCategories.ConeCategory.Examples
(
    exampleConeCategory,
    exampleLimit,
    exampleCoconeCategory,
    exampleColimit,
)
where
    import              Math.Category
    import              Math.FiniteCategories.ConeCategory
    import              Math.FiniteCategories.FunctorCategory
    import              Math.FiniteCategories
    import              Math.FiniteCategories.FunctorCategory.Examples
    
    
    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
    
    
    -- | Example of 'ConeCategory'. Here, there are no cone as 'Square.FH' is different from 'Square.GI'.

    exampleConeCategory :: ConeCategory V VAr VOb Square SquareAr SquareOb
    exampleConeCategory :: ConeCategory V VAr VOb Square SquareAr SquareOb
exampleConeCategory = Diagram V VAr VOb Square SquareAr SquareOb
-> ConeCategory V VAr VOb Square SquareAr SquareOb
forall c1 m1 o1 c2 m2 o2.
(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) =>
Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
coneCategory Diagram V VAr VOb Square SquareAr SquareOb
exampleDiagramVToSquare
    
    -- | Example of limit computation. Here, there are no limit as 'Square.FH' is different from 'Square.GI'.

    exampleLimit :: Set (Cone V VAr VOb Square SquareAr SquareOb)
    exampleLimit :: Set (Cone V VAr VOb Square SquareAr SquareOb)
exampleLimit = Diagram V VAr VOb Square SquareAr SquareOb
-> Set (Cone V VAr VOb Square SquareAr SquareOb)
forall c1 m1 o1 c2 m2 o2.
(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) =>
Diagram c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
limits Diagram V VAr VOb Square SquareAr SquareOb
exampleDiagramVToSquare
    
    -- | Example of 'CoconeCategory'. Here, there are no cocone as 'Square.FH' is different from 'Square.GI'.

    exampleCoconeCategory :: CoconeCategory Hat HatAr HatOb Square SquareAr SquareOb
    exampleCoconeCategory :: CoconeCategory Hat HatAr HatOb Square SquareAr SquareOb
exampleCoconeCategory = Diagram Hat HatAr HatOb Square SquareAr SquareOb
-> CoconeCategory Hat HatAr HatOb Square SquareAr SquareOb
forall c1 m1 o1 c2 m2 o2.
(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) =>
Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
coconeCategory Diagram Hat HatAr HatOb Square SquareAr SquareOb
exampleDiagramHatToSquare
    
    -- | Example of colimit computation. Here, there are no colimit as 'Square.FH' is different from 'Square.GI'.

    exampleColimit :: Set (Cocone Hat HatAr HatOb Square SquareAr SquareOb)
    exampleColimit :: Set (Cocone Hat HatAr HatOb Square SquareAr SquareOb)
exampleColimit = Diagram Hat HatAr HatOb Square SquareAr SquareOb
-> Set (Cocone Hat HatAr HatOb Square SquareAr SquareOb)
forall c1 m1 o1 c2 m2 o2.
(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) =>
Diagram c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)
colimits Diagram Hat HatAr HatOb Square SquareAr SquareOb
exampleDiagramHatToSquare