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

Six examples of 'NumberCategory'. 
-}
module Math.FiniteCategories.NumberCategory.Examples
(
    exampleNumberCategory0,
    exampleNumberCategory1,
    exampleNumberCategory2,
    exampleNumberCategory3,
    exampleNumberCategory4,
    exampleNumberCategory5,
    exampleDiagramOfNumberCategory,
)
where
    import Math.FiniteCategories.NumberCategory
    import Math.FiniteCategory
    import Math.Categories.FunctorCategory
    import Math.Categories.Omega
    
    import Data.WeakSet
    import Data.WeakMap
    
    import Numeric.Natural
    
    -- | The category 0

    exampleNumberCategory0 :: NumberCategory
    exampleNumberCategory0 :: NumberCategory
exampleNumberCategory0 = Natural -> NumberCategory
numberCategory Natural
0
    
    -- | The category 1

    exampleNumberCategory1 :: NumberCategory
    exampleNumberCategory1 :: NumberCategory
exampleNumberCategory1 = Natural -> NumberCategory
numberCategory Natural
1
    
    -- | The category 2

    exampleNumberCategory2 :: NumberCategory
    exampleNumberCategory2 :: NumberCategory
exampleNumberCategory2 = Natural -> NumberCategory
numberCategory Natural
2
    
    -- | The category 3

    exampleNumberCategory3 :: NumberCategory
    exampleNumberCategory3 :: NumberCategory
exampleNumberCategory3 = Natural -> NumberCategory
numberCategory Natural
3
    
    
    -- | The category 4

    exampleNumberCategory4 :: NumberCategory
    exampleNumberCategory4 :: NumberCategory
exampleNumberCategory4 = Natural -> NumberCategory
numberCategory Natural
4
    
    
    -- | The category 5

    exampleNumberCategory5:: NumberCategory
    exampleNumberCategory5 :: NumberCategory
exampleNumberCategory5 = Natural -> NumberCategory
numberCategory Natural
5
    
    -- | An example of 'Diagram' from 3 to 'Omega'.

    exampleDiagramOfNumberCategory :: Diagram NumberCategory (IsSmallerThan Natural) Natural Omega (IsSmallerThan Natural) Natural
    exampleDiagramOfNumberCategory :: Diagram
  NumberCategory
  (IsSmallerThan Natural)
  Natural
  Omega
  (IsSmallerThan Natural)
  Natural
exampleDiagramOfNumberCategory = Diagram
  NumberCategory
  (IsSmallerThan Natural)
  Natural
  Omega
  (IsSmallerThan Natural)
  Natural
diag
        where
            diag :: Diagram
  NumberCategory
  (IsSmallerThan Natural)
  Natural
  Omega
  (IsSmallerThan Natural)
  Natural
diag = Diagram{src :: NumberCategory
src = Natural -> NumberCategory
numberCategory Natural
3, tgt :: Omega
tgt = Omega
omega, omap :: Map Natural Natural
omap = (Natural -> Natural) -> Set Natural -> Map Natural Natural
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Natural -> Natural
forall a. a -> a
id (NumberCategory -> Set Natural
forall c m o. FiniteCategory c m o => c -> Set o
ob (NumberCategory -> Set Natural) -> NumberCategory -> Set Natural
forall a b. (a -> b) -> a -> b
$ Natural -> NumberCategory
numberCategory Natural
3), mmap :: Map (IsSmallerThan Natural) (IsSmallerThan Natural)
mmap = (IsSmallerThan Natural -> IsSmallerThan Natural)
-> Set (IsSmallerThan Natural)
-> Map (IsSmallerThan Natural) (IsSmallerThan Natural)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction IsSmallerThan Natural -> IsSmallerThan Natural
forall a. a -> a
id (NumberCategory -> Set (IsSmallerThan Natural)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (NumberCategory -> Set (IsSmallerThan Natural))
-> NumberCategory -> Set (IsSmallerThan Natural)
forall a b. (a -> b) -> a -> b
$ Natural -> NumberCategory
numberCategory Natural
3)}