open import Function.Base using (_$_)
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.Object.NaturalNumbers using (NNO)
open import Categories.Object.NaturalNumbers.Parametrized

import Categories.Morphism.Reasoning as MR

module Object.NaturalNumbers.Parametrized.Primitive {o ℓ e} {C : Category o ℓ e}
  (cartesian : Cartesian C)
  (PNNO : ParametrizedNNO C cartesian) where

  open Category C
  open Cartesian cartesian
  open ParametrizedNNO PNNO renaming (unique to pnno-unique; η to pnno-η; uniform to pnno-uniform)
  open NNO (Categories.Object.NaturalNumbers.Parametrized.PNNO⇒NNO C cartesian PNNO) using () renaming (unique to nno-unique; universal to nno-universal)
  open import Object.NaturalNumbers.Parametrized cartesian (Categories.Object.NaturalNumbers.Parametrized.PNNO⇒NNO C cartesian PNNO) using (s⁻¹; s⁻¹-succ; s⁻¹-zero)

  open HomReasoning
  open MR C
  open Equiv

  module _ {X C : Obj} (zero : X ⇒ C) (succ : C × X × N ⇒ C) where

    -- primitive recursion
    prec : X × N ⇒ C
    prec = π₁ ∘ universal ⟨ zero , ⟨ id , z ∘ ! ⟩ ⟩  ⟨ succ , (id ×₁ s) ∘ π₂ ⟩

  module _ {X C : Obj} {zero : X ⇒ C} {succ : C × X × N ⇒ C} where

    prec-zero : prec zero succ ∘ ⟨ id , z ∘ ! ⟩ ≈ zero
    prec-zero = begin
      prec zero succ ∘ ⟨ id , z ∘ ! ⟩            ≈⟨ pushʳ commute₁ ⟨
      π₁ ∘ ⟨ zero , ⟨ id , z ∘ ! ⟩ ⟩             ≈⟨ project₁ ⟩
      zero                                       ∎

    prec-zero' : ∀ {f : X ⇒ X} → prec zero succ ∘ ⟨ f , z ∘ ! ⟩ ≈ zero ∘ f
    prec-zero' {f} = begin
      prec zero succ ∘ ⟨ f , z ∘ ! ⟩             ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟨
      prec zero succ ∘ ⟨ id , z ∘ ! ⟩ ∘ f        ≈⟨ pullˡ prec-zero ⟩
      zero ∘ f                                   ∎

    prec-succ : prec zero succ ∘ (id ×₁ s) ≈ succ ∘ ⟨ prec zero succ , id ⟩
    prec-succ = begin
      prec zero succ ∘ (id ×₁ s)                                                                   ≈⟨ pushʳ commute₂ ⟨
      π₁ ∘ ⟨ succ , second s ∘ π₂ ⟩ ∘ universal ⟨ zero , ⟨ id , z ∘ ! ⟩ ⟩ ⟨ succ , second s ∘ π₂ ⟩ ≈⟨ pullˡ project₁ ⟩
      succ ∘ universal ⟨ zero , ⟨ id , z ∘ ! ⟩ ⟩ ⟨ succ , (id ×₁ s) ∘ π₂ ⟩                         ≈⟨ refl⟩∘⟨ unique refl π₂-eq ⟨
      succ ∘ ⟨ prec zero succ , id ⟩                                                               ∎

      where
        π₂-eq : π₂ ∘ universal ⟨ zero , ⟨ id , z ∘ ! ⟩ ⟩ ⟨ succ , (id ×₁ s) ∘ π₂ ⟩ ≈ id
        π₂-eq = pnno-uniform project₂ ○ universal-cong project₂ refl ○ pnno-η

    -- uniqueness: prec zero succ is the unique h satisfying prec-zero and prec-succ
    prec-unique : {h : X × N ⇒ C} → h ∘ ⟨ id , z ∘ ! ⟩ ≈ zero → h ∘ (id ×₁ s) ≈ succ ∘ ⟨ h , id ⟩ → h ≈ prec zero succ
    prec-unique {h = h} h-zero h-succ = sym project₁ ○ ∘-resp-≈ʳ (pnno-unique eq₁ eq₂)
       where
         eq₁ = begin
           ⟨ _ , ⟨ id , z ∘ ! ⟩ ⟩                       ≈⟨ ⟨⟩-cong₂ h-zero identityˡ ⟨
           ⟨ h ∘ ⟨ id , z ∘ ! ⟩ , id ∘ ⟨ id , z ∘ ! ⟩ ⟩ ≈⟨ ⟨⟩∘ ⟨
           ⟨ h , id ⟩ ∘ ⟨ id , z ∘ ! ⟩                  ∎

         eq₂ = begin
           ⟨ _ , (id ×₁ s) ∘ π₂ ⟩ ∘ ⟨ h , id ⟩                ≈⟨ ⟨⟩∘ ⟩
           ⟨ _ ∘ ⟨ h , id ⟩ , ((id ×₁ s) ∘ π₂) ∘ ⟨ h , id ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ h-succ (id-comm-sym ○ pushʳ (sym project₂)) ⟨
           ⟨ h ∘ (id ×₁ s) , id ∘ (id ×₁ s) ⟩                 ≈⟨ ⟨⟩∘ ⟨
           ⟨ h , id ⟩ ∘ (id ×₁ s)                             ∎

  prec-natural : {X C : Obj} {zero : X ⇒ C} {succ : C × X × N ⇒ C} {Y : Obj} {h : Y ⇒ X}
    → prec zero succ ∘ (h ×₁ id) ≈ prec (zero ∘ h) (succ ∘ (id ×₁ h ×₁ id) )

  prec-natural {zero = zero} {succ = succ} {h = h} = prec-unique eq-z (eq-s ○ sym-assoc)
    where
      eq-z : (prec zero succ ∘ (h ×₁ id)) ∘ ⟨ id , z ∘ ! ⟩ ≈ zero ∘ h
      eq-z = begin
        (prec zero succ ∘ (h ×₁ id)) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
        prec zero succ ∘ ⟨ h , z ∘ ! ⟩                ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (∘-resp-≈ʳ (!-unique₂)) ⟩
        prec zero succ ∘ ⟨ h , z ∘ ! ∘ h ⟩            ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ assoc) ⟨
        prec zero succ ∘ ⟨ id , z ∘ ! ⟩ ∘ h           ≈⟨ pullˡ prec-zero ⟩
        zero ∘ h                                      ∎

      eq-s : (prec zero succ ∘ (h ×₁ id)) ∘ (id ×₁ s) ≈ succ ∘ (id ×₁ h ×₁ id) ∘ ⟨ prec zero succ ∘ (h ×₁ id) , id ⟩
      eq-s = begin
        (prec zero succ ∘ (h ×₁ id)) ∘ (id ×₁ s)                     ≈⟨ extendˡ first↔second ⟩
        (prec zero succ ∘ (id ×₁ s)) ∘ (h ×₁ id)                     ≈⟨ pushˡ prec-succ ⟩
        succ ∘ ⟨ prec zero succ , id ⟩ ∘ (h ×₁ id)                   ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ identityˡ) ⟩
        succ ∘ ⟨ prec zero succ ∘ (h ×₁ id) , h ×₁ id ⟩              ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟨ 
        succ ∘ (id ×₁ h ×₁ id) ∘ ⟨ prec zero succ ∘ (h ×₁ id) , id ⟩ ∎

  prec-η : {X C : Obj} (zero : X ⇒ C) → prec zero π₁ ≈ zero ∘ π₁
  prec-η zero = sym $ prec-unique (cancelʳ project₁) $ begin
      (zero ∘ π₁) ∘ (id ×₁ s) ≈⟨ pullʳ π₁∘second ⟩
      zero ∘ π₁               ≈⟨ project₁ ⟨
      π₁ ∘ ⟨ zero ∘ π₁ , id ⟩ ∎

  prec-cong : {X C : Obj} {zero : X ⇒ C} {zero' : X ⇒ C} {succ : C × X × N ⇒ C} {succ' : C × X × N ⇒ C}
    → (zero ≈ zero') → (succ ≈ succ') → prec zero succ ≈ prec zero' succ'

  prec-cong {_}{_} {zero}{zero'}{succ}{succ'} eq-z eq-s =
    prec-unique (prec-zero ○ eq-z) (prec-succ ○ ∘-resp-≈ˡ eq-s)

  prec-uniform : {X C D : Obj} {zero : X ⇒ C} {succ : C × X × N ⇒ C} {succ' : D × X × N ⇒ D} {h : C ⇒ D}
    → h ∘ succ ≈ succ' ∘ (h ×₁ id) → h ∘ prec zero succ ≈ prec (h ∘ zero) succ'

  prec-uniform {zero = zero} {succ = succ} {succ' = succ'} {h = h} eq = prec-unique (assoc ○ eq-z) (assoc ○ eq-s)
    where
      eq-z = begin
        h ∘ prec zero succ ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ prec-zero ⟩
        h ∘ zero                            ∎

      eq-s = begin
        h ∘ prec zero succ ∘ (id ×₁ s)              ≈⟨ refl⟩∘⟨ prec-succ  ⟩
        h ∘ succ ∘ ⟨ prec zero succ , id ⟩          ≈⟨ extendʳ eq ⟩ 
        succ' ∘ (h ×₁ id) ∘ ⟨ prec zero succ , id ⟩ ≈⟨ refl⟩∘⟨ first∘⟨⟩ ⟩
        succ' ∘ ⟨ h ∘ prec zero succ , id ⟩         ∎

  -- case distinction on zero: ifz(0, x, y) = x, ifz(n+1, x, y) = y
  ifz : ∀ {X} → N × X × X ⇒ X
  ifz = prec π₁ (π₂ ∘ π₁ ∘ π₂) ∘ swap

  -- ifz(0, x, y) = x
  ifz-z : ∀ {X} → ifz {X} ∘ ⟨ z ∘ ! , id ⟩ ≈ π₁
  ifz-z = pullʳ swap∘⟨⟩ ○ prec-zero

  -- ifz(n+1, x, y) = y
  ifz-s : ∀ {X} → ifz {X} ∘ (s ×₁ id) ≈ π₂ ∘ π₂
  ifz-s = begin
    ifz ∘ (s ×₁ id)                                           ≈⟨ pullʳ swap∘×₁ ⟩
    prec π₁ (π₂ ∘ π₁ ∘ π₂) ∘ ((id ×₁ s) ∘ swap)               ≈⟨ pullˡ prec-succ ⟩
    ((π₂ ∘ π₁ ∘ π₂) ∘ ⟨ prec π₁ (π₂ ∘ π₁ ∘ π₂) , id ⟩) ∘ swap ≈⟨ pushˡ (pullʳ (pullʳ project₂ ○ identityʳ)) ⟩
    π₂ ∘ π₁ ∘ swap                                            ≈⟨ refl⟩∘⟨ project₁ ⟩
    π₂ ∘ π₂                                                   ∎

  -- signum: sgn(0) = 0, sgn(n+1) = 1
  sgn : N ⇒ N
  sgn = ifz ∘ ⟨ id , ⟨ id , s ∘ z ∘ ! ⟩ ⟩ 

  -- sgn(0) = 0
  sgn-z : sgn ∘ z ≈ z
  sgn-z = begin
    sgn ∘ z                                   ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (⟨⟩∘ ○ ⟨⟩-congʳ identityˡ )) ⟩ 
    ifz ∘ ⟨ z , ⟨ z , (s ∘ z ∘ !) ∘ z ⟩ ⟩     ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (⟨⟩-congˡ (pullʳ (pullʳ !-unique₂))) ⟩ 
    ifz ∘ ⟨ z , ⟨ z , s ∘ z ∘ ! ⟩ ⟩           ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (introʳ !-unique₂) ⟩ 
    ifz ∘ ⟨ z ∘ ! ,  ⟨ z ,  s ∘ z ∘ ! ⟩ ⟩     ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ !-unique₂) identityˡ) ⟨ 
    ifz ∘ ⟨ z ∘ ! , id ⟩ ∘ ⟨ z ,  s ∘ z ∘ ! ⟩ ≈⟨ pullˡ ifz-z ⟩ 
    π₁ ∘ ⟨ z , s ∘ z ∘ ! ⟩                    ≈⟨ project₁ ⟩ 
    z                                         ∎

  -- sgn(n+1) = 1
  sgn-s : sgn ∘ s ≈ s ∘ z ∘ !                                                             
  sgn-s = begin
    sgn ∘ s                                      ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (⟨⟩∘ ○ ⟨⟩-congʳ identityˡ )) ⟩ 
    ifz ∘ ⟨ s , ⟨ s , (s ∘ z ∘ !) ∘ s ⟩ ⟩        ≈⟨ refl⟩∘⟨ (first∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (⟨⟩-congˡ (pushʳ (pushʳ !-unique₂)))) ⟨ 
    ifz ∘ (s ×₁ id) ∘ ⟨ id , ⟨ s , s ∘ z ∘ ! ⟩ ⟩ ≈⟨ extendʳ ifz-s ⟩   
    π₂ ∘ π₂ ∘ ⟨ id , ⟨ s , s ∘ z ∘ ! ⟩ ⟩         ≈⟨ ∘-resp-≈ʳ project₂ ○ project₂ ⟩ 
    s ∘ z ∘ !                                    ∎     

  z-or-s-≈ : ∀ {X Y} {f g : X × N ⇒ Y} → f ∘ ⟨ id , z ∘ ! ⟩ ≈ g ∘ ⟨ id , z ∘ ! ⟩ → f ∘ (id ×₁ s) ≈ g ∘ (id ×₁ s) → f ≈ g
  z-or-s-≈ {_}{_}{f}{g} eq-z eq-s = begin
    f                                             ≈⟨ prec-unique refl (pushʳ (insertʳ project₂)) ⟩
    prec (f ∘ ⟨ id , z ∘ ! ⟩) (f ∘ second s ∘ π₂) ≈⟨ prec-cong eq-z (extendʳ eq-s) ⟩
    prec (g ∘ ⟨ id , z ∘ ! ⟩) (g ∘ second s ∘ π₂) ≈⟨ prec-unique refl (pushʳ (insertʳ project₂)) ⟨
    g                                             ∎

  z-or-s-≈• : ∀ {X} {f g : N ⇒ X} → f ∘ z ∘ ! ≈ g ∘ z ∘ ! → f ∘ s ≈ g ∘ s → f ≈ g
  z-or-s-ť {X}{f}{g} eq-z eq-s = begin
    f          ≈⟨ introʳ project₂ ⟩
    f ∘ π₂ ∘ Δ ≈⟨ extendʳ (z-or-s-≈ eq-z' eq-s') ⟩
    g ∘ π₂ ∘ Δ ≈⟨ introʳ project₂ ⟨ 
    g          ∎
      where
        eq-z' : (f ∘ π₂) ∘ ⟨ id , z ∘ ! ⟩ ≈ (g ∘ π₂) ∘ ⟨ id , z ∘ ! ⟩
        eq-z' = pullʳ project₂ ○ eq-z ○ pushʳ (sym project₂)

        eq-s' : (f ∘ π₂) ∘ (id ×₁ s) ≈ (g ∘ π₂) ∘ (id ×₁ s)
        eq-s' = pullʳ π₂∘×₁ ○ extendʳ eq-s ○ pushʳ (sym π₂∘×₁)

  -- sum of two numbers
  sum : N × N ⇒ N
  sum = prec id (s ∘ π₁)

  -- n + (m+1) = (n + m) + 1
  sum-sʳ : sum ∘ (id ×₁ s) ≈ s ∘ sum
  sum-sʳ = begin
    sum ∘ (id ×₁ s)                      ≈⟨ prec-succ ⟩
    (s ∘ π₁) ∘ ⟨ prec id (s ∘ π₁) , id ⟩ ≈⟨ pullʳ project₁ ⟩
    s ∘ sum                              ∎

  -- n + 0 = n
  sum-zʳ : ∀ {X} {f : X ⇒ N} → sum ∘ ⟨ f , z ∘ !  ⟩ ≈ f
  sum-zʳ {_}{f} = begin
    sum ∘ ⟨ f , z ∘ ! ⟩      ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟨ 
    sum ∘ ⟨ id , z ∘ ! ⟩ ∘ f ≈⟨ pullˡ prec-zero ⟩
    id ∘ f                   ≈⟨ identityˡ ⟩ 
    f                        ∎

  -- 0 + n = n
  sum-zˡ : ∀ {X} {f : X ⇒ N} → sum ∘ ⟨ z ∘ ! , f ⟩ ≈ f
  sum-zˡ {_}{f} = begin
    sum ∘ ⟨ z ∘ ! , f ⟩                                             ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityʳ) ⟨ 
    sum ∘ ( z ∘ ! ×₁ f ) ∘ Δ                                        ≈⟨ refl⟩∘⟨ (×₁∘Δ ○ ⟨⟩-congʳ (sym identityʳ) ○ sym first∘⟨⟩ ) ⟩ 
    sum ∘ ( z ∘ ! ×₁ id ) ∘ ⟨ id , f ⟩                              ≈⟨ pullˡ prec-natural ⟩   
    prec (id ∘ z ∘ !) ((s ∘ π₁) ∘ (id ×₁ z ∘ ! ×₁ id)) ∘ ⟨ id , f ⟩ ≈⟨ prec-cong identityˡ (pullʳ π₁∘second) ⟩∘⟨refl ⟩
    prec (z ∘ !) (s ∘ π₁) ∘ ⟨ id , f ⟩                              ≈⟨ prec-unique project₂ (π₂∘×₁ ○ pushʳ (sym project₁)) ⟩∘⟨refl ⟨  
    π₂ ∘ ⟨ id , f ⟩                                                 ≈⟨ project₂ ⟩
    f                                                               ∎     

  -- (n+1) + m = (n + m) + 1
  sum-sˡ : sum ∘ (s ×₁ id) ≈ s ∘ sum
  sum-sˡ = begin
    sum ∘ (s ×₁ id)                            ≈⟨ prec-natural ⟩
    prec (id ∘ s) ((s ∘ π₁) ∘ (id ×₁ s ×₁ id)) ≈⟨ prec-cong id-comm-sym (pullʳ (project₁ ○ identityˡ)) ⟩
    prec (s ∘ id) (s ∘ π₁)                     ≈⟨ prec-uniform (pushʳ (sym project₁)) ⟨
    s ∘ sum                                    ∎

  -- commutativity of sum: n + m = m + n
  sum-comm : sum ∘ swap ≈ sum
  sum-comm = prec-unique h-zero h-succ
    where
      h-zero = begin
        (sum ∘ swap) ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ pullʳ swap∘⟨⟩ ⟩
        sum ∘ ⟨ z ∘ ! , id ⟩          ≈⟨ sum-zˡ ⟩
        id                            ∎
        
      h-succ = begin
        (sum ∘ swap) ∘ (id ×₁ s)       ≈⟨ pullʳ swap∘×₁ ⟩
        sum ∘ (s ×₁ id) ∘ swap         ≈⟨ pullˡ sum-sˡ ⟩
        (s ∘ sum) ∘ swap               ≈⟨ extendˡ (sym project₁) ⟩
        (s ∘ π₁) ∘ ⟨ sum ∘ swap , id ⟩ ∎

  -- commutativity of sum: pointful version
  sum-comm• : ∀{X}{f g : X ⇒ N} → sum ∘ ⟨ f , g ⟩ ≈ sum ∘ ⟨ g , f ⟩
  sum-comm• {X}{f}{g} = begin
    sum ∘ ⟨ f , g ⟩        ≈⟨ refl⟩∘⟨ swap∘⟨⟩ ⟨
    sum ∘ swap ∘ ⟨ g , f ⟩ ≈⟨ pullˡ sum-comm ⟩
    sum ∘ ⟨ g , f ⟩        ∎


  -- associativity of sum: (n + m) + k = n + (m + k)
  sum-assoc : sum ∘ (sum ×₁ id) ≈ sum ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩
  sum-assoc = prec-natural ○ sym (prec-unique (assoc ○ eq-z ○ sym identityˡ) eq-s) 
    where
      eq-z = begin
        sum ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (cancelʳ project₁) (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ identityʳ))) ⟩
        sum ∘ ⟨ π₁ , sum ∘ ⟨ π₂ , z ∘ ! ⟩ ⟩                   ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ sum-zʳ ⟩
        sum ∘ ⟨ π₁ , π₂ ⟩                                     ≈⟨ elimʳ η ⟩
        sum                                                   ∎
        
      eq-s = begin
        (sum ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩) ∘ (id ×₁ s)                              ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ π₁∘second) (pullʳ first↔second)) ⟩
        sum ∘ ⟨ π₁ ∘ π₁ , sum  ∘ (id ×₁ s) ∘ (π₂ ×₁ id) ⟩                               ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullˡ sum-sʳ) ⟩
        sum ∘ ⟨ π₁ ∘ π₁ , (s ∘ sum) ∘ (π₂ ×₁ id) ⟩                                      ≈⟨ refl⟩∘⟨ (second∘⟨⟩ ○ ⟨⟩-congˡ sym-assoc) ⟨
        sum ∘ (id ×₁ s) ∘  ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩                               ≈⟨ extendʳ sum-sʳ ⟩
        s ∘ sum ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩                                        ≈⟨ refl⟩∘⟨ project₁ ⟨
        s ∘ π₁ ∘ ⟨ sum ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ , id ⟩                          ≈⟨ pullˡ (pushʳ (sym (project₁ ○ identityˡ))) ⟩
        ((s ∘ π₁) ∘ (id ×₁ sum ×₁ id)) ∘  ⟨ sum ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ , id ⟩ ∎

  -- associativity of sum: pointful version
  sum-assoc• : ∀{X}{f g h : X ⇒ N} → sum ∘ ⟨ sum ∘ ⟨ f , g ⟩ , h ⟩ ≈ sum ∘ ⟨ f , sum ∘ ⟨ g , h ⟩ ⟩
  sum-assoc• {X}{f}{g}{h} = begin
    sum ∘ ⟨ sum ∘ ⟨ f , g ⟩ , h ⟩                                                    ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (sym identityˡ) ⟩
    sum ∘ ⟨ sum ∘ ⟨ f , g ⟩ , id ∘ h ⟩                                               ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟨
    sum ∘ (sum ×₁ id) ∘ ⟨ ⟨ f , g ⟩ , h ⟩                                            ≈⟨ pullˡ sum-assoc ○ pullʳ ⟨⟩∘ ⟩
    sum ∘ ⟨ (π₁ ∘ π₁) ∘ ⟨ ⟨ f , g ⟩ , h ⟩ , (sum ∘ (π₂ ×₁ id)) ∘ ⟨ ⟨ f , g ⟩ , h ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ project₁ ○ project₁) (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ project₂ identityˡ)) ⟩
    sum ∘ ⟨ f , sum ∘ ⟨ g , h ⟩ ⟩                                                    ∎

  -- truncated difference
  sub : N × N ⇒ N
  sub = prec id (s⁻¹ ∘ π₁)

  -- n ∸ (m+1) = (n ∸ m) ∸ 1
  sub-sʳ : sub ∘ (id ×₁ s) ≈ s⁻¹ ∘ sub
  sub-sʳ = begin
    prec id (s⁻¹ ∘ π₁) ∘ (id ×₁ s)           ≈⟨ prec-succ ⟩
    (s⁻¹ ∘ π₁) ∘ ⟨ prec id (s⁻¹ ∘ π₁) , id ⟩ ≈⟨ assoc ⟩
    s⁻¹ ∘ π₁ ∘ ⟨ prec id (s⁻¹ ∘ π₁) , id ⟩   ≈⟨ refl⟩∘⟨ project₁ ⟩
    s⁻¹ ∘ prec id (s⁻¹ ∘ π₁)                 ∎

  -- (n+1) ∸ (m+1) = n ∸ m
  sub-ss : sub ∘ (s ×₁ s) ≈ sub
  sub-ss = prec-unique
    (begin
       (sub ∘ (s ×₁ s)) ∘ ⟨ id , z ∘ ! ⟩               ≈⟨ (pushʳ (×₁-cong₂ (sym identityˡ) (sym identityʳ) ○ sym ×₁∘×₁) ○ pushˡ sub-sʳ) ⟩∘⟨refl ⟩
       (s⁻¹ ∘ sub ∘ (s ×₁ id)) ∘ ⟨ id , z ∘ ! ⟩        ≈⟨ pullʳ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ id-comm (identityˡ ○ pushʳ !-unique₂) ○ sym ⟨⟩∘)) ⟩
       s⁻¹ ∘ sub ∘ ⟨ id , z ∘ ! ⟩ ∘ s                  ≈⟨ refl⟩∘⟨ pullˡ prec-zero ⟩
       s⁻¹ ∘ id ∘ s                                    ≈⟨ ∘-resp-≈ʳ identityˡ ○ s⁻¹-succ ⟩
       id                                              ∎)
    (begin
       (sub ∘ (s ×₁ s)) ∘ (id ×₁ s)                     ≈⟨ extendˡ (×₁∘×₁ ○ ×₁-cong₂ id-comm refl ○ sym ×₁∘×₁) ⟩
       (sub ∘ (id ×₁ s)) ∘ (s ×₁ s)                     ≈⟨ pushˡ sub-sʳ ⟩
       s⁻¹ ∘ sub ∘ (s ×₁ s)                             ≈⟨ pullʳ project₁ ⟨
       (s⁻¹ ∘ π₁) ∘ ⟨ sub ∘ (s ×₁ s) , id ⟩             ∎)

  -- (n ∸ 1) ∸ m = (n ∸ m) ∸ 1
  sub-s⁻¹ʳ : sub ∘ (s⁻¹ ×₁ id) ≈ s⁻¹ ∘ sub
  sub-s⁻¹ʳ = prec-unique eq-z eq-s ○ sym (prec-unique (cancelʳ prec-zero) (extendˡ (sub-sʳ ○ sym project₁)))
    where
      eq-z : (sub ∘ (s⁻¹ ×₁ id)) ∘ ⟨ id , z ∘ ! ⟩ ≈ s⁻¹
      eq-z = begin
        (sub ∘ (s⁻¹ ×₁ id)) ∘ ⟨ id , z ∘ ! ⟩           ≈⟨ pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
        sub ∘ ⟨ s⁻¹ , z ∘ ! ⟩                          ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ (sym !-unique₂)) ) ⟨
        (sub ∘ ⟨ id , z ∘ ! ⟩) ∘ s⁻¹                   ≈⟨ elimˡ prec-zero ⟩
        s⁻¹                                            ∎

      eq-s : (sub ∘ (s⁻¹ ×₁ id)) ∘ (id ×₁ s) ≈ (s⁻¹ ∘ π₁) ∘ ⟨ sub ∘ (s⁻¹ ×₁ id) , id ⟩
      eq-s = begin
        (sub ∘ (s⁻¹ ×₁ id)) ∘ (id ×₁ s)                 ≈⟨ extendˡ first↔second ⟩
        (sub ∘ (id ×₁ s)) ∘ (s⁻¹ ×₁ id)                 ≈⟨ pushˡ sub-sʳ ⟩
        s⁻¹ ∘ sub ∘ (s⁻¹ ×₁ id)                         ≈⟨ pullʳ project₁ ⟨
        (s⁻¹ ∘ π₁) ∘ ⟨ sub ∘ (s⁻¹ ×₁ id) , id ⟩         ∎

  -- n ∸ n = 0
  sub-Δ : sub ∘ Δ ≈ z ∘ !
  sub-Δ = begin
    sub ∘ Δ                                            ≈⟨ nno-unique (sym sub-Δz) (identityˡ ○ sym sub-Δs) ⟩
    nno-universal (z ∘ !) id                           ≈⟨ nno-unique (pushʳ !-unique₂) (identityˡ ○ pushʳ !-unique₂) ⟨
    z ∘ !                                              ∎

    where
      sub-Δz : (sub ∘ ⟨ id , id ⟩) ∘ z ≈ z ∘ !
      sub-Δz = begin
        (sub ∘ ⟨ id , id ⟩) ∘ z                                 ≈⟨ refl⟩∘⟨ introʳ !-unique₂ ⟩
        (sub ∘ ⟨ id , id ⟩) ∘ z ∘ !                             ≈⟨ pullʳ ( ⟨⟩∘ ○ ⟨⟩-congˡ (identityˡ ○ pushʳ !-unique₂) ○ sym ⟨⟩∘) ⟩
        sub ∘ ⟨ id , z ∘ ! ⟩ ∘ z ∘ !                            ≈⟨ pullˡ prec-zero ⟩
        id ∘ z ∘ !                                              ≈⟨ identityˡ ⟩
        z ∘ !                                                   ∎

      sub-Δs : (sub ∘ ⟨ id , id ⟩) ∘ s ≈ sub ∘ ⟨ id , id ⟩
      sub-Δs = begin
        (sub ∘ ⟨ id , id ⟩) ∘ s                                 ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ id-comm-sym id-comm-sym ○ sym ×₁∘⟨⟩) ⟩
        sub ∘ (s ×₁ s) ∘ ⟨ id , id ⟩                            ≈⟨ pullˡ sub-ss ⟩
        sub ∘ ⟨ id , id ⟩                                       ∎


  -- n ∸ n = 0 (pointful)
  sub-Δ• : ∀ {X} {n : X ⇒ N} → sub ∘ ⟨ n , n ⟩ ≈ z ∘ !
  sub-Δ• {X}{n} = pushʳ (sym Δ∘) ○ ∘-resp-≈ˡ sub-Δ ○ pullʳ !-unique₂

  -- n ∸ 0 = n
  sub-zʳ : ∀ {X}{f : X ⇒ N} → sub ∘ ⟨ f , z ∘ ! ⟩ ≈ f
  sub-zʳ = pushʳ (unique (cancelˡ project₁) (pullˡ project₂ ○ pullʳ !-unique₂)) ○ ∘-resp-≈ˡ prec-zero ○ identityˡ

  -- 0 ∸ n = 0
  sub-zˡ : sub ∘ ⟨ z ∘ ! , id ⟩ ≈ z ∘ !
  sub-zˡ = begin
    sub ∘ ⟨ z ∘ ! , id ⟩                                         ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟨
    sub ∘ (z ∘ ! ×₁ id) ∘ Δ                                      ≈⟨ pullˡ prec-natural ⟩
    prec (id ∘ z ∘ !) ((s⁻¹ ∘ π₁) ∘ (id ×₁ z ∘ ! ×₁ id)) ∘ Δ     ≈⟨ prec-cong identityˡ (pullʳ π₁∘second) ⟩∘⟨refl ⟩
    prec (z ∘ !) (s⁻¹ ∘ π₁) ∘ Δ                                  ≈⟨ prec-unique (pullʳ (sym !-unique₂)) (pullʳ (sym !-unique₂) ○ pushˡ (sym s⁻¹-zero) ○ pushʳ (sym project₁)) ⟩∘⟨refl ⟨
    (z ∘ !) ∘ Δ                                                  ≈⟨ pushʳ !-unique₂ ⟨
    z ∘ !                                                        ∎    

  -- (n + m) ∸ m = n
  sub-sum : sub ∘ ⟨ sum , π₂ ⟩ ≈ π₁
  sub-sum = prec-unique (assoc ○ eq-z) (assoc ○ eq-s) ○ sym (prec-unique project₁ (π₁∘second ○ sym project₁))
    where
      eq-z = begin
        sub ∘ ⟨ sum , π₂ ⟩ ∘ ⟨ id , z ∘ ! ⟩                      ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟩
        sub ∘ ⟨ sum ∘ ⟨ id , z ∘ ! ⟩ , z ∘ ! ⟩                   ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ prec-zero ⟩
        sub ∘ ⟨ id , z ∘ ! ⟩                                     ≈⟨ prec-zero ⟩
        id                                                       ∎

      eq-s = begin
        sub ∘ ⟨ sum , π₂ ⟩ ∘ (id ×₁ s)                           ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟩
        sub ∘ ⟨ sum ∘ (id ×₁ s) , s ∘ π₂ ⟩                       ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ prec-succ ⟩
        sub ∘ ⟨ (s ∘ π₁) ∘ ⟨ sum , id ⟩ , s ∘ π₂ ⟩               ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (pullʳ project₁) ⟩
        sub ∘ ⟨ s ∘ sum , s ∘ π₂ ⟩                               ≈⟨ pushʳ (sym ×₁∘⟨⟩) ○ ∘-resp-≈ˡ sub-ss ⟩
        sub ∘ ⟨ sum , π₂ ⟩                                       ≈⟨ project₁ ⟨
        π₁ ∘ ⟨ sub ∘ ⟨ sum , π₂ ⟩ , id ⟩                         ∎

  -- (n+1) ∸ n = 1
  sn-n : ∀ {X} {n : X ⇒ N} → sub ∘ ⟨ s ∘ n , n ⟩ ≈ s ∘ z ∘ !
  sn-n {X}{n} = begin                                                                                                                                                                                        
    sub ∘ ⟨ s ∘ n , n ⟩                     ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (sym (∘-resp-≈ʳ (sym (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ)) ○ sym assoc ○ ∘-resp-≈ˡ sum-sˡ ○ assoc ○ ∘-resp-≈ʳ sum-zˡ)) ⟩                                  
    sub ∘ ⟨ sum ∘ ⟨ s ∘ z ∘ ! , n ⟩ , n ⟩   ≈⟨ ∘-resp-≈ʳ (sym (⟨⟩∘ ○ ⟨⟩-congˡ project₂)) ○ sym assoc ○ ∘-resp-≈ˡ sub-sum ○ project₁ ⟩                                                                            
    s ∘ z ∘ !                               ∎ 

  -- maximum: max(n,m) = (n ∸ m) + m
  max : N × N ⇒ N
  max = sum ∘ ⟨ sub , π₂ ⟩ 

  -- minimum: min(n,m) = n ∸ (n ∸ m)
  min : N × N ⇒ N
  min = sub ∘ ⟨ π₁ , sub ⟩

  -- min(n + m, m) = m
  min-sum : min ∘ ⟨ sum , π₂ ⟩ ≈ π₂
  min-sum = begin
    min ∘ ⟨ sum , π₂ ⟩                 ≈⟨ assoc ⟩
    sub ∘ ⟨ π₁ , sub ⟩ ∘ ⟨ sum , π₂ ⟩  ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ project₁ sub-sum) ⟩
    sub ∘ ⟨ sum , π₁ ⟩                 ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (⟺ sum-comm) (⟺ project₂) ⟩
    sub ∘ ⟨ sum ∘ swap , π₂ ∘ swap ⟩   ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨
    sub ∘ ⟨ sum , π₂ ⟩ ∘ swap          ≈⟨ pullˡ sub-sum ⟩
    π₁ ∘ swap                          ≈⟨ project₁ ⟩
    π₂                                 ∎

  -- max(n, 0) = n
  max-zʳ : ∀ {X}{f : X ⇒ N} → max ∘ ⟨ f , z ∘ ! ⟩ ≈ f
  max-zʳ {_}{f} = begin
    max ∘ ⟨ f , z ∘ ! ⟩                                    ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)) ⟨ 
    max ∘ ⟨ id , z ∘ ! ⟩ ∘ f                               ≈⟨ pullˡ (pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ project₂)) ○ assoc ⟩ 
    sum ∘ ⟨ sub ∘ ⟨ id , z ∘ ! ⟩ , z ∘ ! ⟩ ∘ f             ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ prec-zero ⟩∘⟨refl ⟩
    sum ∘ ⟨ id , z ∘ ! ⟩ ∘ f                               ≈⟨ pullˡ prec-zero ○ identityˡ ⟩
    f                                                      ∎

  -- max(0, n) = n
  max-zˡ : ∀ {X}{f : X ⇒ N} → max ∘ ⟨ z ∘ ! , f ⟩ ≈ f
  max-zˡ {_}{f} = begin
    max ∘ ⟨ z ∘ ! , f ⟩                                    ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ !-unique₂) identityˡ) ⟨ 
    max ∘ ⟨ z ∘ ! , id ⟩ ∘ f                               ≈⟨ extendʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ project₂)) ⟩
    sum ∘ ⟨ sub ∘ ⟨ z ∘ ! , id ⟩ , id ⟩ ∘ f                ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ sub-zˡ ⟩∘⟨refl ⟩
    sum ∘ ⟨ z ∘ ! , id ⟩ ∘ f                               ≈⟨ cancelˡ sum-zˡ ⟩ 
    f                                                      ∎

  -- subs((n,m), k) = (n ∸ k, m ∸ k)
  subs : (N × N) × N ⇒ N × N
  subs = ⟨ sub ∘ first π₁ , sub ∘ first π₂ ⟩

  subs-swap : subs ∘ first swap ≈ swap ∘ subs
  subs-swap = begin
    subs ∘ first swap                                       ≈⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ first∘first) (pullʳ first∘first) ⟩
    ⟨ sub ∘ first (π₁ ∘ swap) , sub ∘ first (π₂ ∘ swap) ⟩   ≈⟨ ⟨⟩-cong₂ (∘-resp-≈ʳ (⟨⟩-congʳ (∘-resp-≈ˡ project₁))) (∘-resp-≈ʳ (⟨⟩-congʳ (∘-resp-≈ˡ project₂))) ⟩
    ⟨ sub ∘ (π₂ ×₁ id) , sub ∘ (π₁ ×₁ id) ⟩                 ≈⟨ swap∘⟨⟩ ⟨
    swap ∘ subs                                             ∎    

  -- subs((n,m), 0) = (n, m)
  subs-z : subs ∘ ⟨ id , z ∘ ! ⟩ ≈ id
  subs-z = ⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ first∘⟨⟩ ○ sub-zʳ) (pullʳ first∘⟨⟩ ○ sub-zʳ) ○ unique refl refl

  -- subs((n,m), k+1) = ((n ∸ k) ∸ 1, (m ∸ k) ∸ 1)
  subs-s : subs ∘ second s ≈ (s⁻¹ ×₁ s⁻¹) ∘ subs
  subs-s = begin
    subs ∘ second s                                                 ≈⟨ ⟨⟩∘ ⟩ 
    ⟨ (sub ∘ first π₁) ∘ second s , (sub ∘ first π₂) ∘ second s ⟩   ≈⟨ ⟨⟩-cong₂ (pullʳ first↔second ○ extendʳ sub-sʳ) (pullʳ first↔second ○ extendʳ sub-sʳ) ⟩ 
    ⟨ s⁻¹ ∘ sub ∘ first π₁ , s⁻¹ ∘ sub ∘ first π₂ ⟩                 ≈⟨ ×₁∘⟨⟩ ⟨ 
    (s⁻¹ ×₁ s⁻¹) ∘ subs                                             ∎

  -- max(x ∸ y, y ∸ y) = x ∸ y
  max-subs-xyy : (max ∘ subs) ∘ ⟨ id , π₂ ⟩ ≈ sub
  max-subs-xyy = begin
    (max ∘ subs) ∘ ⟨ id , π₂ ⟩                              ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ identityʳ)) (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ identityʳ)))⟩ 
    max ∘ ⟨ sub ∘ ⟨ π₁ , π₂ ⟩ , sub ∘ ⟨ π₂ , π₂ ⟩ ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (elimʳ η) (pushʳ (sym Δ∘) ○ ∘-resp-≈ˡ sub-Δ ○ pullʳ !-unique₂) ⟩
    max ∘ ⟨ sub  , z ∘ ! ⟩                                  ≈⟨ max-zʳ ⟩
    sub                                                     ∎
    
  -- max(y ∸ y, x ∸ y) = x ∸ y
  max-subs-yxy : (max ∘ subs) ∘ ⟨ swap , π₂ ⟩ ≈ sub
  max-subs-yxy = begin
    (max ∘ subs) ∘ ⟨ swap , π₂ ⟩                            ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ project₁)) (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ project₂)))⟩ 
    max ∘ ⟨ sub ∘ ⟨ π₂ , π₂ ⟩ , sub ∘ ⟨ π₁ , π₂ ⟩ ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pushʳ (sym Δ∘) ○ ∘-resp-≈ˡ sub-Δ ○ pullʳ !-unique₂) (elimʳ η) ⟩ 
    max ∘ ⟨ z ∘ ! , sub ⟩                                   ≈⟨ max-zˡ ⟩
    sub                                                     ∎

  -- auxiliary accumulator for the max-commutativity (Goodstein) argument:
  goodstein : (N × N) × N ⇒ N
  goodstein = prec (z ∘ !) (sum ∘ (id ×₁ sgn ∘ sum ∘ subs))

  -- goodstein is invariant under swapping its pair argument
  goodstein-swap : goodstein ∘ first swap ≈ goodstein
  goodstein-swap = prec-unique (assoc ○ goodstein-swap-z) (assoc ○ goodstein-swap-s ○ sym-assoc)
    where
      goodstein-swap-z = begin
        goodstein ∘ first swap ∘ ⟨ id , z ∘ ! ⟩         ≈⟨ refl⟩∘⟨ first∘⟨⟩ ⟩
        goodstein ∘ ⟨ swap ∘ id , z ∘ ! ⟩               ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ id-comm-sym (pullʳ !-unique₂)) ⟨
        goodstein ∘ ⟨ id , z ∘ ! ⟩ ∘ swap               ≈⟨ pullˡ prec-zero ⟩
        (z ∘ !) ∘ swap                                  ≈⟨ pullʳ !-unique₂ ⟩
        z ∘ !                                           ∎
       
      goodstein-swap-s = begin
        goodstein ∘ first swap ∘ (id ×₁ s)                                            ≈⟨ refl⟩∘⟨ first↔second ⟩
        goodstein ∘ second s ∘ first swap                                             ≈⟨ pullˡ prec-succ ○ assoc ○ assoc ⟩
        sum ∘ (id ×₁ sgn ∘ sum ∘ subs) ∘ ⟨ goodstein , id ⟩ ∘ first swap              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ  identityˡ) ⟩ 
        sum ∘ (id ×₁ sgn ∘ sum ∘ subs) ∘ ⟨ goodstein ∘ first swap , first swap ⟩      ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ (pullʳ assoc)) ⟩
        sum ∘ ⟨ goodstein ∘ first swap , sgn ∘ sum ∘ subs ∘ first swap ⟩              ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (∘-resp-≈ʳ (pushʳ subs-swap ○ ∘-resp-≈ˡ sum-comm)) ⟩        
        sum ∘ ⟨ goodstein ∘ first swap , sgn ∘ sum ∘ subs ⟩                           ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟨        
        sum ∘ second (sgn ∘ sum ∘ subs) ∘ ⟨ goodstein ∘ first swap , id ⟩             ∎
  
  -- max(n ∸ 1, m ∸ 1) + sgn(n + m) = max(n, m)
  max-succ : sum ∘ ⟨ max ∘ (s⁻¹ ×₁ s⁻¹) , sgn ∘ sum ⟩ ≈ max
  max-succ = z-or-s-≈ (assoc ○ max-succ-z) (assoc ○ max-succ-s)
    where
      max-succ-z = begin
        sum ∘ ⟨ max ∘ (s⁻¹ ×₁ s⁻¹) , sgn ∘ sum ⟩ ∘ ⟨ id , z ∘ ! ⟩      ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityʳ)) (cancelʳ sum-zʳ)) ⟩ 
        sum ∘ ⟨ max ∘ ⟨ s⁻¹ , s⁻¹ ∘ z ∘ ! ⟩ , sgn ⟩                    ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (⟨⟩-congˡ (pullˡ s⁻¹-zero)) ○ max-zʳ) ⟩ 
        sum ∘ ⟨ s⁻¹ , sgn ⟩                                            ≈⟨ z-or-s-≈• (assoc ○ eq-z ○ sym identityˡ) (assoc ○ eq-s ○ sym identityˡ) ⟩ 
        id                                                             ≈⟨ max-zʳ ⟨
        max ∘ ⟨ id , z ∘ ! ⟩                                           ∎

        where
          eq-z : sum ∘ ⟨ s⁻¹ , sgn ⟩ ∘ z ∘ ! ≈ z ∘ !
          eq-z = begin
            sum ∘ ⟨ s⁻¹ , sgn ⟩ ∘ z ∘ !                 ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullˡ s⁻¹-zero) (pullˡ sgn-z)) ⟩ 
            sum ∘ ⟨ z ∘ ! , z ∘ ! ⟩                     ≈⟨ sum-zʳ ⟩ 
            z ∘ !                                       ∎

          eq-s : sum ∘ ⟨ s⁻¹ , sgn ⟩ ∘ s ≈ s
          eq-s = begin
            sum ∘ ⟨ s⁻¹ , sgn ⟩ ∘ s                     ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ s⁻¹-succ sgn-s) ⟩ 
            sum ∘ ⟨ id , s ∘ z ∘ ! ⟩                    ≈⟨ pushʳ (⟨⟩-congʳ (sym identityˡ) ○ sym ×₁∘⟨⟩) ○ pushˡ sum-sʳ ⟩ 
            s ∘ sum ∘ ⟨ id , z ∘ ! ⟩                    ≈⟨ elimʳ sum-zʳ ⟩ 
            s ∎
            
      max-succ-s = begin
        sum ∘ ⟨ max ∘ (s⁻¹ ×₁ s⁻¹) , sgn ∘ sum ⟩ ∘ (id ×₁ s)           ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityʳ s⁻¹-succ)) (pullʳ sum-sʳ)) ⟩ 
        sum ∘ ⟨ max ∘ (s⁻¹ ×₁ id) , sgn ∘ s ∘ sum ⟩                    ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullˡ sgn-s ○ pullʳ (pullʳ !-unique₂)) ⟩ 
        sum ∘ ⟨ max ∘ (s⁻¹ ×₁ id) , s ∘ z ∘ ! ⟩                        ≈⟨ pushʳ (sym (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ)) ○ pushˡ sum-sʳ ○ ∘-resp-≈ʳ sum-zʳ ⟩ 
        s ∘ max ∘ (s⁻¹ ×₁ id)                                          ≈⟨ refl⟩∘⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ π₂∘first) ⟩ 
        s ∘ sum ∘ ⟨ sub ∘ (s⁻¹ ×₁ id) , π₂ ⟩                           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ sub-s⁻¹ʳ ⟩   
        s ∘ sum ∘ ⟨ s⁻¹ ∘ sub , π₂ ⟩                                   ≈⟨ pushʳ (⟨⟩-congʳ (sym identityˡ) ○ sym ×₁∘⟨⟩ ) ○ pushˡ sum-sʳ  ⟨
        sum ∘ ⟨ s⁻¹ ∘ sub , s ∘ π₂ ⟩                                   ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ sub-sʳ π₂∘×₁) ⟨ 
        max ∘ (id ×₁ s)                                                ∎

  -- max is commutative
  -- This implements Goodstein's argument from "Logic-free formalisations of recursive arithmetic", 1954
  max-comm : max ≈ max ∘ swap
  max-comm = begin
    max                                                                  ≈⟨ introʳ project₁ ⟩
    max ∘ π₁ ∘ ⟨ id , π₂ ⟩                                               ≈⟨ extendʳ (sym eq₁) ⟩ 
    sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ ⟨ id , π₂ ⟩                       ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congʳ max-subs-xyy) ⟩ 
    sum ∘ ⟨ sub , goodstein ∘ ⟨ id , π₂ ⟩ ⟩                              ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ max-subs-yxy ⟨ 
    sum ∘ ⟨ (max ∘ subs) ∘ ⟨ swap , π₂ ⟩ , goodstein ∘ ⟨ id , π₂ ⟩ ⟩     ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congʳ (extendˡ (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ identityʳ))) ) ⟨
    sum ∘ ⟨ max ∘ subs ∘ first swap , goodstein ⟩ ∘ ⟨ id , π₂ ⟩          ≈⟨ refl⟩∘⟨  ⟨⟩-congʳ (∘-resp-≈ʳ subs-swap) ⟩∘⟨refl ⟩
    sum ∘ ⟨ max ∘ swap ∘ subs , goodstein ⟩ ∘ ⟨ id , π₂ ⟩                ≈⟨ extendʳ ( eq₂ ○ sym-assoc) ○ assoc ⟩
    max ∘ swap ∘ π₁ ∘ ⟨ id , π₂ ⟩                                        ≈⟨ refl⟩∘⟨ introʳ project₁ ⟨ 
    max ∘ swap                                                           ∎

    where
      eq₁-z : sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ ⟨ id , z ∘ ! ⟩ ≈ max
      eq₁-z = begin
        sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ ⟨ id , z ∘ ! ⟩                ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ subs-z ○ identityʳ) prec-zero) ⟩
        sum ∘ ⟨ max , z ∘ ! ⟩                                            ≈⟨ sum-zʳ ⟩
        max                                                              ∎

      eq₂-z : sum ∘ ⟨ max ∘ swap ∘ subs , goodstein ⟩ ∘ ⟨ id , z ∘ ! ⟩ ≈ max ∘ swap
      eq₂-z = begin
        sum ∘ ⟨ max ∘ swap ∘ subs , goodstein ⟩ ∘ ⟨ id , z ∘ ! ⟩         ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ assoc²βε prec-zero) ⟩
        sum ∘ ⟨ max ∘ swap ∘ subs ∘ ⟨ id , z ∘ ! ⟩ , z ∘ ! ⟩             ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (pullˡ (sym subs-swap) ○ pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ identityʳ))) ⟩
        sum ∘ ⟨ max ∘ subs ∘ ⟨ swap , z ∘ ! ⟩ , z ∘ ! ⟩                  ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ (pullʳ !-unique₂)))) (pullʳ !-unique₂)) ⟨
        sum ∘ ⟨ max ∘ subs ∘ ⟨ id , z ∘ ! ⟩ , z ∘ ! ⟩  ∘ swap            ≈⟨ refl⟩∘⟨ pullˡ (⟨⟩∘ ○ ⟨⟩-cong₂ assoc prec-zero) ⟨
        sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ ⟨ id , z ∘ ! ⟩ ∘ swap         ≈⟨ ∘-resp-≈ʳ sym-assoc ○ pullˡ eq₁-z  ⟩
        max ∘ swap                                                       ∎
                  
      eq₁-s : sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ second s ≈ sum ∘ ⟨ max ∘ subs , goodstein ⟩ 
      eq₁-s = begin
        sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ second s                                                          ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congʳ assoc) ⟩
        sum ∘ ⟨ max ∘ subs ∘ second s , goodstein ∘ second s ⟩                                               ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (prec-succ ○ pullʳ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ)) ⟩
        sum ∘ ⟨ max ∘ subs ∘ second s , sum ∘ ⟨ goodstein , sgn ∘ sum ∘ subs ⟩ ⟩                             ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ sum-comm• ⟩
        sum ∘ ⟨ max ∘ subs ∘ second s , sum ∘ ⟨ sgn ∘ sum ∘ subs , goodstein ⟩ ⟩                             ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁ ○ project₁) (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ project₂)))
        ⟨ sum ∘ ⟨ π₁ ∘ π₁ , sum ∘ first π₂ ⟩ ∘ ⟨ ⟨ max ∘ subs ∘ second s , sgn ∘ sum ∘ subs ⟩ , goodstein ⟩  ≈⟨ pullˡ sum-assoc ○ assoc ⟨  
        sum ∘ first sum ∘ ⟨ ⟨ max ∘ subs ∘ second s , sgn ∘ sum ∘ subs ⟩ , goodstein ⟩                       ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ) ⟩
        sum ∘ ⟨ sum ∘ ⟨ max ∘ subs ∘ second s , sgn ∘ sum ∘ subs ⟩ , goodstein ⟩                             ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (⟨⟩-congʳ (∘-resp-≈ʳ subs-s))) ⟩
        sum ∘ ⟨ sum ∘ ⟨ max ∘ (s⁻¹ ×₁ s⁻¹) ∘ subs , sgn ∘ sum ∘ subs ⟩ , goodstein ⟩                         ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (  ⟨⟩-cong₂ sym-assoc sym-assoc ○ sym ⟨⟩∘) ○ pullˡ max-succ ) ⟩
        sum ∘ ⟨ max ∘ subs , goodstein ⟩                                                                     ∎

      eq₂-s : sum ∘ ⟨ max ∘ swap ∘ subs , goodstein ⟩ ∘ (id ×₁ s) ≈ sum ∘ ⟨ max ∘ swap ∘ subs , goodstein ⟩
      eq₂-s = begin
        sum ∘ ⟨ max ∘ swap ∘ subs , goodstein ⟩ ∘ second s            ≈⟨ refl⟩∘⟨ pullˡ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ subs-swap) goodstein-swap) ⟨
        sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ first swap ∘ second s      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ first↔second ⟩
        sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ second s ∘ first swap      ≈⟨ assoc²εβ ○ pushˡ eq₁-s ⟩
        sum ∘ ⟨ max ∘ subs , goodstein ⟩ ∘ first swap                 ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congʳ assoc) ⟩
        sum ∘ ⟨ max ∘ subs ∘ first swap , goodstein ∘ first swap ⟩    ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (∘-resp-≈ʳ subs-swap) goodstein-swap ⟩
        sum ∘ ⟨ max ∘ swap ∘ subs , goodstein ⟩                       ∎

      eq₁ : sum ∘ ⟨ max ∘ subs , goodstein ⟩ ≈ max ∘ π₁
      eq₁ = prec-unique (assoc ○ eq₁-z) (assoc ○ eq₁-s ○ sym project₁) ○ prec-η max

      eq₂ : sum ∘ ⟨ max ∘ swap ∘ subs , goodstein ⟩ ≈ max ∘ swap ∘ π₁
      eq₂ = prec-unique (assoc ○ eq₂-z) (assoc ○ eq₂-s ○ sym project₁) ○ prec-η (max ∘ swap) ○ assoc

  -- commutativity of max (pointful): max(n, m) = max(m, n)
  max-comm• : ∀ {X} {n m : X ⇒ N} → max ∘ ⟨ n , m ⟩ ≈ max ∘ ⟨ m , n ⟩
  max-comm• {X}{n}{m} = pushˡ max-comm ○ ∘-resp-≈ʳ swap∘⟨⟩

  -- cancellation: n + k = m + k ⟹ n = m
  cancel : ∀{X} {n m k : X ⇒ N} → sum ∘ ⟨ n , k ⟩ ≈ sum ∘ ⟨ m , k ⟩ → n ≈ m
  cancel {X}{n}{m}{k} eq = begin
    n                                     ≈⟨ pullˡ sub-sum ○ project₁ ⟨
    sub ∘ ⟨ sum , π₂  ⟩ ∘ ⟨ n , k ⟩       ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟩
    sub ∘ ⟨ sum ∘ ⟨ n , k ⟩ , k ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ eq ⟩
    sub ∘ ⟨ sum ∘ ⟨ m , k ⟩ , k ⟩         ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟨
    sub ∘ ⟨ sum , π₂  ⟩ ∘ ⟨ m , k ⟩       ≈⟨ pullˡ sub-sum ○ project₁ ⟩
    m                                     ∎

  -- iterated subtraction: (a ∸ b) ∸ c ≈ a ∸ (b + c)
  sub-sub : sub ∘ (sub ×₁ id) ≈ sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩
  sub-sub = prec-natural ○ sym (prec-unique (assoc ○ sub-sub-z ○ sym identityˡ) (assoc ○ sub-sub-s ○ sym-assoc))
    where
      sub-sub-z = begin
        sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ ∘ ⟨ id , z ∘ ! ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (cancelʳ project₁) (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ identityʳ))) ⟩
        sub ∘ ⟨ π₁ , sum ∘ ⟨ π₂ , z ∘ ! ⟩ ⟩                   ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ sum-zʳ ⟩
        sub ∘ ⟨ π₁ , π₂ ⟩                                     ≈⟨ elimʳ η ⟩
        sub ∎

      sub-sub-s = begin
        sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ ∘ (id ×₁ s)                                ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ π₁∘second) (pullʳ first↔second)) ⟩
        sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ (id ×₁ s) ∘ (π₂ ×₁ id) ⟩                                ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullˡ sum-sʳ) ⟩
        sub ∘ ⟨ π₁ ∘ π₁ , (s ∘ sum) ∘ (π₂ ×₁ id) ⟩                                      ≈⟨ refl⟩∘⟨ (second∘⟨⟩ ○ ⟨⟩-congˡ sym-assoc) ⟨
        sub ∘ (id ×₁ s) ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩                                ≈⟨ extendʳ sub-sʳ ⟩
        s⁻¹ ∘ sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩                                      ≈⟨ pullʳ (pullˡ π₁∘second ○ project₁) ⟨
        (s⁻¹ ∘ π₁) ∘ (id ×₁ sub ×₁ id) ∘ ⟨ sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ , id ⟩  ∎

  sub-sub• : ∀ {X} {n m k : X ⇒ N} → sub ∘ ⟨ sub ∘ ⟨ n , m ⟩ , k ⟩ ≈ sub ∘ ⟨ n , sum ∘ ⟨ m , k ⟩ ⟩
  sub-sub• {X}{n}{m}{k} = begin
    sub ∘ ⟨ sub ∘ ⟨ n , m ⟩ , k ⟩                                 ≈⟨ refl⟩∘⟨ sym (×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ) ⟩
    sub ∘ (sub ×₁ id) ∘ ⟨ ⟨ n , m ⟩ , k ⟩                         ≈⟨ sym assoc ○ ∘-resp-≈ˡ sub-sub ○ assoc ⟩
    sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ ∘ ⟨ ⟨ n , m ⟩ , k ⟩      ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁) (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ project₂))) ⟩ 
    sub ∘ ⟨ π₁ ∘ ⟨ n , m ⟩ , sum ∘ ⟨ m  , k ⟩ ⟩                   ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ project₁ ⟩
    sub ∘ ⟨ n , sum ∘ ⟨ m , k ⟩ ⟩                                 ∎

  -- (n ∸ m) ∸ n ≈ 0
  -- needs: sub-sub  (collapse to n ∸ (m+n)), sum-comm, sub-Δ, sub-zˡ
  sub-sub-self : sub ∘ ⟨ sub , π₁ ⟩ ≈ z ∘ !
  sub-sub-self = begin
    sub ∘ ⟨ sub , π₁ ⟩                                            ≈⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟨
    sub ∘ (sub ×₁ id) ∘ ⟨ id , π₁ ⟩                               ≈⟨ extendʳ sub-sub ⟩   
    sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ (π₂ ×₁ id) ⟩ ∘ ⟨ id , π₁ ⟩            ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (sum-comm• ○ ∘-resp-≈ʳ (⟨⟩-congʳ identityˡ)) ⟩∘⟨refl ⟩ 
    sub ∘ ⟨ π₁ ∘ π₁ , sum ∘ ⟨ π₂ , π₂ ∘ π₁ ⟩ ⟩ ∘ ⟨ id , π₁ ⟩      ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ (cancelʳ project₁) (cancelʳ (⟨⟩∘ ○ ⟨⟩-cong₂ project₂ (cancelʳ project₁) ○ η))) ⟩
    sub ∘ ⟨ π₁ , sum ⟩                                            ≈⟨ pullˡ sub-sub ○ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁ ○ project₁) (cancelʳ (first∘⟨⟩ ○ ⟨⟩-congʳ project₂ ○ η)))  ⟨
    sub ∘ (sub ×₁ id) ∘ ⟨ ⟨ π₁ , π₁ ⟩ , π₂ ⟩                      ≈⟨ refl⟩∘⟨ first∘⟨⟩ ⟩ 
    sub ∘ ⟨ sub ∘ ⟨ π₁ , π₁ ⟩ , π₂ ⟩                              ≈⟨ refl⟩∘⟨ (⟨⟩-congʳ (∘-resp-≈ʳ (sym (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ identityˡ)) ○ pullˡ sub-Δ ○ pullʳ !-unique₂)) ⟩ 
    sub ∘ ⟨ z ∘ ! , π₂ ⟩                                          ≈⟨ refl⟩∘⟨ sym (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ !-unique₂) identityˡ) ○ pullˡ sub-zˡ  ⟩  
    (z ∘ !) ∘ π₂                                                  ≈⟨ assoc ○ ∘-resp-≈ʳ !-unique₂ ⟩
    z ∘ !                                                         ∎

  -- max(n, n ∸ m) ≈ n 
  -- needs: max-comm, max = sum∘⟨sub,π₂⟩, sub-sub-self, sum-zˡ
  max-sub-self : max ∘ ⟨ π₁ , sub ⟩ ≈ π₁
  max-sub-self = begin
    max ∘ ⟨ π₁ , sub ⟩                         ≈⟨ pushˡ max-comm ○ pullʳ (∘-resp-≈ʳ swap∘⟨⟩ ○ ⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟩  
    sum ∘ ⟨ sub ∘ ⟨ sub , π₁ ⟩ , π₁ ⟩          ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ sub-sub-self ⟩
    sum ∘ ⟨ z ∘ ! , π₁ ⟩                       ≈⟨ sum-zˡ ⟩
    π₁                                         ∎

  -- n ≈ min(n,m) + (n ∸ m)
  -- needs: max-sub-self 
  sum-min-sub : sum ∘ ⟨ min , sub ⟩ ≈ π₁
  sum-min-sub = begin
    sum ∘ ⟨ min , sub ⟩                              ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟨
    max ∘ ⟨ π₁ , sub ⟩                               ≈⟨ max-sub-self ⟩
    π₁                                               ∎

  -- min(n,m) + max(n,m) ≈ n + m
  -- needs: max = sum∘⟨sub,π₂⟩ (unfold), sum-assoc, sum-min-sub, η
  sum-min-max : sum ∘ ⟨ min , max ⟩ ≈ sum
  sum-min-max = begin
    sum ∘ ⟨ min , max ⟩                              ≈⟨ sum-assoc•  ⟨ 
    sum ∘ ⟨ sum ∘ ⟨ min , sub ⟩ , π₂ ⟩               ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ sum-min-sub ⟩ 
    sum ∘ ⟨ π₁ , π₂ ⟩                                ≈⟨ elimʳ η ⟩
    sum                                              ∎

  -- min is commutative -- reduction to max-comm via the cancel/sum-min-max trick
  -- needs: max-comm, sum-min-max, sum-comm, cancel
  min-comm : min ∘ swap ≈ min
  min-comm = cancel $ begin
    sum ∘ ⟨ min ∘ swap , max ⟩                 ≈⟨ refl⟩∘⟨ (⟨⟩-congˡ max-comm ○ sym ⟨⟩∘) ⟩    
    sum ∘ ⟨ min , max ⟩ ∘ swap                 ≈⟨ pullˡ sum-min-max ⟩
    sum ∘ swap                                 ≈⟨ sum-comm ○ sym sum-min-max ⟩
    sum ∘ ⟨ min , max ⟩                        ∎

  -- translation invariance of sub: (n+k) ∸ (m+k) ≈ n ∸ m
  -- needs: sum-comm• (to swap m+k into k+m), sub-sub ((a∸b)∸c ≈ a∸(b+c), backwards), sub-sum ((n+k)∸k ≈ n)
  -- proof shape: (n+k)∸(m+k) ≈ (n+k)∸(k+m) ≈ ((n+k)∸k)∸m ≈ n∸m
  sub-transl : sub ∘ ⟨ sum ∘ (π₁ ×₁ id) , sum ∘ (π₂ ×₁ id) ⟩ ≈ sub ∘ π₁
  sub-transl = begin
    sub ∘ ⟨ sum ∘ (π₁ ×₁ id) , sum ∘ (π₂ ×₁ id) ⟩               ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (∘-resp-≈ʳ (⟨⟩-congˡ identityˡ) ○ sum-comm•) ⟩
    sub ∘ ⟨ sum ∘ (π₁ ×₁ id) , sum ∘ ⟨ π₂ , π₂ ∘ π₁ ⟩ ⟩         ≈⟨ pullˡ sub-sub ○ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁ ○ project₁) (pullʳ (first∘⟨⟩ ○ ⟨⟩-congʳ project₂))) ⟨
    sub ∘ (sub ×₁ id) ∘ ⟨ ⟨ sum ∘ (π₁ ×₁ id) , π₂ ⟩ , π₂ ∘ π₁ ⟩ ≈⟨ refl⟩∘⟨ first∘⟨⟩  ⟩ 
    sub ∘ ⟨ sub ∘ ⟨ sum ∘ (π₁ ×₁ id) , π₂ ⟩ , π₂ ∘ π₁ ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (⟨⟩-congˡ (sym π₂∘first) ○ sym ⟨⟩∘)) ⟩ 
    sub ∘ ⟨ sub ∘ ⟨ sum , π₂ ⟩ ∘ (π₁ ×₁ id) , π₂ ∘ π₁ ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (pullˡ sub-sum ○ project₁) ⟩ 
    sub ∘ ⟨ π₁ ∘ π₁ , π₂ ∘ π₁ ⟩                                 ≈⟨ refl⟩∘⟨ (sym ⟨⟩∘ ○ elimˡ η) ⟩
    sub ∘ π₁                                                    ∎

  -- translation invariance of min: min(n,m) + k ≈ min(n+k, m+k)
  -- needs: sum-min-sub, sub-transl, cancel, sum-assoc, sum-comm
  min-transl : sum ∘ (min ×₁ id) ≈ min ∘ ⟨ sum ∘ (π₁ ×₁ id) , sum ∘ (π₂ ×₁ id) ⟩
  min-transl = cancel $ begin
    sum ∘ ⟨ sum ∘ (min ×₁ id) , sub ∘ π₁ ⟩                             ≈⟨ sum-assoc• ○ ∘-resp-≈ʳ (⟨⟩-congˡ (sum-comm• ○ ∘-resp-≈ʳ (⟨⟩-congˡ identityˡ))) ⟩
    sum ∘ ⟨ min ∘ π₁ , sum ∘ ⟨ sub ∘ π₁ , π₂ ⟩ ⟩                       ≈⟨ sym sum-assoc• ○ ∘-resp-≈ʳ (⟨⟩-congʳ (∘-resp-≈ʳ (sym ⟨⟩∘))) ⟩
    sum ∘ ⟨ sum ∘ ⟨ min , sub ⟩ ∘ π₁ , π₂ ⟩                            ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullˡ sum-min-sub) (sym identityˡ) ⟩   
    sum ∘ (π₁ ×₁ id)                                                   ≈⟨ pullˡ sum-min-sub ○ project₁ ⟨
    sum ∘ ⟨ min , sub ⟩ ∘ ⟨ sum ∘ (π₁ ×₁ id) , sum ∘ (π₂ ×₁ id) ⟩      ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ sub-transl) ⟩
    sum ∘ ⟨ min ∘ ⟨ sum ∘ (π₁ ×₁ id) , sum ∘ (π₂ ×₁ id) ⟩ , sub ∘ π₁ ⟩ ∎

  -- min(n∸m, m∸n) ≈ 0
  -- needs: min-transl, sum-min-sub (applied to n and to m), min-comm, cancel
  min-subs : min ∘ ⟨ sub , sub ∘ swap ⟩ ≈ z ∘ !
  min-subs = cancel $ begin
    sum ∘ ⟨ min ∘ ⟨ sub , sub ∘ swap ⟩ , min ⟩                                                                          ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (sym identityˡ) ⟩
    sum ∘ ⟨ min ∘ ⟨ sub , sub ∘ swap ⟩ , id ∘ min ⟩                                                                     ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟨
    sum ∘ ((min ×₁ id) ∘ ⟨ ⟨ sub , sub ∘ swap ⟩ , min ⟩)                                                                ≈⟨ pullˡ min-transl ○ pullʳ ⟨⟩∘ ⟩
    min ∘ ⟨ (sum ∘ (π₁ ×₁ id)) ∘ ⟨ ⟨ sub , sub ∘ swap ⟩ , min ⟩ , (sum ∘ (π₂ ×₁ id)) ∘ ⟨ ⟨ sub , sub ∘ swap ⟩ , min ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ step₁) (pullʳ step₂) ⟩
    min ∘ ⟨ sum ∘ ⟨ sub , min ⟩ , sum ∘ ⟨ sub ∘ swap , min ⟩ ⟩                                                          ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (sum-comm• ○ sum-min-sub) lem₂ ⟩
    min ∘ ⟨ π₁ , π₂ ⟩                                                                                                   ≈⟨ elimʳ η ⟩
    min                                                                                                                 ≈⟨ sum-zˡ ⟨
    sum ∘ ⟨ z ∘ ! , min ⟩                                                                                               ∎
      where
        -- (π₁ ×₁ id) ∘ ⟨ ⟨n∸m,m∸n⟩ , min(n,m) ⟩ ≈ ⟨ n∸m , min(n,m) ⟩
        step₁ : (π₁ ×₁ id) ∘ ⟨ ⟨ sub , sub ∘ swap ⟩ , min ⟩ ≈ ⟨ sub , min ⟩
        step₁ = ×₁∘⟨⟩ ○ ⟨⟩-cong₂ project₁ identityˡ

        -- (π₂ ×₁ id) ∘ ⟨ ⟨n∸m,m∸n⟩ , min(n,m) ⟩ ≈ ⟨ m∸n , min(n,m) ⟩
        step₂ : (π₂ ×₁ id) ∘ ⟨ ⟨ sub , sub ∘ swap ⟩ , min ⟩ ≈ ⟨ sub ∘ swap , min ⟩
        step₂ = ×₁∘⟨⟩ ○ ⟨⟩-cong₂ project₂ identityˡ

        -- (m∸n) + min(n,m) ≈ m
        lem₂ : sum ∘ ⟨ sub ∘ swap , min ⟩ ≈ π₂
        lem₂ = begin
          sum ∘ ⟨ sub ∘ swap , min ⟩            ≈⟨ sum-comm• ⟩
          sum ∘ ⟨ min , sub ∘ swap ⟩            ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ min-comm ⟨
          sum ∘ ⟨ min ∘ swap , sub ∘ swap ⟩     ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟨
          sum ∘ (⟨ min , sub ⟩ ∘ swap)          ≈⟨ pullˡ sum-min-sub ⟩
          π₁ ∘ swap                             ≈⟨ project₁ ⟩
          π₂                                    ∎

  -- a ∸ b ≈ a ∸ min(a,b)
  -- needs: sub-sum (already in file: (x+y)∸y ≈ x), sum-comm, sum-min-sub
  sub-min : sub ≈ sub ∘ ⟨ π₁ , min ⟩
  sub-min = begin
    sub                                                ≈⟨ project₁ ⟨
    π₁ ∘ ⟨ sub , min ⟩                                 ≈⟨ pullˡ sub-sum ⟨
    sub ∘ ⟨ sum , π₂ ⟩ ∘ ⟨ sub , min ⟩                 ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟩
    sub ∘ ⟨ sum ∘ ⟨ sub , min ⟩ , min ⟩                ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ sum-sub-min ⟩
    sub ∘ ⟨ π₁ , min ⟩                                 ∎
      where
        -- (n∸m) + min(n,m) ≈ n
        sum-sub-min : sum ∘ ⟨ sub , min ⟩ ≈ π₁
        sum-sub-min = sum-comm• ○ sum-min-sub

  -- the goal: n ∸ m ≈ (n ∸ m) ∸ (m ∸ n)
  -- needs: sub-min (rewrite (n∸m)∸(m∸n) as (n∸m)∸min(n∸m,m∸n)), min-disjoint, sub-zʳ
  sub-sub-comm : sub ≈ sub ∘ ⟨ sub , sub ∘ swap ⟩
  sub-sub-comm = begin
    sub                                                ≈⟨ sub-zʳ ⟨ 
    sub ∘ ⟨ sub , z ∘ ! ⟩                              ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ min-subs ⟨  
    sub ∘ ⟨ sub , min ∘ ⟨ sub , sub ∘ swap ⟩ ⟩         ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-congʳ project₁) ⟨ 
    sub ∘ ⟨ π₁ , min ⟩ ∘ ⟨ sub , sub ∘ swap ⟩          ≈⟨ pushˡ sub-min ⟨ 
    sub ∘ ⟨ sub , sub ∘ swap ⟩                         ∎

  -- n ∸ (k+1) = n ⟹ n = 0
  n∸sk≈n : ∀ {X} {n k : X ⇒ N} → sub ∘ ⟨ n , s ∘ k ⟩ ≈ n → n ≈ z ∘ !
  n∸sk≈n {X}{n}{k} eq = sym (sym sub-Δ• ○ pushʳ (sym first∘⟨⟩) ○ ∘-resp-≈ˡ n∸k≈n ○ cancelʳ project₁)
    where
      sk∸n≈sk : sub ∘ ⟨ s ∘ k , n ⟩ ≈ s ∘ k
      sk∸n≈sk = cancel $ begin
        sum ∘ ⟨ sub ∘ ⟨ s ∘ k , n ⟩ , n ⟩         ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ project₂ ) ⟨ 
        max ∘ ⟨ s ∘ k , n ⟩                       ≈⟨ pushˡ max-comm ○ ∘-resp-≈ʳ swap∘⟨⟩ ⟩
        max ∘ ⟨ n , s ∘ k ⟩                       ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟩ 
        sum ∘ ⟨ sub ∘ ⟨ n , s ∘ k ⟩ , s ∘ k ⟩     ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ eq ⟩
        sum ∘ ⟨ n , s ∘ k ⟩                       ≈⟨ sum-comm• ⟩
        sum ∘ ⟨ s ∘ k , n ⟩                       ∎
        
      1∸n≈1 : sub ∘ ⟨ s ∘ z ∘ ! , n ⟩ ≈ s ∘ z ∘ !
      1∸n≈1 = begin
        sub ∘ ⟨ s ∘ z ∘ ! , n ⟩                   ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ sn-n ⟨
        sub ∘ ⟨ sub ∘ ⟨ s ∘ k , k ⟩ , n ⟩         ≈⟨ sub-sub• ⟩
        sub ∘ ⟨ s ∘ k , sum ∘ ⟨ k , n ⟩ ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ sum-comm• ⟩
        sub ∘ ⟨ s ∘ k , sum ∘ ⟨ n , k ⟩ ⟩         ≈⟨ sub-sub• ⟨        
        sub ∘ ⟨ sub ∘ ⟨ s ∘ k , n ⟩ , k ⟩         ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ sk∸n≈sk ⟩
        sub ∘ ⟨ s ∘ k , k ⟩                       ≈⟨ sn-n ⟩
        s ∘ z ∘ !                                 ∎

      n∸1≈n : sub ∘ ⟨ n , s ∘ z ∘ ! ⟩ ≈ n
      n∸1≈n = cancel $ begin
        sum ∘ ⟨ sub ∘ ⟨ n , s ∘ z ∘ ! ⟩ , s ∘ z ∘ ! ⟩   ≈⟨ sym (pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ project₂)) ⟩
        max ∘ ⟨ n , s ∘ z ∘ ! ⟩                         ≈⟨ max-comm• ⟩ 
        max ∘ ⟨ s ∘ z ∘ ! , n ⟩                         ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-congˡ project₂) ⟩ 
        sum ∘ ⟨ sub ∘ ⟨ s ∘ z ∘ ! , n ⟩ , n ⟩           ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ 1∸n≈1 ⟩
        sum ∘ ⟨ s ∘ z ∘ ! , n ⟩                         ≈⟨ sum-comm• ⟩
        sum ∘ ⟨ n , s ∘ z ∘ ! ⟩                         ∎

      n∸sk≈n∸k : sub ∘ (n ×₁ s) ≈ sub ∘ (n ×₁ id)
      n∸sk≈n∸k = begin
        sub ∘ (n ×₁ s)                                  ≈⟨ ∘-resp-≈ʳ (sym identityʳ ○ ∘-resp-≈ʳ (sym η) ○ ×₁∘⟨⟩) ⟩
        sub ∘ ⟨ n ∘ π₁ , s ∘ π₂ ⟩                       ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (sym (pushʳ (sym first∘⟨⟩) ○ pushˡ sum-sˡ ○ ∘-resp-≈ʳ sum-zˡ)) ⟩
        sub ∘ ⟨ n ∘ π₁ , sum ∘ ⟨ s ∘ z ∘ ! , π₂ ⟩ ⟩     ≈⟨ sym sub-sub• ⟩
        sub ∘ ⟨ sub ∘ ⟨ n ∘ π₁ , s ∘ z ∘ ! ⟩ , π₂ ⟩     ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ʳ (⟨⟩-congˡ (pushʳ (pushʳ !-unique₂)) ○ sym ⟨⟩∘) ○ pullˡ n∸1≈n) ⟩
        sub ∘ ⟨ n ∘ π₁ , π₂ ⟩                           ≈⟨ sym (∘-resp-≈ʳ (sym identityʳ ○ ∘-resp-≈ʳ (sym η) ○ ×₁∘⟨⟩ ○ ⟨⟩-congˡ identityˡ)) ⟩
        sub ∘ (n ×₁ id)                                 ∎

      n∸k≈n : sub ∘ (n ×₁ id) ≈ n ∘ π₁
      n∸k≈n = prec-unique (pullʳ first∘⟨⟩ ○ sub-zʳ ○ identityʳ) (pullʳ first∘second ○ n∸sk≈n∸k ○ sym project₁)
        ○ sym (prec-unique (cancelʳ project₁) (pullʳ π₁∘second ○ sym project₁))
      
  -- n ∸ m > 0 ⟹ m ∸ n = 0
  n∸m>0→m∸n=0 : ∀ {X} {n m k : X ⇒ N} → sub ∘ ⟨ n , m ⟩ ≈ s ∘ k → sub ∘ ⟨ m , n ⟩ ≈ z ∘ !
  n∸m>0→m∸n=0 {X}{n}{m}{k} eq = n∸sk≈n $ begin
    sub ∘ ⟨ sub ∘ ⟨ m , n ⟩ , s ∘ k ⟩                          ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (sym (assoc ○ ∘-resp-≈ʳ swap∘⟨⟩ ○ eq)) ⟩
    sub ∘ ⟨ sub ∘ ⟨ m , n ⟩ , (sub ∘ swap) ∘ ⟨ m , n ⟩ ⟩       ≈⟨ sym (pullʳ ⟨⟩∘) ⟩
    (sub ∘ ⟨ sub , sub ∘ swap ⟩) ∘ ⟨ m , n ⟩                   ≈⟨ sym sub-sub-comm ⟩∘⟨ refl ⟩
    sub ∘ ⟨ m , n ⟩                                            ∎
    
  -- n ∸ m = k+1 ⟹ n = (k + m) + 1
  sub>0 : ∀ {X} {n m k : X ⇒ N} → sub ∘ ⟨ n , m ⟩ ≈ s ∘ k → n ≈ s ∘ sum ∘ ⟨ k , m ⟩
  sub>0{X}{n}{m}{k} eq = begin
    n                         ≈⟨ sum-zˡ ⟨
    sum ∘ ⟨ z ∘ ! , n ⟩       ≈⟨ pushʳ (unique (pullˡ project₁ ○ eq') (pullˡ project₂ ○ project₂)) ⟩
    max ∘ ⟨ m , n ⟩           ≈⟨ pushˡ max-comm ○ ∘-resp-≈ʳ swap∘⟨⟩ ⟩
    max ∘ ⟨ n , m ⟩           ≈⟨ pushʳ (unique (pullˡ project₁ ○ eq) (pullˡ project₂ ○ project₂)) ⟨
    sum ∘ ⟨ s ∘ k , m ⟩       ≈⟨ pushʳ (sym first∘⟨⟩) ○ pushˡ sum-sˡ ⟩
    s ∘ sum ∘ ⟨ k , m ⟩       ∎
      where
        eq' : sub ∘ ⟨ m , n ⟩ ≈ z ∘ !
        eq' = n∸m>0→m∸n=0 eq