{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : By regarding each natural number as the linearly ordered set of all preceding natural number, it yields a category. __0__, __1__, __2__, __3__, ... are all number categories.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

By regarding each natural number as the linearly ordered set of all preceding natural number, it yields a category. __0__, __1__, __2__, __3__, ... are all number categories.

See (See "Categories for the Working Mathematican" Saunders Mac Lane. p.11)
-}

module Math.FiniteCategories.NumberCategory 
(
    -- * Number category

    NumberCategoryObject(..),
    NumberCategoryMorphism(..),
    IsSmallerThan(..),
    NumberCategory(..),
    numberCategory,
)
where
    import          Math.FiniteCategory
    import          Math.FiniteCategories.FullSubcategory
    import          Math.Categories.TotalOrder
    import          Math.Categories.Omega
    
    import          Numeric.Natural

    import          Data.WeakSet.Safe    
    
    -- | An object in a 'NumberCategory'.

    type NumberCategoryObject = Natural
    
    -- | A morphism in a 'NumberCategory'.

    type NumberCategoryMorphism = IsSmallerThan Natural
    
    -- | A 'NumberCategory' is an 'InheritedFullSubcategory' of __'Omega'__ containing successive numbers beginning from one.

    type NumberCategory = InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural

    -- | The 'NumberCategory' associated to a given number.

    numberCategory :: Natural -> NumberCategory
    numberCategory :: Natural -> NumberCategory
numberCategory Natural
n = (Omega -> Set Natural -> NumberCategory
forall c m o. c -> Set o -> InheritedFullSubcategory c m o
InheritedFullSubcategory Omega
omega ([Natural] -> Set Natural
forall a. [a] -> Set a
set [Natural
1..Natural
n]))