Fancy induction principle for W-types

WInd.agda

{- Question: https://stackoverflow.com/questions/79894235/can-we-prove-equal-subcases-have-equal-induction-hypotheses-in-recursion-princip
   I don't think this is possible without funext -}

module W-Ind {i j}(A : Set i)(B : A → Set j) where

open import Level
open import Relation.Binary.PropositionalEquality renaming (subst to tr; cong to ap)
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)

postulate
  fext : ∀ {i j}{A : Set i}{B : A → Set j}{f g : ∀ a → B a} → (∀ a → f a ≡ g a) → f ≡ g

UIP : ∀ {i}{A : Set i}{x y : A}{p q : x ≡ y} → p ≡ q
UIP {p = refl}{refl} = refl

data W : Set (i ⊔ j) where
  sup : (a : A) → (B a → W) → W

module Elim {k}
            (Wᵒ   : W → Set k)
            (supᵒ : ∀ {a}(f : B a → W)(fᵒ : ∀ b → Wᵒ (f b))(ext : ∀ b b' (p : f b ≡ f b') → tr Wᵒ p (fᵒ b) ≡ fᵒ b')
                    → Wᵒ (sup a f)) where

  supᵒ≡ : ∀ {a}{f : B a → W}{fᵒ fᵒ' : ∀ b → Wᵒ (f b)}(f~ : fᵒ ≡ fᵒ')
          {ext  : ∀ b b' (p : f b ≡ f b') → tr Wᵒ p (fᵒ b) ≡ fᵒ b'}
          {ext' : ∀ b b' (p : f b ≡ f b') → tr Wᵒ p (fᵒ' b) ≡ fᵒ' b'}
          → supᵒ f fᵒ ext ≡ supᵒ f fᵒ' ext'
  supᵒ≡ {f = f}{fᵒ} refl = ap (supᵒ f fᵒ) (fext λ _ → fext λ _ → fext λ _ → UIP)

  R : ∀ w → Wᵒ w → Set (i ⊔ j ⊔ k)
  R (sup a f) wᵒ = ∃₂ λ fᵒ ext → (∀ b → R (f b) (fᵒ b)) × (wᵒ ≡ supᵒ f fᵒ ext)

  right-unique : ∀ w (wᵒ wᵒ' : Wᵒ w) → R w wᵒ → R w wᵒ' → wᵒ ≡ wᵒ'
  right-unique (sup a f) wᵒ wᵒ' (fᵒ , ext , p , refl) (fᵒ' , ext' , p' , refl) =
    supᵒ≡ (fext λ b → right-unique _ _ _ (p b) (p' b))

  left-total : ∀ w → ∃ (R w)
  left-total (sup a f) =
    let fᵒ : ∀ b → Wᵒ (f b)
        fᵒ b = left-total (f b) .₁

        hyp : ∀ b → R (f b) (fᵒ b)
        hyp b = left-total (f b) .₂

        ext : ∀ b b' (p : f b ≡ f b') → tr Wᵒ p (fᵒ b) ≡ fᵒ b'
        ext b b' p =
          let Rfb  = J (λ fb' p → R fb' (tr Wᵒ p (fᵒ b))) p (hyp b)
              Rfb' = hyp b'
          in right-unique _ _ _ Rfb Rfb'

    in supᵒ f fᵒ ext , fᵒ , ext , hyp , refl

  elim : ∀ w → Wᵒ w
  elim w = left-total w .₁