Provable `fun-ext`and "rewriting under binders" in intensional MLTT

Question

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 as we mostly care about canonicity for computational purposes, we can interpret terms of our intensional MLTT as terms of extensional MLTT. Erase J and here we go, we get canonicity w.r.t. the equational theory of extensional MLTT (which is enough to view the extended intensional MLTT as a programming language).

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

Answer 1

The new rule seems to be equivalent to funext plus the definitional equality that says that funext of constant refl is refl. As such, I don't see any issue with it. As you say equality reflection implies the new rule.

The higher-order assumptions aren't too problematic. If we have universes, we can rephrase them as plain functions. But I don't see a good reason to use the modified J rule. I like it better when eliminators of type formers make sense separately and follow a specification from some universal property, and extra axioms can be added on the top of that.