{-# OPTIONS --safe #-}

open import Categories.Category.Core
open import Categories.Object.Terminal using (Terminal)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Object.NaturalNumbers using (NNO)

import Categories.Morphism.Reasoning as MR

module Object.NaturalNumbers.Parametrized {o ℓ e} {C : Category o ℓ e}
    (cartesian : Cartesian C)
    (ℕ : NNO C (Cartesian.terminal cartesian)) where

  open Category C
  open Cartesian cartesian
  module ℕ = NNO ℕ
  open ℕ using (N; z; s; z-commute; s-commute) renaming (universal to nno-universal; η to nno-η; unique to nno-unique)
  open Equiv
  open HomReasoning
  open MR C

  -- parametrized recursion: h 0 = zero, h (n+1) = succ (h n, n)
  module _ {C} (zero : ⊤ ⇒ C) (succ : C × N ⇒ C) where

    NNO-universal-parametrized : N ⇒ C
    NNO-universal-parametrized = π₁ {C} {N} ∘ nno-universal ⟨ zero , z ⟩ ⟨ succ , s ∘ π₂ ⟩

    NNO-universal-parametrized-zero : NNO-universal-parametrized ∘ z ≈ zero
    NNO-universal-parametrized-zero = begin
      NNO-universal-parametrized ∘ z           ≈⟨ pushʳ z-commute ⟨
      π₁ ∘ ⟨ zero , z ⟩                        ≈⟨ project₁ ⟩
      zero                                     ∎

    NNO-universal-parametrized-succ : NNO-universal-parametrized ∘ s ≈ succ ∘ ⟨ NNO-universal-parametrized , id ⟩
    NNO-universal-parametrized-succ = begin
      NNO-universal-parametrized ∘ s                                                              ≈⟨ pushʳ s-commute ⟨
      π₁ ∘ ⟨ succ , s ∘ π₂ ⟩ ∘ nno-universal ⟨ zero , z ⟩ ⟨ succ , s ∘ π₂ ⟩                       ≈⟨ pullˡ project₁ ⟩
      succ ∘ nno-universal ⟨ zero , z ⟩ ⟨ succ , s ∘ π₂ ⟩                                         ≈⟨ refl⟩∘⟨ g-η ⟨
      succ ∘ ⟨ NNO-universal-parametrized , π₂ ∘ nno-universal ⟨ zero , z ⟩ ⟨ succ , s ∘ π₂ ⟩ ⟩   ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl π₂-eq ⟩
      succ ∘ ⟨ NNO-universal-parametrized , id ⟩                                                  ∎

      where
        π₂-eq : π₂ ∘ nno-universal ⟨ zero , z ⟩ ⟨ succ , s ∘ π₂ ⟩ ≈ id
        π₂-eq = nno-unique (sym project₂ ○ pushʳ z-commute) (extendʳ (sym project₂) ○ pushʳ s-commute) ○ nno-η

  s⁻¹ : N ⇒ N
  s⁻¹ = NNO-universal-parametrized z π₂

  s⁻¹-zero : s⁻¹ ∘ z ≈ z
  s⁻¹-zero = NNO-universal-parametrized-zero z π₂

  s⁻¹-succ : s⁻¹ ∘ s ≈ id
  s⁻¹-succ = NNO-universal-parametrized-succ z π₂ ○ project₂