[Agda] dependent extensionality

[Thorsten Altenkirch]

On 28 Sep 2010, at 20:48, James Chapman wrote:

> 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?

In the sense that they are maybe not. :-)

I thought that ext -> dext, where

dext : {A : Set}{B : A → Set}(f g : (a : A) → B a)
      → ((a : A) → f a ≡ g a)
      → f ≡ g

The idea is to define f' g' : A → Σ A B as f' a = a , f a etc and then use ext to prove that f' ≡ g'.

Clearly f = (λ a → proj₂ (f' a)) and similar for g. Now if we can substitute f' for g' we are done.

But can we?

Cheers,
Thorsten