{-# OPTIONS --rewriting #-}

module FunExt where

open import Equality
open import Function
open import FunctionExtensionality
open import Interval
open import Level
open import Path

----------------------------------------------------------------------
-- Function extensionality, modulo ~
----------------------------------------------------------------------
~funext :
  {  ℓ' : Level}
  {A : Set }
  {B : A  Set ℓ'}
  {f g : (x : A)  B x}
  (p : (x : A)  f x ~ g x)
   -----------------------
  f ~ g
~funext p =  i  x  p x at i)

{--
Given f g : (x : A) → B x, the canonical function from f ~ g to 
(x : A) → f x ~ g x) is actually an (extensional) isomorphism:
--} 
~apply :
  {  ℓ' : Level}
  {A : Set }
  {B : A  Set ℓ'}
  {f g : (x : A)  B x}
  (p : f ~ g) 
   -------------------
  (x : A)  f x ~ g x
~apply (path h) x =  i (h i x)

~funext∘~apply :
  {  ℓ' : Level}
  {A : Set }
  {B : A  Set ℓ'}
  {f g : (x : A)  B x}
  (p : f ~ g) 
   --------------------
  ~funext (~apply p)  p
~funext∘~apply (path h) = refl

~apply∘~funext :
  {  ℓ' : Level}
  {A : Set }
  {B : A  Set ℓ'}
  {f g : (x : A)  B x}
  (p : (x : A)  f x ~ g x)
   -----------------------
  ~apply (~funext p)  p
~apply∘~funext p = funext  _  atInj refl)