On Tue, Sep 28, 2010 at 9:52 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote: > I think dependent extensionality and non-dependent extensionality are equivalent anyway and I don't see how the levels should cause any harm. Equivalent in what sense? James