Cubical Agda represents equality proofs as functions from an "interval" (a structure with two end points I₀ and I₁) to some type, such that if we have such a function `f : I → τ` then it is considered as proof that `Eq (f I₀) (f I₁)`. This works because those functions from I are special: the operations provided on I are limited such that they basically can't examine whether they have an I₀ or an I₁. So they're necessarily "constant functions".
In Typer we can represent a similar idea using erasable arguments:
Eq.eq : (f : Bool ≡> ?τ) → Eq (f true) (f false);
notice the `≡>` on the type of `f` which means that this function can't use its boolean argument in any significant way because it'll be erased.
So `Eq x y` basically is a proof that we were able to provide a constant function that returns `x` or `y` depending on a boolean that it's not allowed to use.
[ Note: in reality, Typer's erasable arguments are also implicit, so rather than `f true` we have to write `f (_ := true)` to explicitly provide those erasable arguments. But I'll write it the sloppy way in this message. ]
So we can define our usual reflection constructor:
Eq.refl : Eq ?x ?x; Eq.refl = Eq.eq (λ_ ≡> ?x);
things To be interesting, tho, we do need those functions to be not-quite-constant. For that reason, we add an eliminator
Eq.uneq : (x : ?τ) → (y : ?τ) → Eq x y → Bool ≡> ?τ;
with reduction rules:
Eq.uneq x y eq true ↝ x Eq.uneq x y eq false ↝ y
IOW, `Eq.uneq x y eq` returns a function which takes an erasable argument and returns different results depending on that argument. This is a bit weird since a function should not be allowed to look at its erasable argument, but it's exceptionally tolerated because we have a proof that the two possible return values are actually equal, so they're not really different after all.
With that we can prove functional extensionality:
funext : ((x : ?τ) → Eq (?f x) (?g x)) → Eq ?f ?g; funext eqf = Eq.eq (λ i ≡> λx → Eq.uneq (?f x) (?g x) (eqf x) i);
What's so special about an erasable `Bool` (a.k.a `I`), tho?
We can generalize the above to any function taking an erasable argument:
Const : (τ₁ → τ₂) → Type; Const.in : (f : τ₁ ≡> τ₂) → Const (λx → f x); Const.out : (f : τ₁ → τ₂) → Const f → τ₁ ≡> τ₂;
such that
Const.out f cst x ↝ f x
And we can recover the old `Eq` with:
Eq x y = Const (λi → if i then x else y);
But when we try to prove functional extensionality:
funext : ((x : ?τ) → Const (λi → if i then ?f x else ?g x)) → Const (λi → if i then ?f else ?g); funext eqf = Const.in (λi ≡> λx → Const.out (λi → if i then ?f x else ?g x) (eqf x) i) ↝ Const.in (λi ≡> λx → if i then ?f x else ?g x);
[ Let's disregard the fact after this reduction `i` is used in a way that's incompatible with an erasable argument. ] This does not have the desired type because
Const (λi → if i then ?f else ?g); ≠ Const (λi → λx → if i then ?f x else ?g x)
We'd need functional extensionality to prove functional extensionality :-(
So, in a sense, what's special about `Eq x y` compared to `Const f` is that it provides an extensional representation of the constant function: `Const f` exposes the intensional definition of `f`, which ends up being too detailed for what we want. In constrast `Eq.eq` returns an `Eq x y` whose type hides the intensional definition of the witness function, which is key to making it possible to prove `funext`.
Stefan