[Agda] dependent extensionality

[James Chapman]

I accidentally chopped the theorem off the bottom. Here's (hopefully)
a more successful cut and paste...

James

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

module ext where

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

subst : {A : Set}(P : A → Set){a a' : A} → a ≡ a' → P a → P a'
subst P refl p = p

trans : {A : Set}{a a' a'' : A} → a ≡ a' → a' ≡ a'' → a ≡ a''
trans refl p = p

_•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
      (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
f • g = λ a → f (g a)

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}{a : A}{p q : B a} → p ≡ q → _≡_ {Σ A B}
(a , p) (a , q)
lem refl = refl

lem'' : {A : Set}{B : A → Set}{f g : A → Σ A B}(p : f ≡ g) → subst (λ
f → (a : A) → B (fst (f a))) p (snd • f) ≡ (snd • g)
lem'' refl = refl

substlem : {A : Set}(P : A → Set){a a' : A}(p : a ≡ a')(x : P a)(q : P
a ≡ P a') → subst (λ x → x) q x ≡ subst P p x
substlem P refl x refl = refl

lem' : {A : Set}{B : A → Set}{f g : (x : A) → B x} → f * ≡ g * → f ≡ g
lem' {A}{B}{f}{g} p = trans (substlem (λ f' → (a : A) → B (fst (f'
a))) p f refl) (lem'' p)

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 : A) → lem (q x))

2010/9/29 James Chapman <james at cs.ioc.ee>:
> Here's a homogeneous version:
>
> {-# OPTIONS --type-in-type #-}
>
> module ext where
>
> data _≡_ {A : Set}(a : A) : A → Set where
>  refl : a ≡ a
>
> subst : {A : Set}(P : A → Set){a a' : A} → a ≡ a' → P a → P a'
> subst P refl p = p
>
> trans : {A : Set}{a a' a'' : A} → a ≡ a' → a' ≡ a'' → a ≡ a''
> trans refl p = p
>
> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>      (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
> f • g = λ a → f (g a)
>
> 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}{a : A}{p q : B a} → p ≡ q → _≡_ {Σ A B}
> (a , p) (a , q)
> lem refl = refl
>
> lem'' : {A : Set}{B : A → Set}{f g : A → Σ A B}(p : f ≡ g) → subst (λ
> f → (a : A) → B (fst (f a))) p (snd • f) ≡ (snd • g)
> lem'' refl = refl
>
> substlem : {A : Set}(P : A → Set){a a' : A}(p : a ≡ a')(x : P a)(q : P
> a ≡ P a') → subst (λ x → x) q x ≡ subst P p x
> substlem P refl x refl = refl
>
> lem' : {A : Set}{B : A → Set}{f g : (x : A) → B x} → f * ≡ g * → f ≡ g
> lem' {A}{B}{f}{g} p = trans (substlem (λ f' → (a : A) → B (fst (f'
> a))) p f refl) (lem'' p)
>
> 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)
>
> Regards,
>
> James
>