[Agda] Unification of function types

[Nils Anders Danielsson]

On 2013-09-19 16:18, Jesper Cockx wrote:
> I guess the problem with the first definition is that Agda doesn't
> know how to unify the two types (x : A₁) → B₁ x and (x : A₁) → B₂ x.
> Would it be problematic add such a rule to the unification algorithm?

You may be interested in the following mailing list threads:

   heterogeneous equality
   https://lists.chalmers.se/pipermail/agda/2008/000153.html

   Agda with the excluded middle is inconsistent ?
   http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322

-- 
/NAD