{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Core
open import Categories.Object.Terminal hiding (up-to-iso)

module Categories.Object.NaturalNumbers {o β„“ e} (π’ž : Category o β„“ e) (π’ž-Terminal : Terminal π’ž) where

open import Level

open import Categories.Morphism π’ž
open import Categories.Morphism.Reasoning π’ž

open Category π’ž
open HomReasoning
open Equiv

open Terminal π’ž-Terminal

record IsNNO (N : Obj) : Set (o βŠ” β„“ βŠ” e) where
  field
    z : ⊀ β‡’ N
    s : N β‡’ N
    universal : βˆ€ {A} β†’ ⊀ β‡’ A β†’ A β‡’ A β†’ N β‡’ A
    z-commute : βˆ€ {A} {q : ⊀ β‡’ A} {f : A β‡’ A} β†’ q β‰ˆ universal q f ∘ z
    s-commute : βˆ€ {A} {q : ⊀ β‡’ A} {f : A β‡’ A} β†’ f ∘ universal q f β‰ˆ universal q f ∘ s
    unique    : βˆ€ {A} {q : ⊀ β‡’ A} {f : A β‡’ A} {u : N β‡’ A} β†’ q β‰ˆ u ∘ z β†’ f ∘ u β‰ˆ u ∘ s β†’ u β‰ˆ universal q f

  Ξ· : universal z s β‰ˆ id
  η = ⟺ (unique (⟺ identityˑ) id-comm)

  universal-cong : βˆ€ {A} β†’ {f fβ€² : ⊀ β‡’ A} β†’ {g gβ€² : A β‡’ A} β†’ f β‰ˆ fβ€² β†’ g β‰ˆ gβ€² β†’ universal f g β‰ˆ universal fβ€² gβ€²
  universal-cong fβ‰ˆfβ€² gβ‰ˆgβ€² = unique (⟺ fβ‰ˆfβ€² β—‹  z-commute) (∘-resp-β‰ˆΛ‘ (⟺ gβ‰ˆgβ€²) β—‹ s-commute)

record NNO : Set (o βŠ” β„“ βŠ” e) where
  field
    N : Obj
    isNNO : IsNNO N

  open IsNNO isNNO public

open NNO

module _ (N : NNO) (Nβ€² : NNO) where
  private
    module N = NNO N
    module Nβ€² = NNO Nβ€²

  up-to-iso : N.N β‰… Nβ€².N
  up-to-iso = record
    { from = N.universal Nβ€².z Nβ€².s
    ; to = Nβ€².universal N.z N.s
    ; iso = record
      { isoΛ‘ = universal-∘ N Nβ€²
      ; isoΚ³ = universal-∘ Nβ€² N
      }
    }
    where
      universal-∘ : βˆ€ (N Nβ€² : NNO) β†’ universal Nβ€² (z N) (s N) ∘ universal N (z Nβ€²) (s Nβ€²) β‰ˆ id
      universal-∘ N Nβ€² = unique N (z-commute Nβ€² β—‹ pushΚ³ (z-commute N)) (pullΛ‘ (s-commute Nβ€²) β—‹ assoc β—‹ ∘-resp-β‰ˆΚ³ (s-commute N) β—‹ ⟺ assoc) β—‹ (Ξ· N)