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