Copyright | Guillaume Sabbagh 2022 |
---|---|
License | GPL-3 |
Maintainer | guillaumesabbagh@protonmail.com |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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)
Synopsis
- type NumberCategoryObject = Natural
- type NumberCategoryMorphism = IsSmallerThan Natural
- data IsSmallerThan a = IsSmallerThan a a
- type NumberCategory = InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural
- numberCategory :: Natural -> NumberCategory
Number category
type NumberCategoryObject = Natural Source #
An object in a NumberCategory
.
type NumberCategoryMorphism = IsSmallerThan Natural Source #
A morphism in a NumberCategory
.
data IsSmallerThan a Source #
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.
IsSmallerThan a a |
Instances
type NumberCategory = InheritedFullSubcategory Omega (IsSmallerThan Natural) Natural Source #
A NumberCategory
is an InheritedFullSubcategory
of Omega
containing successive numbers beginning from one.
numberCategory :: Natural -> NumberCategory Source #
The NumberCategory
associated to a given number.