{-# 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)