Chuangjie Xu 2012

In this module, we postulate the axiom of function extensionality.

\begin{code}

module UsingFunext.Funext where

open import Preliminaries.SetsAndFunctions

postulate
  funext : Funext

funext² : {X : Set}
          {Y : X → Set}
          {Z : (x : X) → (y : Y x) → Set} →
          {f g : (x : X) → (y : Y x) → Z x y}
        → (∀ x y → f x y ≡ g x y) → f ≡ g
funext² ex = funext (λ x → funext (ex x))

funext³ : {X : Set}
          {Y : X → Set}
          {Z : (x : X) → Y x → Set}
          {W : (x : X) → (y : Y x) → Z x y → Set}
          {f g : (x : X) → (y : Y x) → (z : Z x y) → W x y z}
        → (∀ x y z → f x y z ≡ g x y z) → f ≡ g
funext³ ex = funext (λ x → funext (λ y → funext (ex x y)))

funext⁴ : {X : Set}
          {Y : X → Set}
          {Z : (x : X) → Y x → Set}
          {W : (x : X) → (y : Y x) → Z x y → Set}
          {U : (x : X) → (y : Y x) → (z : Z x y) → (w : W x y z) → Set}
          {f g : (x : X) → (y : Y x) → (z : Z x y) → (w : W x y z) → U x y z w}
        → (∀ x y z w → f x y z w ≡ g x y z w) → f ≡ g
funext⁴ ex = funext (λ x → funext (λ y → funext (λ z → funext (ex x y z))))

funext⁵ : {X : Set}
          {Y : X → Set}
          {Z : (x : X) → Y x → Set}
          {W : (x : X) → (y : Y x) → Z x y → Set}
          {U : (x : X) → (y : Y x) → (z : Z x y) → W x y z → Set}
          {V : (x : X) → (y : Y x) → (z : Z x y) → (w : W x y z) → U x y z w → Set}
          {f g : (x : X) → (y : Y x) → (z : Z x y) → (w : W x y z) → (u : U x y z w) → V x y z w u}
        → (∀ x y z w u → f x y z w u ≡ g x y z w u) → f ≡ g
funext⁵ ex = funext (λ x → funext (λ y → funext (λ z → funext (λ w → funext (ex x y z w)))))

\end{code}