Martin Escardo, 19th May 2018.

Properties of function extensionality.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.FunExt-Properties where

open import MLTT.Spartan
open import UF.Base
open import UF.FunExt
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.Yoneda
open import UF.Singleton-Properties
open import UF.Subsingletons
open import UF.Retracts

\end{code}

Vladimir Voevodsky proved in Coq that naive function extensionality
(any two pointwise equal non-dependent functions are equal) implies
function extensionality (happly is an equivalence, for dependent
functions):

  https://github.com/vladimirias/Foundations/blob/master/Generalities/uu0.v

Here is an Agda version, with explicit indication of the universe levels.

\begin{code}

naive-funext-gives-funext' : naive-funext 𝓀 (𝓀 βŠ” π“₯) β†’ naive-funext 𝓀 𝓀 β†’ funext 𝓀 π“₯
naive-funext-gives-funext' {𝓀} {π“₯} nfe nfe' = funext-via-singletons Ξ³
 where
  Ξ³ : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ )
    β†’ ((x : X) β†’ is-singleton (A x))
    β†’ is-singleton (Ξ  A)
  Ξ³ X A Ο† = Ξ΄
   where
    f : Ξ£ A β†’ X
    f = pr₁

    f-is-equiv : is-equiv f
    f-is-equiv = pr₁-is-equiv X A Ο†

    g : (X β†’ Ξ£ A) β†’ (X β†’ X)
    g h = f ∘ h

    g-is-equiv : is-equiv g
    g-is-equiv = equiv-post nfe nfe' f f-is-equiv

    e : βˆƒ! h κž‰ (X β†’ Ξ£ A) , f ∘ h ＝ id
    e = equivs-are-vv-equivs g g-is-equiv id

    r : (Ξ£ h κž‰ (X β†’ Ξ£ A) , f ∘ h ＝ id) β†’ Ξ  A
    r (h , p) x = transport A (happly p x) (prβ‚‚ (h x))

    s : Ξ  A β†’ (Ξ£ h κž‰ (X β†’ Ξ£ A) , f ∘ h ＝ id)
    s Ο† = (Ξ» x β†’ x , Ο† x) , refl

    rs : βˆ€ Ο† β†’ r (s Ο†) ＝ Ο†
    rs Ο† = refl

    Ξ΄ : is-singleton (Ξ  A)
    Ξ΄ = retract-of-singleton (r , s , rs) e

naive-funext-gives-funext : naive-funext 𝓀 𝓀 β†’ funext 𝓀 𝓀
naive-funext-gives-funext fe = naive-funext-gives-funext' fe fe

naive-funext-gives-funextβ‚€ : naive-funext 𝓀 𝓀 β†’ funext 𝓀 𝓀₀
naive-funext-gives-funextβ‚€ fe = naive-funext-gives-funext' fe fe

\end{code}

Added by Evan Cavallo on 13th March 2025.

The equivalence extensionality axiom is the restriction of function
extensionality to equivalences. By an argument similar to the proof of function
extensionality from univalence, it implies full function extensionality.

\begin{code}

equivext : βˆ€ 𝓀 π“₯ β†’ 𝓀 ⁺ βŠ” π“₯ ⁺ Μ‡
equivext 𝓀 π“₯ =
 {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (Ξ± Ξ² : X ≃ Y)
 β†’ is-equiv (Ξ» (p : Ξ± ＝ Ξ²) β†’ happly (ap ⌜_⌝ p))

equivext-gives-funext : equivext 𝓀 𝓀 β†’ funext 𝓀 𝓀
equivext-gives-funext {𝓀} ee =
 funext-via-singletons main
 where
  promote : (A : 𝓀 Μ‡ ) {X Y : 𝓀 Μ‡ } β†’ X ≃ Y β†’ (A ≃ X) ≃ (A ≃ Y)
  promote A Ξ± =
   qinveq
    (_● Ξ±)
    ( (_● ≃-sym Ξ±)
    , (Ξ» Ξ² β†’ inverse _ (ee _ _) (inverses-are-retractions _ (prβ‚‚ Ξ±) ∘ ⌜ Ξ² ⌝))
    , (Ξ» Ξ³ β†’ inverse _ (ee _ _) (inverses-are-sections _ (prβ‚‚ Ξ±) ∘ ⌜ Ξ³ ⌝)))

  module _ (X : 𝓀 Μ‡ ) (Y : X β†’ 𝓀 Μ‡ ) (cY : (x : X) β†’ is-singleton (Y x)) where
   Ο€ : (Ξ£ Y) ≃ X
   Ο€ =
    qinveq
     pr₁
     ( (Ξ» x β†’ x , pr₁ (cY x))
     , (Ξ» (x , y) β†’ to-Ξ£-＝ (refl , prβ‚‚ (cY x) y))
     , ∼-refl)

   sec : Ξ  Y β†’ fiber ⌜ promote X Ο€ ⌝ π•šπ••
   sec f =
    ( qinveq
       (Ξ» x β†’ x , f x)
       ( pr₁
       , ∼-refl
       , (Ξ» (x , y) β†’ to-Ξ£-＝ (refl , singletons-are-props (cY x) _ _)))
    , inverse _ (ee _ _) ∼-refl)

   ret : fiber ⌜ promote X Ο€ ⌝ π•šπ•• β†’ Ξ  Y
   ret (Ξ± , p) x = transport Y (happly (ap ⌜_⌝ p) x) (prβ‚‚ (pr₁ Ξ± x))

   inv : ret ∘ sec ∼ id
   inv f =
    ap (Ξ» h β†’ Ξ» x β†’ transport Y (h x) (prβ‚‚ (pr₁ Ξ± x))) cancel
     where
      Ξ± = pr₁ (sec f)
      p = prβ‚‚ (sec f)

      cancel : happly (ap ⌜_⌝ p) ＝ ∼-refl
      cancel = inverses-are-sections _ (ee _ _) (∼-refl)

   main : is-singleton (Ξ  Y)
   main = retract-of-singleton
           (ret , sec , inv)
           (equivs-are-vv-equivs _ (prβ‚‚ (promote X Ο€)) π•šπ••)

\end{code}

End of addition.