[Agda] Unification of function types

Nils Anders Danielsson nad at cse.gu.se
Thu Sep 19 16:43:28 CEST 2013

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

   Agda with the excluded middle is inconsistent ?


More information about the Agda mailing list