Chuangjie Xu and Martin Escardo 2013.

We postulate the double negation of function extensionality. With
this, we don't lose canonicity.

Actually, something weaker than the double negation is sufficient,
called funext¹, but we postulate the double negation, because we know
that double negation of consistent axioms don't break canonicity.
http://www.cs.bham.ac.uk/~mhe/papers/negative-axioms.pdf

\begin{code}

module not-not-funext where

open import MiniLibrary
open import not-not
open import Sequence
open import Inequality

Funext : Set₁
Funext = {X : Set}{Y : X → Set}{f g : (x : X) → Y x} →
         (∀(x : X) → f x ≡ g x) → f ≡ g

postulate [funext] : [ Funext ]


funext¹ : {X : Set}{Y : X → Set}{f g : (x : X) → Y x} →
         (∀(x : X) → f x ≡ g x) → [ f ≡ g ]
funext¹ e u = [funext] (λ f → u (f e))

funext² : {X : Set}{Y : X → Set}{Z : (x : X) → (y : Y x) → Set} →
          {f g : (x : X) → (y : Y x) → Z x y} →
          (∀(x : X)(y : Y x) → f x y ≡ g x y) → [ f ≡ g ]
funext² {X} {Y} {Z} {f} {g} exy = goal
 where
  F G : (w : Σ \(x : X) → Y x) → Z (π₀ w) (π₁ w)
  F (x , y) = f x y
  G (x , y) = g x y
  Exy : (w : Σ \(x : X) → Y x) → F w ≡ G w
  Exy (x , y) = exy x y
  E : [ F ≡ G ]
  E = funext¹ Exy
  goal : [ f ≡ g ]
  goal = functor (ap (λ φ x y → φ(x , y))) E


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 : X)(y : Y x)(z : Z x y) → f x y z ≡ g x y z) → [ f ≡ g ]
funext³ {X} {Y} {Z} {W} {f} {g} exyz = goal
 where
  F G : (w : Σ \(x : X) → Σ \(y : Y x) → Z x y) → W (π₀ w) (π₀(π₁ w)) (π₁(π₁ w))
  F (x , y , z) = f x y z
  G (x , y , z) = g x y z
  Exyz : (w : Σ \(x : X) → Σ \(y : Y x) → Z x y) → F w ≡ G w
  Exyz (x , y , z) = exyz x y z
  E : [ F ≡ G ]
  E = funext¹ Exyz
  goal : [ f ≡ g ]
  goal = functor (ap (λ φ x y z → φ(x , y , z))) E


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 : X)(y : Y x)(z : Z x y)(w : W x y z) → f x y z w ≡ g x y z w) → [ f ≡ g ]
funext⁴ {X} {Y} {Z} {W} {U} {f} {g} ex = goal
 where
  Ω : Set
  Ω = Σ \(x : X) → Σ \(y : Y x) → Σ \(z : Z x y) → W x y z
  F G : (ω : Ω) → U (π₀ ω) (π₀(π₁ ω)) (π₀(π₁(π₁ ω))) (π₁(π₁(π₁ ω)))
  F (x , y , z , w) = f x y z w
  G (x , y , z , w) = g x y z w
  Ex : (ω : Ω) → F ω ≡ G ω
  Ex (x , y , z , w) = ex x y z w
  E : [ F ≡ G ]
  E = funext¹ Ex
  goal : [ f ≡ g ]
  goal = functor (ap (λ φ x y z w → φ(x , y , z , w))) E


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 : X)(y : Y x)(z : Z x y)(w : W x y z)(u : U x y z w) → f x y z w u ≡ g x y z w u) → [ f ≡ g ]
funext⁵ {X} {Y} {Z} {W} {U} {V} {f} {g} ex = goal
 where
  Ω : Set
  Ω = Σ \(x : X) → Σ \(y : Y x) → Σ \(z : Z x y) → Σ \(w : W x y z) → U x y z w
  F G : (ω : Ω) → V (π₀ ω) (π₀(π₁ ω)) (π₀(π₁(π₁ ω))) (π₀(π₁(π₁(π₁ ω)))) (π₁(π₁(π₁(π₁ ω))))
  F (x , y , z , w , u) = f x y z w u
  G (x , y , z , w , u) = g x y z w u
  Ex : (ω : Ω) → F ω ≡ G ω
  Ex (x , y , z , w , u) = ex x y z w u
  E : [ F ≡ G ]
  E = funext¹ Ex
  goal : [ f ≡ g ]
  goal = functor (ap (λ φ x y z w u → φ(x , y , z , w , u))) E



Lemma[[]-[hprop]] : {X : Set} → (xh yh : [ X ]) → [ xh ≡ yh ]
Lemma[[]-[hprop]] {X} xh yh = funext¹ eu
 where
  eu : (u : ¬ X) → xh u ≡ yh u
  eu u = ∅-elim (xh u)

\end{code}