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

open import Level
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.Category.Cocartesian using (BinaryCoproducts)
open import Categories.Category.CartesianClosed using (CartesianClosed)

-- In CCCs every NNO is a PNNO

module Categories.Object.NaturalNumbers.Properties.Parametrized {o  e} (𝒞 : Category o  e) (𝒞-CartesianClosed : CartesianClosed 𝒞) (𝒞-Coproducts : BinaryCoproducts 𝒞) where

open Category 𝒞
open CartesianClosed 𝒞-CartesianClosed using (cartesian; λg; eval′; β′; λ-inj; λ-cong; η-exp′; λ-unique′; subst)
open Cartesian cartesian using (terminal; products)
open BinaryProducts products renaming (unique′ to bp-unique′)
open Terminal terminal

open import Categories.Object.NaturalNumbers 𝒞 terminal using (NNO)
open import Categories.Object.NaturalNumbers.Parametrized 𝒞 cartesian using (ParametrizedNNO)
open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞

open HomReasoning
open Equiv

NNO×CCC⇒PNNO : NNO  ParametrizedNNO
NNO×CCC⇒PNNO nno = record
  { N = N
  ; isParametrizedNNO = record
    { z = z
    ; s = s
    ; universal = λ {A} {X} f g  (eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap
    ; commute₁ = commute₁'
    ; commute₂ = commute₂'
    ; unique = unique'
    }
  }
  where
  open NNO nno renaming (unique to nno-unique)

  commute₁' :  {A X} {f : A  X} {g : X  X}  f  ((eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap)   id , z  ! 
  commute₁' {A} {X} {f} {g} = begin
    f                                                                                   ≈⟨ introʳ project₂ 
    f  π₂   ! , id                                                                  ≈⟨ pullˡ ( β′) 
    (eval′  (λg (f  π₂)  id))   ! , id                                            ≈⟨ pullʳ ⁂∘⟨⟩ 
    eval′   λg (f  π₂)  ! , id  id                                                ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ˡ z-commute) 
    eval′   (universal (λg (f  π₂)) (λg (g  eval′))  z)  ! , id  id             ≈⟨ refl⟩∘⟨ (⟨⟩-congʳ assoc   ⁂∘⟨⟩) 
    eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id)   z  ! , id             ≈⟨ sym-assoc  pushʳ ( swap∘⟨⟩) 
    ((eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap)   id , z  !  

  commute₂' :  {A X} {f : A  X} {g : X  X}
     g  ((eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap)  ((eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap)  (id  s)
  commute₂' {A} {X} {f} {g} = begin
    g  (eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap                       ≈⟨ pullˡ (pullˡ ( β′)) 
    ((eval′  (λg (g  eval′)  id))  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap ≈⟨ (pullʳ ⁂∘⁂) ⟩∘⟨refl 
    (eval′  (λg (g  eval′)   universal (λg (f  π₂)) (λg (g  eval′))  id  id))  swap    ≈⟨ (refl⟩∘⟨ (⁂-cong₂ s-commute refl)) ⟩∘⟨refl 
    (eval′  (universal (λg (f  π₂))  (λg (g  eval′))  s  id  id))  swap                 ≈⟨ (refl⟩∘⟨ ( ⁂∘⁂)) ⟩∘⟨refl 
    (eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id)  (s  id))  swap                ≈⟨ pullʳ (pullʳ ( swap∘⁂)) 
    eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id)  swap  (id  s)                  ≈⟨ sym-assoc  sym-assoc 
    ((eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap)  (id  s)              

  unique' :  {A X} {f : A  X} {g : X  X} {u : A × N  X}
     f  u   id , z  !   g  u  u  (id  s)  u  (eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap
  unique' {A} {X} {f} {g} {u} eqᶻ eqˢ = swap-epi _ _ (λ-inj (begin
    λg (u  swap)                                                                  ≈⟨ nno-unique ( z-commutes) s-commutes 
    universal (λg (f  π₂)) (λg (g  eval′))                                       ≈˘⟨ η-exp′ 
    λg (eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))                   ≈˘⟨ λ-cong (cancelʳ swap∘swap) 
    λg (((eval′  (universal (λg (f  π₂)) (λg (g  eval′))  id))  swap)  swap) ))
    where
    z-commutes : λg (u  swap)  z  λg (f  π₂)
    z-commutes = λ-unique′ (begin
      eval′  (λg (u  swap)  z  id)        ≈˘⟨ refl⟩∘⟨ (⁂∘⁂  ⁂-cong₂ refl identity²) 
      eval′  (λg (u  swap)  id)  (z  id) ≈⟨ extendʳ β′ 
      u  swap  (z  id)                     ≈⟨ refl⟩∘⟨ swap∘⁂ 
      u  (id  z)  swap                     ≈⟨ refl⟩∘⟨ (bp-unique′ π₁-commutes π₂-commutes) 
      u   id , z  !   π₂                 ≈⟨ pullˡ ( eqᶻ) 
      f  π₂                                  )
      where
      π₁-commutes : π₁  (id  z)  swap  π₁   id , z  !   π₂
      π₁-commutes = begin
        π₁  (id  z)  swap     ≈⟨ extendʳ project₁  identityˡ 
        π₁  swap                ≈⟨ project₁ 
        π₂                       ≈˘⟨ cancelˡ project₁ 
        π₁   id , z  !   π₂ 
      π₂-commutes : π₂  (id  z)  swap  π₂   id , z  !   π₂
      π₂-commutes = begin
        π₂  (id  z)  swap     ≈⟨ extendʳ project₂ 
        z  π₂  swap            ≈⟨ refl⟩∘⟨ project₂ 
        z  π₁                   ≈⟨ refl⟩∘⟨ !-unique₂ 
        z  !  π₂               ≈˘⟨ extendʳ project₂ 
        π₂   id , z  !   π₂ 
    s-commutes : λg (g  eval′)  λg (u  swap)  λg (u  swap)  s
    s-commutes = begin
      λg (g  eval′)  λg (u  swap)          ≈⟨ subst 
      λg ((g  eval′)  (λg (u  swap)  id)) ≈⟨ λ-cong (pullʳ β′  pullˡ eqˢ) 
      λg ((u  (id  s))  swap)              ≈⟨ λ-cong (pullʳ ( swap∘⁂)  sym-assoc) 
      λg ((u  swap)  (s  id))              ≈˘⟨ subst 
      λg (u  swap)  s