open import Categories.Category.Core
open import Categories.Category.Cartesian
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.BinaryProducts
open import Categories.Object.Terminal

import Categories.Morphism.Reasoning as MR


module Misc.PrimitiveRecursion {o β„“ e} {π’ž : Category o β„“ e} (cartesian : Cartesian π’ž) (PNNO : ParametrizedNNO π’ž cartesian) where
  open Cartesian cartesian
  open Category π’ž
  open MR π’ž
  open Equiv
  open HomReasoning
  open ParametrizedNNO PNNO
  open BinaryProducts products renaming (unique to ⟨⟩-unique; Ξ· to ⁂-Ξ·)
  open Terminal terminal using (!; !-unique)

  Ο†' : βˆ€ {X Y : Obj} β†’ X β‡’ Y β†’ Y Γ— X Γ— N β‡’ Y β†’ X Γ— N β‡’ Y Γ— X Γ— N
  Ο†' {X} {Y} f g = universal {X = Y Γ— X Γ— N} ⟨ f , ⟨ id , z ∘ ! ⟩ ⟩ ⟨ g , ⟨ π₁ ∘ Ο€β‚‚ , s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ⟩


  p-rec : βˆ€ {X Y : Obj} β†’ X β‡’ Y β†’ Y Γ— (X Γ— N) β‡’ Y β†’ X Γ— N β‡’ Y
  p-rec {X} {Y} f g = π₁ ∘ Ο†' f g

  p-rec-IB : βˆ€ {X Y : Obj} (f : X β‡’ Y) (g : Y Γ— X Γ— N β‡’ Y) β†’ p-rec f g ∘ ⟨ id , z ∘ ! ⟩ β‰ˆ f
  p-rec-IB {X} {Y} f g = (pullΚ³ (sym commute₁)) β—‹ project₁

  p-rec-IS : βˆ€ {X Y : Obj} (f : X β‡’ Y) (g : Y Γ— X Γ— N β‡’ Y) β†’ p-rec f g ∘ ( id ⁂ s ) β‰ˆ g ∘ Ο†' f g
  p-rec-IS {X} {Y} f g = (pullΚ³ (sym commuteβ‚‚)) β—‹ pullΛ‘ project₁

  Ο€β‚βˆ˜Ο€β‚‚βˆ˜Ο†' : βˆ€ {X Y : Obj} (f : X β‡’ Y) (g : Y Γ— X Γ— N β‡’ Y) β†’ π₁ ∘ Ο€β‚‚ ∘ Ο†' f g β‰ˆ π₁
  Ο€β‚βˆ˜Ο€β‚‚βˆ˜Ο†' f g = begin 
    π₁ ∘ Ο€β‚‚ ∘ Ο†' f g β‰ˆβŸ¨ unique (sym zero₁) (sym succ₁) ⟩ 
    universal id id β‰ˆβŸ¨ sym (unique (sym project₁) (sym Ο€β‚βˆ˜β‚)) ⟩ 
    π₁ ∎
    where
      zero₁ : (π₁ ∘ Ο€β‚‚ ∘ Ο†' f g) ∘ ⟨ id , z ∘ ! ⟩ β‰ˆ id
      zero₁ = begin 
        (π₁ ∘ Ο€β‚‚ ∘ Ο†' f g) ∘ ⟨ id , z ∘ ! ⟩ β‰ˆβŸ¨ pullΚ³ (pullΚ³ (sym commute₁)) ⟩ 
        π₁ ∘ Ο€β‚‚ ∘ ⟨ f , ⟨ id , z ∘ ! ⟩ ⟩    β‰ˆβŸ¨ refl⟩∘⟨ projectβ‚‚ ⟩ 
        π₁ ∘ ⟨ id , z ∘ ! ⟩                 β‰ˆβŸ¨ project₁ ⟩ 
        id                                  ∎
      succ₁ : (π₁ ∘ Ο€β‚‚ ∘ Ο†' f g) ∘ (id ⁂ s) β‰ˆ id ∘ π₁ ∘ Ο€β‚‚ ∘ Ο†' f g
      succ₁ = begin 
        (π₁ ∘ Ο€β‚‚ ∘ Ο†' f g) ∘ (id ⁂ s)                        β‰ˆβŸ¨ pullΚ³ (pullΚ³ (sym commuteβ‚‚)) ⟩ 
        π₁ ∘ Ο€β‚‚ ∘ ⟨ g , ⟨ π₁ ∘ Ο€β‚‚ , s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ⟩ ∘ Ο†' f g β‰ˆβŸ¨ refl⟩∘⟨ pullΛ‘ projectβ‚‚ ⟩ 
        π₁ ∘ ⟨ π₁ ∘ Ο€β‚‚ , s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∘ Ο†' f g              β‰ˆβŸ¨ pullΛ‘ project₁ ⟩ 
        (π₁ ∘ Ο€β‚‚) ∘ Ο†' f g                                   β‰ˆβŸ¨ (sym identityΛ‘) β—‹ refl⟩∘⟨ assoc ⟩
        id ∘ π₁ ∘ Ο€β‚‚ ∘ Ο†' f g                                ∎

  Ο€β‚‚βˆ˜Ο€β‚‚βˆ˜Ο†' : βˆ€ {X Y : Obj} (f : X β‡’ Y) (g : Y Γ— X Γ— N β‡’ Y) β†’ Ο€β‚‚ ∘ Ο€β‚‚ ∘ Ο†' f g β‰ˆ Ο€β‚‚
  Ο€β‚‚βˆ˜Ο€β‚‚βˆ˜Ο†' f g = begin 
    Ο€β‚‚ ∘ Ο€β‚‚ ∘ Ο†' f g β‰ˆβŸ¨ unique (sym zero₁) (sym succ₁) ⟩ 
    universal (z ∘ !) s β‰ˆβŸ¨ sym (unique (sym projectβ‚‚) (sym Ο€β‚‚βˆ˜β‚)) ⟩ 
    Ο€β‚‚ ∎
    where
      zero₁ : (Ο€β‚‚ ∘ Ο€β‚‚ ∘ Ο†' f g) ∘ ⟨ id , z ∘ ! ⟩ β‰ˆ z ∘ !
      zero₁ = begin 
        (Ο€β‚‚ ∘ Ο€β‚‚ ∘ Ο†' f g) ∘ ⟨ id , z ∘ ! ⟩ β‰ˆβŸ¨ pullΚ³ (pullΚ³ (sym commute₁)) ⟩ 
        Ο€β‚‚ ∘ Ο€β‚‚ ∘ ⟨ f , ⟨ id , z ∘ ! ⟩ ⟩    β‰ˆβŸ¨ refl⟩∘⟨ projectβ‚‚ ⟩ 
        Ο€β‚‚ ∘ ⟨ id , z ∘ ! ⟩                 β‰ˆβŸ¨ projectβ‚‚ ⟩ 
        z ∘ !                               ∎
      succ₁ : (Ο€β‚‚ ∘ Ο€β‚‚ ∘ Ο†' f g) ∘ (id ⁂ s) β‰ˆ s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ∘ Ο†' f g
      succ₁ = begin 
        (Ο€β‚‚ ∘ Ο€β‚‚ ∘ Ο†' f g) ∘ (id ⁂ s)                        β‰ˆβŸ¨ pullΚ³ (pullΚ³ (sym commuteβ‚‚)) ⟩ 
        Ο€β‚‚ ∘ Ο€β‚‚ ∘ ⟨ g , ⟨ π₁ ∘ Ο€β‚‚ , s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ⟩ ∘ Ο†' f g β‰ˆβŸ¨ refl⟩∘⟨ pullΛ‘ projectβ‚‚ ⟩ 
        Ο€β‚‚ ∘ ⟨ π₁ ∘ Ο€β‚‚ , s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∘ Ο†' f g              β‰ˆβŸ¨ pullΛ‘ projectβ‚‚ ⟩ 
        (s ∘ Ο€β‚‚ ∘ Ο€β‚‚) ∘ Ο†' f g                               β‰ˆβŸ¨ assocΒ²Ξ²Ξ΅ ⟩
        s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ∘ Ο†' f g                                 ∎

  Ο†'-charac : βˆ€ {X Y : Obj} (f : X β‡’ Y) (g : Y Γ— X Γ— N β‡’ Y) β†’ Ο†' f g β‰ˆ ⟨ p-rec f g , ⟨ π₁ , Ο€β‚‚ ⟩ ⟩
  Ο†'-charac f g = sym (⟨⟩-unique refl (sym (⟨⟩-unique (Ο€β‚βˆ˜Ο€β‚‚βˆ˜Ο†' f g) (Ο€β‚‚βˆ˜Ο€β‚‚βˆ˜Ο†' f g))))

  p-induction : βˆ€ {X Y : Obj} (f : X β‡’ Y) (g : Y Γ— X Γ— N β‡’ Y) (w : X Γ— N β‡’ Y) β†’ f β‰ˆ w ∘ ⟨ id , z ∘ ! ⟩ β†’ g ∘ ⟨ w , id ⟩ β‰ˆ w ∘ (id ⁂ s) β†’ p-rec f g β‰ˆ w
  p-induction {X} {Y} f g w eq₁ eqβ‚‚ = begin 
    π₁ ∘ Ο†' f g β‰ˆβŸ¨ refl⟩∘⟨ (sym (unique zero₁ succ₁)) ⟩
    π₁ ∘ w'     β‰ˆβŸ¨ project₁ ⟩
    w           ∎
    where
      w' : X Γ— N β‡’ Y Γ— X Γ— N
      w' = ⟨ w , id ⟩
      zero₁ : ⟨ f , ⟨ id , z ∘ ! ⟩ ⟩ β‰ˆ w' ∘ ⟨ id , z ∘ ! ⟩
      zero₁ = sym (begin 
        w' ∘ ⟨ id , z ∘ ! ⟩                          β‰ˆβŸ¨ ⟨⟩∘ ⟩ 
        ⟨ w ∘ ⟨ id , z ∘ ! ⟩ , id ∘ ⟨ id , z ∘ ! ⟩ ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ (sym eq₁) identityΛ‘ ⟩ 
        ⟨ f , ⟨ id , z ∘ ! ⟩ ⟩                       ∎)
      succ₁ : ⟨ g , ⟨ π₁ ∘ Ο€β‚‚ , s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ⟩ ∘ ⟨ w , id ⟩ β‰ˆ ⟨ w , id ⟩ ∘ (id ⁂ s)
      succ₁ = begin 
        ⟨ g , ⟨ π₁ ∘ Ο€β‚‚ , s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ⟩ ∘ ⟨ w , id ⟩                               β‰ˆβŸ¨ ⟨⟩∘ ⟩ 
        ⟨ g ∘ ⟨ w , id ⟩ , ⟨ π₁ ∘ Ο€β‚‚ , s ∘ Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∘ ⟨ w , id ⟩ ⟩                  β‰ˆβŸ¨ ⟨⟩-congβ‚‚ refl ⟨⟩∘ ⟩ 
        ⟨ g ∘ ⟨ w , id ⟩ , ⟨ (π₁ ∘ Ο€β‚‚) ∘ ⟨ w , id ⟩ , (s ∘ Ο€β‚‚ ∘ Ο€β‚‚) ∘ ⟨ w , id ⟩ ⟩ ⟩ β‰ˆβŸ¨ ⟨⟩-congβ‚‚ eqβ‚‚ (⟨⟩-congβ‚‚ (cancelΚ³ projectβ‚‚) (pullΚ³ (cancelΚ³ projectβ‚‚))) ⟩ 
        ⟨ w ∘ (id ⁂ s) , ⟨ π₁ , s ∘ Ο€β‚‚ ⟩ ⟩                                           β‰ˆβŸ¨ ⟨⟩-congβ‚‚ refl (⟨⟩-congβ‚‚ (sym identityΛ‘) refl β—‹ sym β‚βˆ˜βŸ¨βŸ©) ⟩ 
        ⟨ w ∘ (id ⁂ s) , (id ⁂ s) ∘ ⟨ π₁ , Ο€β‚‚ ⟩ ⟩                                    β‰ˆβŸ¨ ⟨⟩-congβ‚‚ refl (elimΚ³ ⁂-Ξ·) ⟩ 
        ⟨ w ∘ (id ⁂ s) , (id ⁂ s) ⟩                                                  β‰ˆβŸ¨ ⟨⟩-congβ‚‚ refl (sym identityΛ‘) β—‹ sym ⟨⟩∘ ⟩ 
        ⟨ w , id ⟩ ∘ (id ⁂ s)                                                        ∎