{-# OPTIONS --rewriting #-}
module FunExt where
open import Equality
open import Function
open import FunctionExtensionality
open import Interval
open import Level
open import Path
~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)
~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)