[Agda] Unification of function types

[Vilhelm Sjöberg]

On 2013-09-20 06:14, Jesper Cockx wrote:
> From a more theoretical perspective, it seems to me quite 
> unproblematic to add a rule that A1 = A2 and B1 = B2 whenever (x : A1) 
> -> B1 = (x : A2) -> B2.
What do you propose to do about the bound variable x in B1?

One idea is to say that for any (a:A1), we should be able to conclude
{a/x}B1 = {a/x}B2.
But now the injectivity rule is really an injectivity axiom scheme which 
can be instantiated for arbitrary a:s, and it seems hard to use such a 
rule in a terminating algorithm (as we would want for definitional 
equality). For example, any equation scheme
∀ x y z. (a = b)
could be expressed by an assumption
((x y z:A) -> a) = ((x y z:A) -> b)
and deciding equality in a theory with arbitrary axioms is undecidable.

I was just thinking about this problem in another context, so ideas or 
literature pointers would be welcome. :)

Vilhelm