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

Examples of 'CommaCategory'.
-}
module Math.FiniteCategories.CommaCategory.Examples
(
    exampleSlice,
    exampleCoslice,
    exampleArrowCategory,
)
where
    import Math.Categories
    import Math.FiniteCategories
    
    -- | Example of slice category : (Id_4 | 2). This is the category of objects over 2 in the simplex category 4.

    exampleSlice :: CommaCategory NumberCategory NumberCategoryMorphism NumberCategoryObject One One One NumberCategory NumberCategoryMorphism NumberCategoryObject
    Just CommaCategory
  NumberCategory
  NumberCategoryMorphism
  NumberCategoryObject
  One
  One
  One
  NumberCategory
  NumberCategoryMorphism
  NumberCategoryObject
exampleSlice = NumberCategory
-> NumberCategoryObject
-> Maybe
     (CommaCategory
        NumberCategory
        NumberCategoryMorphism
        NumberCategoryObject
        One
        One
        One
        NumberCategory
        NumberCategoryMorphism
        NumberCategoryObject)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
c -> o -> Maybe (CommaCategory c m o One One One c m o)
sliceCategory (NumberCategoryObject -> NumberCategory
numberCategory NumberCategoryObject
4) NumberCategoryObject
2
    
    -- | Example of coslice category : (2 | Id_4). This is the category of objects under 2 in the simplex category 4.

    exampleCoslice :: CommaCategory One One One NumberCategory NumberCategoryMorphism NumberCategoryObject NumberCategory NumberCategoryMorphism NumberCategoryObject
    Just CommaCategory
  One
  One
  One
  NumberCategory
  NumberCategoryMorphism
  NumberCategoryObject
  NumberCategory
  NumberCategoryMorphism
  NumberCategoryObject
exampleCoslice = NumberCategory
-> NumberCategoryObject
-> Maybe
     (CommaCategory
        One
        One
        One
        NumberCategory
        NumberCategoryMorphism
        NumberCategoryObject
        NumberCategory
        NumberCategoryMorphism
        NumberCategoryObject)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
c -> o -> Maybe (CommaCategory One One One c m o c m o)
cosliceCategory (NumberCategoryObject -> NumberCategory
numberCategory NumberCategoryObject
4) NumberCategoryObject
2
    
    -- | Example of arrow category : (Id_4 | Id_4). This is the category of arrows of the simplex category 4.

    exampleArrowCategory :: CommaCategory NumberCategory NumberCategoryMorphism NumberCategoryObject NumberCategory NumberCategoryMorphism NumberCategoryObject NumberCategory NumberCategoryMorphism NumberCategoryObject
    exampleArrowCategory :: CommaCategory
  NumberCategory
  NumberCategoryMorphism
  NumberCategoryObject
  NumberCategory
  NumberCategoryMorphism
  NumberCategoryObject
  NumberCategory
  NumberCategoryMorphism
  NumberCategoryObject
exampleArrowCategory = NumberCategory
-> CommaCategory
     NumberCategory
     NumberCategoryMorphism
     NumberCategoryObject
     NumberCategory
     NumberCategoryMorphism
     NumberCategoryObject
     NumberCategory
     NumberCategoryMorphism
     NumberCategoryObject
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
c -> CommaCategory c m o c m o c m o
arrowCategory (NumberCategoryObject -> NumberCategory
numberCategory NumberCategoryObject
4)