A puzzle about an "extensional" induction principle for W-types

W.agda

{-# OPTIONS --without-K #-}
module W where
open import Data.Container.Core
open import Data.Container.Relation.Unary.All
open import Data.W
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- Originally asked by Jasper Hugunin at https://stackoverflow.com/questions/79894235

-- The goal is to show the following induction principle for W, where
-- the induction hypothesis is assumed to be "extensional" in the sense
-- that it yields equal results for equal subtrees.
module _
  {ℓ ℓ' ℓ''} {A : Set ℓ} {B : A → Set ℓ'}
  (P : W (A ▷ B) → Set ℓ'')
  (ps : {a : A} {f : B a → W (A ▷ B)}
      → (IH : ∀ ba → P (f ba))
      → (ext : ∀ b1 b2 → (p : f b1 ≡ f b2) → subst P p (IH b1) ≡ IH b2)
      → P (sup (a , f)))
  where
  ΠP = (w : W (A ▷ B)) → P w

  -- We can do this by defining the induction principle by pattern matching,
  -- mutually with the fact that it preserves equality.
  mutual
    W-ind : ΠP
    W-ind (sup (a , f)) = ps (λ ba → W-ind (f ba))
      λ b1 b2 p → dcong-W-ind (f b1) (f b2) p
      -- Inlining dcong-W-ind as follows causes the termination checker to complain about `W-ind w2`:
      -- λ b1 b2 p → J (λ w2 q → subst P q (W-ind (f b1)) ≡ W-ind w2) p refl

    dcong-W-ind : ∀ w1 w2 → (p : w1 ≡ w2) → subst P p (W-ind w1) ≡ W-ind w2
    dcong-W-ind w1 w2 refl = refl

  -- Agda's termination checker accepts the above, but can this actually be
  -- translated to eliminators? Should the motive be generalised somehow?
  W-ind-elim : ΠP
  W-ind-elim = induction _ λ (all x) → ps x {! ??? !}