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