2
$\begingroup$

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?

$\endgroup$
12
  • $\begingroup$ Does stand for the identity type or judgemental equality? What is δ? $\endgroup$ Sep 2, 2023 at 17:37
  • $\begingroup$ You should explain what Γ (Δ ⊦ α : A) (Δ ⊦ β : a₀ ≡ α) ⊦ B type is supposed to mean. What is a context, precisely? What are the judgement forms? You're changing these notions in a fundamental way, so you should explain the changes. $\endgroup$ Sep 2, 2023 at 17:39
  • $\begingroup$ stands for the identity type, like in Agda. Regarding δ: just like we use the notation x. t to stand for a family t in the background context extended by some x : ?, I have δ.t standing for a family t in the background context extended by a telescope δ : ?. In that particular case δ : Δ. A context is a snoc-list of families of types (where families can depend on preceding families). Families can be eliminated just like variables in normal MLTT, but now we need to provide an instance of the context the family depends on. $\endgroup$
    – Russoul
    Sep 2, 2023 at 20:21
  • $\begingroup$ Of course there is a lot to it, but hopefully that conveys the idea. All that's new is that we replace dependence on type (x : A) with dependence on family (Δ ⊦ x : A) $\endgroup$
    – Russoul
    Sep 2, 2023 at 20:22
  • $\begingroup$ I vaguely remember that Mike Shulman at some point was asking & thinking about having such multi-level contexts. Is he listening? $\endgroup$ Sep 2, 2023 at 22:38

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ But maybe if we reformulate type theory via the "family of types" contexts instead of "plain types" contexts the new J would reflect some universal property? $\endgroup$
    – Russoul
    Sep 3, 2023 at 10:40
  • $\begingroup$ @Russoul: Maybe. The burden on proof is on the person suggesting that there is such a thing. $\endgroup$ Sep 3, 2023 at 17:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.