# Natural numbers object in a precategory

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-11-29.

module category-theory.natural-numbers-object-precategories where

Imports
open import category-theory.precategories
open import category-theory.terminal-objects-precategories

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.uniqueness-quantification
open import foundation.universe-levels


## Idea

Let C be a precategory with a terminal object t. A natural numbers object in C is an object n with morphisms z : hom t n and s : hom n n such that for any object x and morphisms q : hom t x and f : hom x x there exists a unique u : hom n x such that:

• u ∘ z = q
• u ∘ s = f ∘ u.
module _
{l1 l2 : Level} (C : Precategory l1 l2)
((t , _) : terminal-obj-Precategory C)
where

is-natural-numbers-object-Precategory :
(n : obj-Precategory C) →
hom-Precategory C t n → hom-Precategory C n n → UU (l1 ⊔ l2)
is-natural-numbers-object-Precategory n z s =
(x : obj-Precategory C)
(q : hom-Precategory C t x)
(f : hom-Precategory C x x) →
uniquely-exists-structure
( hom-Precategory C n x)
( λ u →
( comp-hom-Precategory C u z ＝ q) ×
( comp-hom-Precategory C u s ＝ comp-hom-Precategory C f u))

natural-numbers-object-Precategory : UU (l1 ⊔ l2)
natural-numbers-object-Precategory =
Σ (obj-Precategory C) λ n →
Σ (hom-Precategory C t n) λ z →
Σ (hom-Precategory C n n) λ s →
is-natural-numbers-object-Precategory n z s

module _
{l1 l2 : Level} (C : Precategory l1 l2)
((t , p) : terminal-obj-Precategory C)
(nno : natural-numbers-object-Precategory C (t , p))
where

object-natural-numbers-object-Precategory : obj-Precategory C
object-natural-numbers-object-Precategory = pr1 nno

zero-natural-numbers-object-Precategory :
hom-Precategory C t object-natural-numbers-object-Precategory
zero-natural-numbers-object-Precategory = pr1 (pr2 nno)

succ-natural-numbers-object-Precategory :
hom-Precategory C
( object-natural-numbers-object-Precategory)
( object-natural-numbers-object-Precategory)
succ-natural-numbers-object-Precategory = pr1 (pr2 (pr2 nno))

module _
(x : obj-Precategory C)
(q : hom-Precategory C t x)
(f : hom-Precategory C x x)
where

morphism-natural-numbers-object-Precategory :
hom-Precategory C object-natural-numbers-object-Precategory x
morphism-natural-numbers-object-Precategory =
pr1 (pr1 (pr2 (pr2 (pr2 nno)) x q f))

morphism-natural-numbers-object-Precategory-zero-comm :
comp-hom-Precategory C morphism-natural-numbers-object-Precategory
( zero-natural-numbers-object-Precategory) ＝ q
morphism-natural-numbers-object-Precategory-zero-comm =
pr1 (pr2 (pr1 (pr2 (pr2 (pr2 nno)) x q f)))

morphism-natural-numbers-object-Precategory-succ-comm :
comp-hom-Precategory
( C)
( morphism-natural-numbers-object-Precategory)
( succ-natural-numbers-object-Precategory) ＝
comp-hom-Precategory (C) (f) (morphism-natural-numbers-object-Precategory)
morphism-natural-numbers-object-Precategory-succ-comm =
pr2 (pr2 (pr1 (pr2 (pr2 (pr2 nno)) x q f)))

is-unique-morphism-natural-numbers-object-Precategory :
( u' :
hom-Precategory C object-natural-numbers-object-Precategory x) →
comp-hom-Precategory C u' zero-natural-numbers-object-Precategory ＝ q →
comp-hom-Precategory C u' succ-natural-numbers-object-Precategory ＝
comp-hom-Precategory C f u' →
morphism-natural-numbers-object-Precategory ＝ u'
is-unique-morphism-natural-numbers-object-Precategory u' α β =
ap pr1 (pr2 (pr2 (pr2 (pr2 nno)) x q f) (u' , α , β))