```{-# OPTIONS --rewriting #-}

module FunctionExtensionality where

open import Equality
open import Level
open import Quotient

----------------------------------------------------------------------
-- Function extensionalty via quotients
----------------------------------------------------------------------
{- abstract block used to speed up type-checking uses of funext -}
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

----------------------------------------------------------------------
-- Function extensionality with implicit arguments
----------------------------------------------------------------------
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)
```