[Agda] dependent extensionality

[James Chapman]

On Wed, Sep 29, 2010 at 6:00 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk> 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.

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

I think so. See below:

{-# OPTIONS --type-in-type #-}

module ext where

data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
  refl : a ≡ a

resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≡ a' → f a ≡ f a'
resp f refl = refl

record Σ (A : Set)(B : A -> Set) : Set where
  constructor _,_
  field fst : A
	snd : B fst
open Σ

_* : {A : Set}{B : A → Set}(f : (a : A) → B a) → A → (Σ A λ a → B a)
f *  = λ x → x , f x

lem : ∀{A : Set}{B : A → Set}{f g : A → Σ A B} → f ≡ g →
     _≡_ {(x : A) → B (fst (f x))} (λ x → snd (f x))
         {(x : A) → B (fst (g x))} (λ x → snd (g x))
lem refl = refl

simext : Set
simext  = (A B : Set)(f g : A → B) → (∀ x → f x ≡ g x) → f ≡ g

depext : Set
depext = (A : Set)(B : A → Set)(f g : (x : A) → B x) → (∀ x → f x ≡ g x) → f ≡ g

right : depext → simext
right p A B = p A (λ _ → B)

left : simext → depext
left p A B f g q  = lem (p A (Σ A λ a → B a) (f *) (g *) (λ x → resp
(_,_ x) (q x)))

Regards,

James