Omega.hs

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

{-| Module  : FiniteCategories
Description : The category associated to the ordinal number omega is the category generated by the arrows 0 -> 1 -> 2 -> ... (See Categories for the working mathematican. Saunders Mac Lane. p.12)
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'Omega'__ linear order category is the category generated by the arrows 0 -> 1 -> 2 -> ... (See "Categories for the Working Mathematican" Saunders Mac Lane. p.12)
-}

module Math.Categories.Omega
(
    Omega(..),
    omega,
    module Math.Categories.OrdinalCategory
)
where
    import          Math.Category
    import          Math.Categories.OrdinalCategory
    import          Math.IO.PrettyPrint
    
    import          Data.WeakSet.Safe
    
    import          Numeric.Natural
    
    -- | __'Omega'__ is an 'OrdinalCategory' on natural numbers.
    type Omega = OrdinalCategory Natural
    
    -- | The __'Omega'__ category.
    --
    -- The __'Omega'__ linear order category is the category generated by the arrows 0 -> 1 -> 2 -> ... (See "Categories for the Working Mathematican" Saunders Mac Lane. p.12)
    omega :: Omega
    omega = OrdinalCategory TotalOrder