{-# OPTIONS --rewriting #-}
module FunctionExtensionality where
open import Equality
open import Level
open import Quotient
abstract
funext :
{ℓ ℓ' : Level}
{A : Set ℓ}
{B : A → Set ℓ'}
{f g : (x : A) → B x}
(_ : (x : A) → f x ≡ g x)
→
f ≡ g
funext {A = A} {B} {f} {g} h = cong m (by r) where
data s≡t : Set where
s : s≡t
t : s≡t
data R : s≡t → s≡t → Set where
r : R s t
k : (x : A) → s≡t → B x
k x s = f x
k x t = g x
l : (x : A)(b b' : s≡t) → R b b' → k x b ≡ k x b'
l x _ _ r = h x
m : s≡t / R → (x : A) → B x
m z x = qrec R (B x) (k x) (l x) z
implicit-eval :
{ℓ ℓ' : Level}
{A : Set ℓ}
{B : A → Set ℓ'}
→
((x : A) → B x) → {x : A} → B x
implicit-eval f {x} = f x
implicit-funext :
{ℓ ℓ' : Level}
{A : Set ℓ}
{B : A → Set ℓ'}
{f g : {x : A} → B x}
(_ : (x : A) → f {x} ≡ g {x})
→
(λ {x} → f {x}) ≡ g
implicit-funext {f = f} {g} e =
cong implicit-eval (funext {f = λ x → f{x}} {g = λ x → g{x}} e)