Natural numbers object in a precategory

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

Imports

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

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unique-existence
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-object-Precategory C)
  where

  is-natural-numbers-object-Precategory :
    (n : obj-Precategory C) →
    type-hom-Precategory C t n → type-hom-Precategory C n n → UU (l1 ⊔ l2)
  is-natural-numbers-object-Precategory n z s =
    (x : obj-Precategory C)
    (q : type-hom-Precategory C t x)
    (f : type-hom-Precategory C x x) →
    ∃! (type-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 →
    Σ (type-hom-Precategory C t n) λ z →
    Σ (type-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-object-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 :
    type-hom-Precategory C t object-natural-numbers-object-Precategory
  zero-natural-numbers-object-Precategory = pr1 (pr2 nno)

  succ-natural-numbers-object-Precategory :
    type-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 : type-hom-Precategory C t x)
    (f : type-hom-Precategory C x x)
    where

    morphism-natural-numbers-object-Precategory :
      type-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' :
        type-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' , α , β))