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