[Agda] dependent extensionality

[James Chapman]

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