open import Categories.Category.Core
open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Initial using (Initial)
open import Categories.Category.Cocartesian using (BinaryCoproducts)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Object.NaturalNumbers using (NNO)
open import Categories.Functor.Core
open import Categories.Functor.Algebra

import Categories.Morphism.Reasoning as MR

-- open import Categories.Category.Construction.F-Algebras

module Object.NaturalNumbers.Primitive {o ℓ e} {C : Category o ℓ e} (cartesian : Cartesian C) (coproducts : BinaryCoproducts C) (ℕ : NNO C (Cartesian.terminal cartesian)) where
  open Category C
  open Cartesian cartesian
  open BinaryProducts products
  open Terminal terminal
  open BinaryCoproducts coproducts
  module ℕ = NNO ℕ
  open ℕ using (N; z; s)
  open import Categories.Object.NaturalNumbers.Properties.F-Algebras C terminal coproducts
  open Equiv
  open HomReasoning
  open MR C


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

    NNO-universal-primitive : N ⇒ C
    NNO-universal-primitive = π₁ {C} {N} ∘ F-Algebra-Morphism.f (Initial.! (NNO⇒Initial ℕ) {A = alg})

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

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

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