{-# OPTIONS --safe #-}

open import Level
open import Categories.Category.Core
open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Initial using (IsInitial; Initial)
open import Categories.Category.Construction.F-Algebras
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cocartesian using (BinaryCoproducts)
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Functor.Algebra
open import Categories.Functor.Core

import Categories.Morphism.Reasoning as MR

module Object.NaturalNumbers.Parametrized.Primitive {o ℓ e} {C : Category o ℓ e} (cartesian : Cartesian C) (coproducts : BinaryCoproducts C) (PNNO : ParametrizedNNO C cartesian) where
  open Category C
  open Cartesian cartesian
  open BinaryProducts products
  open BinaryCoproducts coproducts
  open ParametrizedNNO PNNO
  open import Categories.Object.NaturalNumbers.Parametrized.Properties.F-Algebras C cartesian coproducts
  open Terminal terminal using (⊤; !)
  open HomReasoning
  open MR C
  open Equiv

  module _ {X C : Obj} (zero : X ⇒ C) (succ : C × (X × N) ⇒ C) where
    private
      alg : F-Algebra (X +-)
      alg = record { A = C × (X × N) ; α = ⟨ [ zero , succ ] , [ ⟨ id , z ∘ ! ⟩ , (id ⁂ s) ] ∘ (id +₁ π₂) ⟩ }

    prec : X × N ⇒ C
    prec = π₁ {C} {X × N} ∘ F-Algebra-Morphism.f (IsInitial.! (PNNO⇒Initial₂ PNNO X) {A = alg})

    prec-charak : prec ∘ [ ⟨ id , z ∘ ! ⟩ , (id ⁂ s) ] ≈ [ zero , succ ∘ ⟨ prec , id ⟩ ]
    prec-charak = begin 
      (π₁ ∘ ⟦ ¡ ⟧) ∘ [ ⟨ id , z ∘ ! ⟩ , (id ⁂ s) ]                                        ≈⟨ pullʳ (commutes ¡) ⟩ 
      π₁ ∘ ⟨ [ zero , succ ] , [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ (id +₁ π₂) ⟩ ∘ (id +₁ ⟦ ¡ ⟧) ≈⟨ pullˡ project₁ ⟩ 
      [ zero , succ ] ∘ (id +₁ ⟦ ¡ ⟧)                                                     ≈⟨ []∘+₁ ⟩ 
      [ zero ∘ id , succ ∘ ⟦ ¡ ⟧ ]                                                        ≈⟨ []-cong₂ identityʳ (∘-resp-≈ʳ helper) ⟩ 
      [ zero , succ ∘ ⟨ prec , id ⟩ ]                                 ∎
      where
      open Initial (record { ⊥ = PNNO-Algebra X N z s ; ⊥-is-initial = (PNNO⇒Initial₂ PNNO X) }) using () renaming (! to ¡; !-unique to ¡-unique)
      open F-Algebra-Morphism using (commutes) renaming (f to ⟦_⟧)
      helper : ⟦ ¡ ⟧ ≈ ⟨ prec , id ⟩
      helper = begin 
        ⟦ ¡ ⟧ 
          ≈˘⟨ g-η ⟩ 
        ⟨ prec , π₂ ∘ ⟦ ¡ ⟧ ⟩ 
          ≈˘⟨ ⟨⟩-cong₂ refl (¡-unique (record { f = π₂ ∘ ⟦ ¡ ⟧ ; commutes = commutes' })) ⟩ 
        ⟨ prec , ⟦ ¡ {A = record { A = X × N ; α = [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] }} ⟧ ⟩ 
          ≈⟨ ⟨⟩-cong₂ refl (¡-unique (record { f = id ; commutes = id-comm-sym ○ ∘-resp-≈ʳ (sym (Functor.identity (X +-))) })) ⟩
        ⟨ prec , id ⟩ ∎
        where
          commutes' : (π₂ ∘ ⟦ ¡ {A = alg} ⟧) ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ≈ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ (id +₁ π₂ ∘ ⟦ ¡ {A = alg} ⟧)
          commutes' = begin 
            (π₂ ∘ ⟦ ¡ ⟧) ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]                                          ≈⟨ pullʳ (commutes (¡ {A = alg})) ⟩ 
            π₂ ∘ ⟨ [ zero , succ ] , [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ (id +₁ π₂) ⟩ ∘ (id +₁ ⟦ ¡ ⟧) ≈⟨ extendʳ project₂ ⟩ 
            [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ (id +₁ π₂) ∘ (id +₁ ⟦ ¡ ⟧)                            ≈⟨ refl⟩∘⟨ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩ 
            [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ (id +₁ π₂ ∘ ⟦ ¡ {A = alg} ⟧)                          ∎

    prec-zero : prec ∘ ⟨ id , z ∘ ! ⟩ ≈ zero
    prec-zero = begin 
      prec ∘ ⟨ id , z ∘ ! ⟩                     ≈˘⟨ refl⟩∘⟨ inject₁ ⟩ 
      prec ∘ [ ⟨ id , z ∘ ! ⟩ , (id ⁂ s) ] ∘ i₁ ≈⟨ pullˡ prec-charak ⟩
      [ zero , succ ∘ ⟨ prec , id ⟩ ] ∘ i₁      ≈⟨ inject₁ ⟩
      zero                                                          ∎

    prec-succ : prec ∘ (id ⁂ s) ≈ succ ∘ ⟨ prec , id ⟩
    prec-succ = begin 
      prec ∘ (id ⁂ s)                           ≈˘⟨ refl⟩∘⟨ inject₂ ⟩
      prec ∘ [ ⟨ id , z ∘ ! ⟩ , (id ⁂ s) ] ∘ i₂ ≈⟨ pullˡ prec-charak ⟩ 
      [ zero , succ ∘ ⟨ prec , id ⟩ ] ∘ i₂      ≈⟨ inject₂ ⟩ 
      succ ∘ ⟨ prec , id ⟩                      ∎