funext.md

I'm thinking on how to add funext to a Type Theory in the spirit of that answer

my understanding is that OTT, as presented, introduces computation rules for a built-in identity / propositional equality type. for example, in OTT, we'd have something like:

Eq (A,B) (a0,b0) (a1,b1)

reduce to

(Eq A a0 a1 , Eq B b0 b1)

and the way that FunExt is implemented is by merely making:

Eq (∀(x:A).(B x)) f g

reduce to

∀x:A. Eq (B x) (f x) (g x)

or, in other words, the type of equality on functions is definitionaly equivalent to the type of a function that returns an equality on each point.

now, if I understand it right, you mention that this is inconvenient for some reasons and suggest, instead, to just let the user explicitly apply type eliminators to equalities of that type. for example, if:

x : Eq (A,B) (a0,b0) (a1,b1)

then,

fst x : Eq A a0 a1

that is, by letting the user project equalities as if they were values, we can emulate OTT without the inconveniences bought by the identity type computing to something else. I suspect that, in a similar way, you also allow one to inhabit the identity type by constructing an element of the type it equates. for example:

refl          : Eq (Bool,Bool) (True,False) (True,False)
(refl , refl) : Eq (Bool,Bool) (True,False) (True,False)

both would work. is that right?

if so, in that spirit, I suspect the proof of FunExt would go more or less like this:

funext
: ∀A: Set
  ∀B: A → Set
  ∀f: ∀(x:A). (B x)
  ∀g: ∀(x:A). (B x)
  ∀h: ∀(x:A). Eq (B x) (F x) (G x)
  Eq (∀(x:A).(B x)) f g
= λA. λB. λf. λg. λh.
  -- here, the goal is `Eq (∀(x:A).(B x)) f g`
  -- since this is an equality on a function type, we can introduce a lambda
  λx.
  -- here, the goal is `Eq (B x) (f x) (g x)`
  -- we can construct it by simply applying 'h' to 'x'
  (h x)
  -- this completes the proof

so basically all we need to implement FunExt is to let the compiler accept λx. as a way to introduce Eq (∀(x:A).(B x)) f g kind of

is this correct? am I on the right track?