I've noticed that the underlying judgemental machinery of intensional MLTT can be extended such that function extensionality becomes provable. Or in other words it becomes possible to "rewrite under binders". I came up with the idea when working on a rewrite tactic for extensional MLTT. Given a goal type, a path to a sub-expression inside the goal type, and a proof-term the tactic rewrites the sub-expression according to the proof-term (just replaces one side with another). What's interesting is that the proof-term can depend on the binders we pass by when moving along the path to the sub-expression. In intensional MLTT J plays a role similar to that tactic. But it can't rewrite inside binders (unless the term we are rewriting doesn't depend on the bound variables).

Here is what we can do to make J as powerful as that tactic:

We enhance the contexts of type theory to hold families of types instead of just types.

Here is what the J rule looks like now:

Γ ⊦ Δ ctx
Γ Δ ⊦ A type
Γ Δ ⊦ a₀ : A
Γ (Δ ⊦ α : A) (Δ ⊦ β : a₀ ≡ α) ⊦ B type
Γ ⊦ r : B(a₀, Refl)
Γ Δ ⊦ a₁ : A
Γ Δ ⊦ a : a₀ ≡ a₁
----------------------------------------------------
Γ ⊦ J δ.A δ.a₀ (α(δ). β(δ). B) r δ.a₁ δ.a : B(δ.a₁, δ.a)
Γ ⊦ J δ.A δ.a₀ (α(δ). β(δ). B) r δ.a₀ δ.Refl = r : B(δ.a₀, δ.Refl)

fun-ext is derivable:

Γ ⊦ A type
Γ (x : A) ⊦ B type
Γ ⊦ f : (x : A) → B
Γ ⊦ g : (x : A) → B
Γ ⊦ p : (x : A) → f x ≡ g x
--------------------------------------------------------------------------------------------------------------
fun-ext A (x. B) f g p ≔ J (x. B) (x. f x) (α(x). β(x). (x ↦ f x) ≡ (x ↦ α(x))) Refl (x. g x) (x. p x) : f ≡ g      

Canonicity is lost in that case. But if we simply erase J in closed evaluation we shall get canonicity back, I believe.

I'd love to get a professional opinion on the construction. Does it make sense? Do you see any obvious problems with it?