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