=========================
 =                       =
 =  Example: continuity  =
 =                       =
 =========================

    Chuangjie Xu, July 2019

\begin{code}

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

open import Preliminaries
open import Tplus

module Continuity where

\end{code}

■ A nucleus for moduli of continuity

\begin{code}

J : Ty → Ty
J σ = σ ⊠ ι

η : {Γ : Cxt} {σ : Ty} → T Γ (σ ⇾ J σ)
η = Lam (Pair · ν₀ · Zero)
--  λ x . ⟨ x , 0 ⟩

κ : {Γ : Cxt} {σ τ : Ty} → T Γ ((σ ⇾ J τ) ⇾ J σ ⇾ J τ)
κ = Lam (Lam (Pair · (Pr1 · (ν₁ · (Pr1 · ν₀)))
                   · (Max · (Pr2 · ν₀) · (Pr2 · (ν₁ · (Pr1 · ν₀))))))
--  λ g x . ⟨ (g x₁)₁ , max x₂ (g x₁)₂ ⟩

open import GentzenTranslation J η κ

Ω : {Γ : Cxt} → T Γ ((ι ⇾ ι) ⇾ J ι ⇾ J ι)
Ω = Lam (κ · Lam (Pair · (ν₁ · ν₀) · (Succ · ν₀)))
--  λ α . (λ n . ⟨ αn , n+1 ⟩)ᴷ

--
-- Internal modulus of continuity
--
Mᵀ : T ε ((ι ⇾ ι) ⇾ ι) → T ε ((ι ⇾ ι) ⇾ ι)
Mᵀ f = Lam (Pr2 · (wkn (f ᴶ) · (Ω · ν₀)))

--
-- External modulus of continuity
--
M : T ε ((ι ⇾ ι) ⇾ ι) → ℕᴺ → ℕ
M f α = pr₂ (⟦ f ᴶ ⟧ (⟦ Ω ⟧ α))

{- Todo: show ∀ f α → ⟦ Mᵀ f ⟧ α = M f α -}

\end{code}

■ Correctness

Use the lifting nucleus b σ = (ι ⇾ ι) ⇾ σ.

\begin{code}

open import Lifting (ι ⇾ ι) renaming (J    to b
                                    ; η    to ηᵇ
                                    ; κ    to κᵇ
                                    ; ⟨_⟩ᴶ to ⟨_⟩ᵇ
                                    ; ⟪_⟫ᴶ to ⟪_⟫ᵇ
                                    ; ⟨_⟩ᵛ to ⟨_⟩ⱽ
                                    ; KE   to KEᵇ
                                    ; _ᴶ   to _ᵇ)

Ωᵇ : {Γ : Cxt} → T Γ (b ι ⇾ b ι)
Ωᵇ = Lam (Lam (ν₀ · (ν₁ · ν₀)))
--   λ f α . α (f α)

Lemma[≐] : (f : T ε (b ι)) (α : ℕᴺ) → ⟦ f ⟧ α ≡ ⟦ f ᵇ · Ωᵇ ⟧ α
Lemma[≐] f α = Lemma[R] f α ⋆ (ap α)

C : (ρ : Ty) → ℕᴺ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ → ⟦ ⟨ ρ ⟩ᵇ ⟧ʸ → Set
C  ι      α (k , m)      f      = f α ≡ k × (∀ β → α ≡[ m ] β → f α ≡ f β)
C (σ ⇾ τ) α  g           h      = ∀ {x y} → C σ α x y → C τ α (g x) (h y)
C (σ ⊠ τ) α (x , y)     (f , g) = C σ α x f × C τ α y g
C (σ ⊞ τ) α (inl x , m)  f      = case (λ z → C σ α x z × (∀ β → α ≡[ m ] β → f α ≡ f β)) (λ _ → 𝟘) (f α)
C (σ ⊞ τ) α (inr y , m)  f      = case (λ _ → 𝟘) (λ z → C τ α y z × (∀ β → α ≡[ m ] β → f α ≡ f β)) (f α)

C[KEᶥ] : (ρ : Ty) {Γ Δ : Cxt} {γ : ⟦ Γ ⟧ˣ} {δ : ⟦ Δ ⟧ˣ} (α : ℕᴺ)
       → {f : ℕ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ} {g : ℕ → ⟦ ⟨ ρ ⟩ᵇ ⟧ʸ}
       → ((i : ℕ) → C ρ α (f i) (g i))
       → C (ι ⇾ ρ) α (⟦ KE ρ ⟧ᵐ γ f) (⟦ KEᵇ ρ ⟧ᵐ δ g)

C[KE⁺] : (ρ : Ty) (α : ℕᴺ) {σ τ : Ty} {Γ Δ : Cxt} {γ : ⟦ Γ ⟧ˣ} {δ : ⟦ Δ ⟧ˣ}
       → (f : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ + ⟦ ⟨ τ ⟩ᴶ ⟧ʸ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ)
       → (g : ⟦ ⟨ σ ⟩ᵇ ⟧ʸ + ⟦ ⟨ τ ⟩ᵇ ⟧ʸ → ⟦ ⟨ ρ ⟩ᵇ ⟧ʸ)
       → ({x : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ} {a : ⟦ ⟨ σ ⟩ᵇ ⟧ʸ} → C σ α x a → C ρ α (f (inl x)) (g (inl a)))
       → ({y : ⟦ ⟨ τ ⟩ᴶ ⟧ʸ} {b : ⟦ ⟨ τ ⟩ᵇ ⟧ʸ} → C τ α y b → C ρ α (f (inr y)) (g (inr b)))
       → C (σ ⊞ τ ⇾ ρ) α (⟦ KE ρ ⟧ᵐ γ f) (⟦ KEᵇ ρ ⟧ᵐ δ g)

Cˣ : {Γ : Cxt} → ℕᴺ → ⟦ ⟪ Γ ⟫ᴶ ⟧ˣ → ⟦ ⟪ Γ ⟫ᵇ ⟧ˣ → Set
Cˣ {ε}     _  _       _      = 𝟙
Cˣ {Γ ₊ ρ} α (γ , a) (δ , b) = Cˣ α γ δ × C ρ α a b

C[Var] : {Γ : Cxt} {ρ : Ty} {γ : ⟦ ⟪ Γ ⟫ᴶ ⟧ˣ} {δ : ⟦ ⟪ Γ ⟫ᵇ ⟧ˣ} (α : ℕᴺ)
       → Cˣ α γ δ → (i : ∥ ρ ∈ Γ ∥) → C ρ α (γ ₍ ⟨ i ⟩ᵛ ₎) (δ ₍ ⟨ i ⟩ⱽ ₎)
C[Var] α (_ , θ)  zero    = θ
C[Var] α (ζ , _) (succ i) = C[Var] α ζ i

Lemma[C] : {Γ : Cxt} {ρ : Ty} (t : T Γ ρ) (α : ℕᴺ)
         → {γ : ⟦ ⟪ Γ ⟫ᴶ ⟧ˣ} {δ : ⟦ ⟪ Γ ⟫ᵇ ⟧ˣ} → Cˣ α γ δ
         → C ρ α (⟦ t ᴶ ⟧ᵐ γ) (⟦ t ᵇ ⟧ᵐ δ)
Lemma[C] (Var i)  α ζ = C[Var] α ζ i
Lemma[C] (Lam t)  α ζ = λ x → Lemma[C] t α (ζ , x)
Lemma[C] (f · a)  α ζ = Lemma[C] f α ζ (Lemma[C] a α ζ)
Lemma[C] Zero     _ _ = refl , (λ _ _ → refl)
Lemma[C] Succ     _ _ = λ χ → ap succ (pr₁ χ) , (λ β es → ap succ (pr₂ χ β (≡[≤] es (Max-spec₀ _ _))))
Lemma[C](Rec{ρ})  α _ = λ χ ξ → C[KEᶥ] ρ α (ind χ (λ _ p → ξ (refl , (λ _ _ → refl)) p))
Lemma[C] Pair     _ _ = λ χ₀ χ₁ → χ₀ , χ₁
Lemma[C] Pr1      _ _ = pr₁
Lemma[C] Pr2      _ _ = pr₂
Lemma[C] Inj1     _ _ = λ χ → χ , (λ _ _ → refl)
Lemma[C] Inj2     _ _ = λ χ → χ , (λ _ _ → refl)
Lemma[C](Case{ρ}) α _ = λ χ ξ → C[KE⁺] ρ α _ _ χ ξ

C[Ω] : (α : ℕᴺ) → C (ι ⇾ ι) α (⟦ Ω ⟧ α) ⟦ Ωᵇ ⟧
C[Ω] α {k , m} {f} (e , p) = eq , pr
 where
  eq : α (f α) ≡ α k
  eq = ap α e
  pr : (β : ℕ → ℕ) → α ≡[ ⟦ Max ⟧ m (succ k) ] β → α (f α) ≡ β (f β)
  pr β es = begin
            α (f α) ≡⟨ eq ⟩
            α k     ≡⟨ ≡[]-< es (Max-spec₁ m (succ k)) ⟩
            β k     ≡⟨ ap β (sym e) ⟩
            β (f α) ≡⟨ ap β (p β (≡[≤] es (Max-spec₀ m (succ k)))) ⟩
            β (f β) ∎

Theorem : (f : T ε ((ι ⇾ ι) ⇾ ι))
        → (α β : ℕᴺ) → α ≡[ M f α ] β → ⟦ f ⟧ α ≡ ⟦ f ⟧ β
Theorem f α β em = begin
                   ⟦ f ⟧ α        ≡⟨ Lemma[≐] f α ⟩
                   ⟦ f ᵇ · Ωᵇ ⟧ α ≡⟨ pr₂ (Lemma[C] f α ⋆ (C[Ω] α)) β em ⟩
                   ⟦ f ᵇ · Ωᵇ ⟧ β ≡⟨ sym (Lemma[≐] f β) ⟩
                   ⟦ f ⟧ β        ∎

\end{code}

■ Detailed proofs

\begin{code}

C⁺≡LL : {σ τ : Ty} {α : ℕᴺ}
      → {w : ⟦ ⟨ σ ⊞ τ ⟩ᴶ ⟧ʸ} {f : ⟦ ⟨ σ ⊞ τ ⟩ᵇ ⟧ʸ}
      → {x : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ} {m : ℕ} {y : ⟦ ⟨ σ ⟩ᵇ ⟧ʸ}
      → pr₁ w ≡ inl x → pr₂ w ≡ m → f α ≡ inl y
      → C (σ ⊞ τ) α w f ≡ (C σ α x y × (∀ β → α ≡[ m ] β → f α ≡ f β))
C⁺≡LL refl refl = case⁼ˡ

C⁺≡LR : {σ τ : Ty} {α : ℕᴺ}
      → {w : ⟦ ⟨ σ ⊞ τ ⟩ᴶ ⟧ʸ} {f : ⟦ ⟨ σ ⊞ τ ⟩ᵇ ⟧ʸ}
      → {x : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ} {y : ⟦ ⟨ τ ⟩ᵇ ⟧ʸ}
      → pr₁ w ≡ inl x → f α ≡ inr y
      → C (σ ⊞ τ) α w f ≡ 𝟘
C⁺≡LR refl = case⁼ʳ

C⁺≡RL : {σ τ : Ty} {α : ℕᴺ}
      → {w : ⟦ ⟨ σ ⊞ τ ⟩ᴶ ⟧ʸ} {f : ⟦ ⟨ σ ⊞ τ ⟩ᵇ ⟧ʸ}
      → {x : ⟦ ⟨ τ ⟩ᴶ ⟧ʸ} {y : ⟦ ⟨ σ ⟩ᵇ ⟧ʸ}
      → pr₁ w ≡ inr x → f α ≡ inl y
      → C (σ ⊞ τ) α w f ≡ 𝟘
C⁺≡RL refl = case⁼ˡ

C⁺≡RR : {σ τ : Ty} {α : ℕᴺ}
      → {w : ⟦ ⟨ σ ⊞ τ ⟩ᴶ ⟧ʸ} {f : ⟦ ⟨ σ ⊞ τ ⟩ᵇ ⟧ʸ}
      → {x : ⟦ ⟨ τ ⟩ᴶ ⟧ʸ} {m : ℕ} {y : ⟦ ⟨ τ ⟩ᵇ ⟧ʸ}
      → pr₁ w ≡ inr x → pr₂ w ≡ m → f α ≡ inr y
      → C (σ ⊞ τ) α w f ≡ (C τ α x y × (∀ β → α ≡[ m ] β → f α ≡ f β))
C⁺≡RR refl refl = case⁼ʳ

{- Proof of
C[KEᶥ] : (ρ : Ty) {Γ Δ : Cxt} {γ : ⟦ Γ ⟧ˣ} {δ : ⟦ Δ ⟧ˣ} (α : ℕᴺ)
       → {f : ℕ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ} {g : ℕ → ⟦ ⟨ ρ ⟩ᵇ ⟧ʸ}
       → ((i : ℕ) → C ρ α (f i) (g i))
       → C (ι ⇾ ρ) α (⟦ KE ρ ⟧ᵐ γ f) (⟦ KEᵇ ρ ⟧ᵐ δ g)
-}
C[KEᶥ] ι α {f} {g} ζ {k , m} {h} (hα=k , p) = e , q
 where
  e : g (h α) α ≡ pr₁ (f k)
  e = g (h α) α ≡⟨ pr₁ (ζ (h α)) ⟩     pr₁ (f (h α))
                ≡⟨ ap (pr₁ ∘ f) hα=k ⟩ pr₁ (f k) ∎
  q : (β : ℕᴺ) → α ≡[ ⟦ Max ⟧ m (pr₂ (f k)) ] β → g (h α) α ≡ g (h β) β
  q β es = begin
           g (h α) α ≡⟨ ap (λ x → g x α) hα=k ⟩
           g k α     ≡⟨ pr₂ (ζ k) β (≡[≤] es (Max-spec₁ m _)) ⟩
           g k β     ≡⟨ ap (λ i → g i β) (sym hα=k) ⟩
           g (h α) β ≡⟨ ap (λ i → g i β) (p β (≡[≤] es (Max-spec₀ m _))) ⟩
           g (h β) β ∎
C[KEᶥ] (σ ⊠ τ) α ζ χ = C[KEᶥ] σ α (pr₁ ∘ ζ) χ , C[KEᶥ] τ α (pr₂ ∘ ζ) χ
C[KEᶥ] (σ ⊞ τ) α {f} {g} ζ {k , m} {h} (hα=k , p) = goal
 where
  n : ℕ
  n = ⟦ Max ⟧ m (pr₂ (f k))
  goal : C (σ ⊞ τ) α (pr₁ (f k) , n) (λ γ → g (h γ) γ)
  goal with inspect (pr₁ (f k))
  goal | (inl x) with≡ el with inspect (g (h α) α)
  ...  | (inl a) with≡ el' = transport (λ X → X) E (claim₀ , claim₁)
   where
    E  : (C σ α x a × (∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β))
       ≡ C (σ ⊞ τ) α (pr₁ (f k) , n) (λ γ → g (h γ) γ)
    E  = sym (C⁺≡LL el refl el')
    E' : C (σ ⊞ τ) α (f k) (g k)
       ≡ (C σ α x a × (∀ β → α ≡[ pr₂ (f k) ] β → g k α ≡ g k β))
    E' = C⁺≡LL el refl (transport (λ i → g i α ≡ inl a) hα=k el')
    claim₀ : C σ α x a
    claim₀ = pr₁ (transport (λ X → X) E' (ζ k))
    claim₁ : ∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β
    claim₁ β en = begin
                  g (h α) α ≡⟨ ap (λ i → g i α) hα=k ⟩
                  g k α     ≡⟨ pr₂ (transport (λ X → X) E' (ζ k)) β (≡[≤] en (Max-spec₁ m _)) ⟩
                  g k β     ≡⟨ ap (λ i → g i β) (sym hα=k) ⟩
                  g (h α) β ≡⟨ ap (λ i → g i β) (p β (≡[≤] en (Max-spec₀ m _))) ⟩
                  g (h β) β ∎
  ...  | (inr b) with≡ er' = 𝟘-elim (transport (λ X → X) E (ζ k))
   where
    E : C (σ ⊞ τ) α (f k) (g k) ≡ 𝟘
    E = C⁺≡LR el (transport (λ i → g i α ≡ inr b) hα=k er')
  goal | (inr y) with≡ er with inspect (g (h α) α)
  ...  | (inl a) with≡ el' = 𝟘-elim (transport (λ X → X) E (ζ k))
   where
    E : C (σ ⊞ τ) α (f k) (g k) ≡ 𝟘
    E = C⁺≡RL er (transport (λ i → g i α ≡ inl a) hα=k el')
  ...  | (inr b) with≡ er' = transport (λ X → X) E (claim₀ , claim₁)
   where
    E  : (C τ α y b × (∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β))
       ≡ C (σ ⊞ τ) α (pr₁ (f k) , n) (λ γ → g (h γ) γ)
    E  = sym (C⁺≡RR er refl er')
    E' : C (σ ⊞ τ) α (f k) (g k)
       ≡ (C τ α y b × (∀ β → α ≡[ pr₂ (f k) ] β → g k α ≡ g k β))
    E' = C⁺≡RR er refl (transport (λ i → g i α ≡ inr b) hα=k er')
    claim₀ : C τ α y b
    claim₀ = pr₁ (transport (λ X → X) E' (ζ k))
    claim₁ : ∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β
    claim₁ β en = begin
                  g (h α) α ≡⟨ ap (λ i → g i α) hα=k ⟩
                  g k α     ≡⟨ pr₂ (transport (λ X → X) E' (ζ k)) β (≡[≤] en (Max-spec₁ m _)) ⟩
                  g k β     ≡⟨ ap (λ i → g i β) (sym hα=k) ⟩
                  g (h α) β ≡⟨ ap (λ i → g i β) (p β (≡[≤] en (Max-spec₀ m _))) ⟩
                  g (h β) β ∎
C[KEᶥ] (σ ⇾ τ) α ζ χ = λ ξ → C[KEᶥ] τ α (λ i → ζ i ξ) χ

{- Proof of
C[KE⁺] : (ρ : Ty) (α : ℕᴺ) {σ τ : Ty} {Γ Δ : Cxt} {γ : ⟦ Γ ⟧ˣ} {δ : ⟦ Δ ⟧ˣ}
       → (f : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ + ⟦ ⟨ τ ⟩ᴶ ⟧ʸ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ)
       → (g : ⟦ ⟨ σ ⟩ᵇ ⟧ʸ + ⟦ ⟨ τ ⟩ᵇ ⟧ʸ → ⟦ ⟨ ρ ⟩ᵇ ⟧ʸ)
       → ({x : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ} {a : ⟦ ⟨ σ ⟩ᵇ ⟧ʸ} → C σ α x a → C ρ α (f (inl x)) (g (inl a)))
       → ({y : ⟦ ⟨ τ ⟩ᴶ ⟧ʸ} {b : ⟦ ⟨ τ ⟩ᵇ ⟧ʸ} → C τ α y b → C ρ α (f (inr y)) (g (inr b)))
       → C (σ ⊞ τ ⇾ ρ) α (⟦ KE ρ ⟧ᵐ γ f) (⟦ KEᵇ ρ ⟧ᵐ δ g)
-}
C[KE⁺] ι α {σ} {τ} f g ζ ξ {inl x , m} {h} χ with inspect (h α)
... | (inl a) with≡ el = e , p
 where
  claim₀ : C σ α x a
         × (∀ β → α ≡[ m ] β → h α ≡ h β)
  claim₀ = transport (case _ _) el χ
  claim₁ : g (inl a) α ≡ pr₁ (f (inl x))
         × (∀ β → α ≡[ pr₂ (f (inl x)) ] β → g (inl a) α ≡ g (inl a) β)
  claim₁ = ζ (pr₁ claim₀)
  e : g (h α) α ≡ pr₁ (f (inl x))
  e = begin
      g (h α) α       ≡⟨ ap (λ i → g i α) el ⟩
      g (inl a) α     ≡⟨ pr₁ claim₁ ⟩
      pr₁ (f (inl x)) ∎
  p : ∀ β → α ≡[ ⟦ Max ⟧ m (pr₂ (f (inl x))) ] β → g (h α) α ≡ g (h β) β
  p β es = begin
           g (h α) α   ≡⟨ ap (λ i → g i α) el ⟩
           g (inl a) α ≡⟨ pr₂ claim₁ β (≡[≤] es (Max-spec₁ m _)) ⟩
           g (inl a) β ≡⟨ ap (λ i → g i β) (sym el) ⟩
           g (h α) β   ≡⟨ ap (λ i → g i β) (pr₂ claim₀ β (≡[≤] es (Max-spec₀ m _))) ⟩
           g (h β) β   ∎
... | (inr b) with≡ er = 𝟘-elim (transport (case _ _) er χ)
C[KE⁺] ι α {σ} {τ} f g ζ ξ {inr y , m} {h} χ with inspect (h α)
... | (inl a) with≡ el = 𝟘-elim (transport (case _ _) el χ)
... | (inr b) with≡ er = e , p
 where
  claim₀ : C τ α y b
         × (∀ β → α ≡[ m ] β → h α ≡ h β)
  claim₀ = transport (case _ _) er χ
  claim₁ : g (inr b) α ≡ pr₁ (f (inr y))
         × (∀ β → α ≡[ pr₂ (f (inr y)) ] β → g (inr b) α ≡ g (inr b) β)
  claim₁ = ξ (pr₁ claim₀)
  e : g (h α) α ≡ pr₁ (f (inr y))
  e = begin
      g (h α) α       ≡⟨ ap (λ i → g i α) er ⟩
      g (inr b) α     ≡⟨ pr₁ claim₁ ⟩
      pr₁ (f (inr y)) ∎  
  p : ∀ β → α ≡[ ⟦ Max ⟧ m (pr₂ (f (inr y))) ] β → g (h α) α ≡ g (h β) β
  p β es = begin
           g (h α) α   ≡⟨ ap (λ i → g i α) er ⟩
           g (inr b) α ≡⟨ pr₂ claim₁ β (≡[≤] es (Max-spec₁ m _)) ⟩
           g (inr b) β ≡⟨ ap (λ i → g i β) (sym er) ⟩
           g (h α) β   ≡⟨ ap (λ i → g i β) (pr₂ claim₀ β (≡[≤] es (Max-spec₀ m _))) ⟩
           g (h β) β   ∎
C[KE⁺] (ρ₁ ⊠ ρ₂) α f g ζ ξ χ = C[KE⁺] ρ₁ α (pr₁ ∘ f) (pr₁ ∘ g) (pr₁ ∘ ζ) (pr₁ ∘ ξ) χ ,
                               C[KE⁺] ρ₂ α (pr₂ ∘ f) (pr₂ ∘ g) (pr₂ ∘ ζ) (pr₂ ∘ ξ) χ
C[KE⁺] (ρ₁ ⊞ ρ₂) α {σ} {τ} f g ζ ξ {inl x , m} {h} χ with inspect (h α)
... | (inl a) with≡ ehl = goal
 where
  n : ℕ
  n = ⟦ Max ⟧ m (pr₂ (f (inl x)))
  claim₀ : C σ α x a
         × (∀ β → α ≡[ m ] β → h α ≡ h β)
  claim₀ = transport (case _ _) ehl χ
  claim₁ : C (ρ₁ ⊞ ρ₂) α (f (inl x)) (g (inl a))
  claim₁ = ζ (pr₁ claim₀)
  goal : C (ρ₁ ⊞ ρ₂) α (pr₁ (f (inl x)) , n) (λ γ → g (h γ) γ)
  goal with inspect (pr₁ (f (inl x)))
  goal | (inl u) with≡ efl with inspect (g (h α) α)
  goal | (inl u) with≡ efl | (inl c) with≡ egl = transport (λ X → X) E (claim₂ , claim₃)
   where
    E  : (C ρ₁ α u c × (∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β))
       ≡ C (ρ₁ ⊞ ρ₂) α (pr₁ (f (inl x)) , n) (λ γ → g (h γ) γ)
    E  = sym (C⁺≡LL efl refl egl)
    E' : C (ρ₁ ⊞ ρ₂) α (f (inl x)) (g (inl a))
       ≡ (C ρ₁ α u c × (∀ β → α ≡[ pr₂ (f (inl x)) ] β → g (inl a) α ≡ g (inl a) β))
    E' = C⁺≡LL efl refl (transport (λ i → g i α ≡ inl c) ehl egl)
    claim₂ : C ρ₁ α u c
    claim₂ = pr₁ (transport (λ X → X) E' claim₁)
    claim₃ : ∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β
    claim₃ β es = begin
                  g (h α) α   ≡⟨ ap (λ z → g z α) ehl ⟩
                  g (inl a) α ≡⟨ pr₂ (transport (λ X → X) E' claim₁) β (≡[≤] es (Max-spec₁ m _)) ⟩
                  g (inl a) β ≡⟨ ap (λ z → g z β) (sym ehl) ⟩
                  g (h α) β   ≡⟨ ap (λ z → g z β) (pr₂ claim₀ β (≡[≤] es (Max-spec₀ m _))) ⟩
                  g (h β) β   ∎
  goal | (inl u) with≡ efl | (inr d) with≡ egr = 𝟘-elim (transport (λ X → X) E claim₁)
   where
    E : C (ρ₁ ⊞ ρ₂) α (f (inl x)) (g (inl a)) ≡ 𝟘
    E = C⁺≡LR efl (transport (λ i → g i α ≡ inr d) ehl egr)
  goal | (inr v) with≡ efr with inspect (g (h α) α)
  goal | (inr v) with≡ efr | (inl c) with≡ egl = 𝟘-elim (transport (λ X → X) E claim₁)
   where
    E : C (ρ₁ ⊞ ρ₂) α (f (inl x)) (g (inl a)) ≡ 𝟘
    E = C⁺≡RL efr (transport (λ i → g i α ≡ inl c) ehl egl)
  goal | (inr v) with≡ efr | (inr d) with≡ egr = transport (λ X → X) E (claim₂ , claim₃)
   where
    E  : (C ρ₂ α v d × (∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β))
       ≡ C (ρ₁ ⊞ ρ₂) α (pr₁ (f (inl x)) , n) (λ γ → g (h γ) γ)
    E  = sym (C⁺≡RR efr refl egr)
    E' : C (ρ₁ ⊞ ρ₂) α (f (inl x)) (g (inl a))
       ≡ (C ρ₂ α v d × (∀ β → α ≡[ pr₂ (f (inl x)) ] β → g (inl a) α ≡ g (inl a) β))
    E' = C⁺≡RR efr refl (transport (λ i → g i α ≡ inr d) ehl egr)
    claim₂ : C ρ₂ α v d
    claim₂ = pr₁ (transport (λ X → X) E' claim₁)
    claim₃ : ∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β
    claim₃ β es = begin
                  g (h α) α   ≡⟨ ap (λ z → g z α) ehl ⟩
                  g (inl a) α ≡⟨ pr₂ (transport (λ X → X) E' claim₁) β (≡[≤] es (Max-spec₁ m _)) ⟩
                  g (inl a) β ≡⟨ ap (λ z → g z β) (sym ehl) ⟩
                  g (h α) β   ≡⟨ ap (λ z → g z β) (pr₂ claim₀ β (≡[≤] es (Max-spec₀ m _))) ⟩
                  g (h β) β   ∎
... | (inr b) with≡ ehr = 𝟘-elim (transport (case _ _) ehr χ)
C[KE⁺] (ρ₁ ⊞ ρ₂) α {σ} {τ} f g ζ ξ {inr y , m} {h} χ with inspect (h α)
... | (inl a) with≡ ehl = 𝟘-elim (transport (case _ _) ehl χ)
... | (inr b) with≡ ehr = goal
 where
  n : ℕ
  n = ⟦ Max ⟧ m (pr₂ (f (inr y)))
  claim₀ : C τ α y b
         × (∀ β → α ≡[ m ] β → h α ≡ h β)
  claim₀ = transport (case _ _) ehr χ
  claim₁ : C (ρ₁ ⊞ ρ₂) α (f (inr y)) (g (inr b))
  claim₁ = ξ (pr₁ claim₀)
  goal : C (ρ₁ ⊞ ρ₂) α (pr₁ (f (inr y)) , n) (λ γ → g (h γ) γ)
  goal with inspect (pr₁ (f (inr y)))
  goal | (inl u) with≡ efl with inspect (g (h α) α)
  goal | (inl u) with≡ efl | (inl c) with≡ egl = transport (λ X → X) E (claim₂ , claim₃)
   where
    E  : (C ρ₁ α u c × (∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β))
       ≡ C (ρ₁ ⊞ ρ₂) α (pr₁ (f (inr y)) , n) (λ γ → g (h γ) γ)
    E  = sym (C⁺≡LL efl refl egl)
    E' : C (ρ₁ ⊞ ρ₂) α (f (inr y)) (g (inr b))
       ≡ (C ρ₁ α u c × (∀ β → α ≡[ pr₂ (f (inr y)) ] β → g (inr b) α ≡ g (inr b) β))
    E' = C⁺≡LL efl refl (transport (λ i → g i α ≡ inl c) ehr egl)
    claim₂ : C ρ₁ α u c
    claim₂ = pr₁ (transport (λ X → X) E' claim₁)
    claim₃ : ∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β
    claim₃ β es = begin
                  g (h α) α   ≡⟨ ap (λ z → g z α) ehr ⟩
                  g (inr b) α ≡⟨ pr₂ (transport (λ X → X) E' claim₁) β (≡[≤] es (Max-spec₁ m _)) ⟩
                  g (inr b) β ≡⟨ ap (λ z → g z β) (sym ehr) ⟩
                  g (h α) β   ≡⟨ ap (λ z → g z β) (pr₂ claim₀ β (≡[≤] es (Max-spec₀ m _))) ⟩
                  g (h β) β   ∎
  goal | (inl u) with≡ efl | (inr d) with≡ egr = 𝟘-elim (transport (λ X → X) E claim₁)
   where
    E : C (ρ₁ ⊞ ρ₂) α (f (inr y)) (g (inr b)) ≡ 𝟘
    E = C⁺≡LR efl (transport (λ i → g i α ≡ inr d) ehr egr)
  goal | (inr v) with≡ efr with inspect (g (h α) α)
  goal | (inr v) with≡ efr | (inl c) with≡ egl = 𝟘-elim (transport (λ X → X) E claim₁)
   where
    E : C (ρ₁ ⊞ ρ₂) α (f (inr y)) (g (inr b)) ≡ 𝟘
    E = C⁺≡RL efr (transport (λ i → g i α ≡ inl c) ehr egl)
  goal | (inr v) with≡ efr | (inr d) with≡ egr = transport (λ X → X) E (claim₂ , claim₃)
   where
    E  : (C ρ₂ α v d × (∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β))
       ≡ C (ρ₁ ⊞ ρ₂) α (pr₁ (f (inr y)) , n) (λ γ → g (h γ) γ)
    E  = sym (C⁺≡RR efr refl egr)
    E' : C (ρ₁ ⊞ ρ₂) α (f (inr y)) (g (inr b))
       ≡ (C ρ₂ α v d × (∀ β → α ≡[ pr₂ (f (inr y)) ] β → g (inr b) α ≡ g (inr b) β))
    E' = C⁺≡RR efr refl (transport (λ i → g i α ≡ inr d) ehr egr)
    claim₂ : C ρ₂ α v d
    claim₂ = pr₁ (transport (λ X → X) E' claim₁)
    claim₃ : ∀ β → α ≡[ n ] β → g (h α) α ≡ g (h β) β
    claim₃ β es = begin
                  g (h α) α   ≡⟨ ap (λ z → g z α) ehr ⟩
                  g (inr b) α ≡⟨ pr₂ (transport (λ X → X) E' claim₁) β (≡[≤] es (Max-spec₁ m _)) ⟩
                  g (inr b) β ≡⟨ ap (λ z → g z β) (sym ehr) ⟩
                  g (h α) β   ≡⟨ ap (λ z → g z β) (pr₂ claim₀ β (≡[≤] es (Max-spec₀ m _))) ⟩
                  g (h β) β   ∎
C[KE⁺] (_ ⇾ ρ) α f g ζ ξ χ θ = C[KE⁺] ρ α _ _ (λ z → ζ z θ) (λ z → ξ z θ) χ

\end{code}