{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

{-| 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 n = (InheritedFullSubcategory omega (set [1..n]))