Math.FiniteCategories.NumberCategory

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)

Number category

type NumberCategoryObject = Natural

An object in a NumberCategory.

type NumberCategoryMorphism = IsSmallerThan Natural

A morphism in a NumberCategory.

data IsSmallerThan a

IsSmallerThan is the type of morphisms in a linear order, it reminds the fact that there is a morphism from a source to a target iff the source is smaller than the target.

Constructors

IsSmallerThan a a

Instances

PrettyPrint a => PrettyPrint (IsSmallerThan a)

Defined in Math.Categories.TotalOrder

Methods

pprint :: IsSmallerThan a -> String

Show a => Show (IsSmallerThan a)

Defined in Math.Categories.TotalOrder

Methods

showsPrec :: Int -> IsSmallerThan a -> ShowS

show :: IsSmallerThan a -> String

showList :: [IsSmallerThan a] -> ShowS

Eq a => Eq (IsSmallerThan a)

Defined in Math.Categories.TotalOrder

Methods

(==) :: IsSmallerThan a -> IsSmallerThan a -> Bool

(/=) :: IsSmallerThan a -> IsSmallerThan a -> Bool

Eq a => Morphism (IsSmallerThan a) a

Defined in Math.Categories.TotalOrder

Methods

(@?) :: IsSmallerThan a -> IsSmallerThan a -> Maybe (IsSmallerThan a)

source :: IsSmallerThan a -> a

target :: IsSmallerThan a -> a

(Enum a, Ord a) => Category (OrdinalCategory a) (IsSmallerThan a) a

Defined in Math.Categories.OrdinalCategory

Methods

identity :: OrdinalCategory a -> a -> IsSmallerThan a

ar :: OrdinalCategory a -> a -> a -> Set (IsSmallerThan a)

genAr :: OrdinalCategory a -> a -> a -> Set (IsSmallerThan a)

decompose :: OrdinalCategory a -> IsSmallerThan a -> [IsSmallerThan a]

(Eq a, Ord a) => Category (TotalOrder a) (IsSmallerThan a) a

Defined in Math.Categories.TotalOrder

Methods

identity :: TotalOrder a -> a -> IsSmallerThan a

ar :: TotalOrder a -> a -> a -> Set (IsSmallerThan a)

genAr :: TotalOrder a -> a -> a -> Set (IsSmallerThan a)

decompose :: TotalOrder a -> IsSmallerThan a -> [IsSmallerThan a]

type NumberCategory = InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural

A NumberCategory is an InheritedFullSubcategory of Omega containing successive numbers beginning from one.

numberCategory :: Natural -> NumberCategory

The NumberCategory associated to a given number.