[Agda] dependent extensionality

[Thorsten Altenkirch]

Well done. Hetreogenous equality does the trick.

But now John Major isn't PM anymore. Can you do it without K?

Cheers,
Thorsten

On 29 Sep 2010, at 13:08, James Chapman wrote:

> 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