Natural numbers object in a precategory

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

Created on 2022-11-29.
Last modified on 2024-04-11.

module category-theory.natural-numbers-object-precategories where
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


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)

  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) 
      ( 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))

  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)

    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 :
        ( 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' , α , β))

Recent changes