open import Level
open import Categories.Category.Core
open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Initial using (IsInitial)
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

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

  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 +₁ π₂) ⟩ }
    PNNO-universal-primitive : X × N ⇒ C
    PNNO-universal-primitive = π₁ {C} {X × N} ∘ F-Algebra-Morphism.f (IsInitial.! (PNNO⇒Initial₂ PNNO X) {A = alg})

    PNNO-universal-primitive-charak : PNNO-universal-primitive ∘ [ ⟨ id , z ∘ ! ⟩ , (id ⁂ s) ] ≈ [ zero , succ ∘ ⟨ PNNO-universal-primitive , id ⟩ ]
    PNNO-universal-primitive-charak = {!   !}

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

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