Martin Escardo. Formulation of function extensionality. Notice that this file doesn't postulate function extensionality. It only defines the concept, which is used explicitly as a hypothesis each time it is needed. \begin{code} {-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-} module UF.FunExt where open import MLTT.Spartan open import UF.Base open import UF.Equiv open import UF.LeftCancellable \end{code} The appropriate notion of function extensionality in univalent mathematics is funext, define below. It is implied, by an argument due to Voevodky, by naive, non-dependent function extensionality, written naive-funext here. \begin{code} naive-funext : โ ๐ค ๐ฅ โ ๐ค โบ โ ๐ฅ โบ ฬ naive-funext ๐ค ๐ฅ = {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {f g : X โ Y} โ f โผ g โ f ๏ผ g DN-funext : โ ๐ค ๐ฅ โ ๐ค โบ โ ๐ฅ โบ ฬ DN-funext ๐ค ๐ฅ = {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } {f g : ฮ A} โ f โผ g โ f ๏ผ g funext : โ ๐ค ๐ฅ โ ๐ค โบ โ ๐ฅ โบ ฬ funext ๐ค ๐ฅ = {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (f g : ฮ A) โ is-equiv (happly' f g) FunExt : ๐คฯ FunExt = (๐ค ๐ฅ : Universe) โ funext ๐ค ๐ฅ Fun-Ext : ๐คฯ Fun-Ext = {๐ค ๐ฅ : Universe} โ funext ๐ค ๐ฅ โ-funext : funext ๐ค ๐ฅ โ {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (f g : ฮ A) โ (f ๏ผ g) โ (f โผ g) โ-funext fe f g = happly' f g , fe f g abstract dfunext : funext ๐ค ๐ฅ โ DN-funext ๐ค ๐ฅ dfunext fe {X} {A} {f} {g} = inverse (happly' f g) (fe f g) happly-funext : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (fe : funext ๐ค ๐ฅ) (f g : ฮ A) (h : f โผ g) โ happly (dfunext fe h) ๏ผ h happly-funext fe f g = inverses-are-sections happly (fe f g) funext-happly : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (fe : funext ๐ค ๐ฅ) โ (f g : ฮ A) (h : f ๏ผ g) โ dfunext fe (happly h) ๏ผ h funext-happly fe f g refl = inverses-are-retractions happly (fe f f) refl happly-โ : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (fe : funext ๐ค ๐ฅ) {f g : (x : X) โ A x} โ (f ๏ผ g) โ f โผ g happly-โ fe = happly , fe _ _ funext-lc : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (fe : funext ๐ค ๐ฅ) (f g : ฮ A) โ left-cancellable (dfunext fe {X} {A} {f} {g}) funext-lc fe f g = section-lc (dfunext fe) (happly , happly-funext fe f g) happly-lc : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (fe : funext ๐ค ๐ฅ) (f g : ฮ A) โ left-cancellable (happly' f g) happly-lc fe f g = section-lc happly (equivs-are-sections happly (fe f g)) inverse-happly-is-dfunext : {๐ค ๐ฅ : Universe} {A : ๐ค ฬ } {B : ๐ฅ ฬ } (fe0 : funext ๐ค ๐ฅ) (fe1 : funext (๐ค โ ๐ฅ) (๐ค โ ๐ฅ)) (f g : A โ B) โ inverse (happly' f g) (fe0 f g) ๏ผ dfunext fe0 inverse-happly-is-dfunext fe0 fe1 f g = dfunext fe1 ฮป h โ happly-lc fe0 f g (happly' f g (inverse (happly' f g) (fe0 f g) h) ๏ผโจ inverses-are-sections _ (fe0 f g) h โฉ h ๏ผโจ happly-funext fe0 f g h โปยน โฉ happly' f g (dfunext fe0 h) โ) dfunext-refl : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ } (fe : funext ๐ค ๐ฅ) (f : ฮ A) โ dfunext fe (ฮป (x : X) โ ๐ป๐ฎ๐ป๐ต (f x)) ๏ผ refl dfunext-refl fe f = happly-lc fe f f (happly-funext fe f f (ฮป x โ refl)) ap-funext : {X : ๐ฅ ฬ } {Y : ๐ฆ ฬ } (f g : X โ Y) {A : ๐ฆ' ฬ } (k : Y โ A) (h : f โผ g) (fe : funext ๐ฅ ๐ฆ) (x : X) โ ap (ฮป (- : X โ Y) โ k (- x)) (dfunext fe h) ๏ผ ap k (h x) ap-funext f g k h fe x = ap (ฮป - โ k (- x)) (dfunext fe h) ๏ผโจ refl โฉ ap (k โ (ฮป - โ - x)) (dfunext fe h) ๏ผโจ I โฉ ap k (ap (ฮป - โ - x) (dfunext fe h)) ๏ผโจ refl โฉ ap k (happly (dfunext fe h) x) ๏ผโจ II โฉ ap k (h x) โ where I = (ap-ap (ฮป - โ - x) k (dfunext fe h))โปยน II = ap (ฮป - โ ap k (- x)) (happly-funext fe f g h) ap-precomp-funext : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {A : ๐ฆ ฬ } (f g : X โ Y) (k : A โ X) (h : f โผ g) (feโ : funext ๐ค ๐ฅ) (feโ : funext ๐ฆ ๐ฅ) โ ap (_โ k) (dfunext feโ h) ๏ผ dfunext feโ (h โ k) ap-precomp-funext f g k h feโ feโ = ap (_โ k) (dfunext feโ h) ๏ผโจ I โฉ dfunext feโ (happly (ap (_โ k) (dfunext feโ h))) ๏ผโจ II โฉ dfunext feโ (h โ k) โ where I = funext-happly feโ (f โ k) (g โ k) _ โปยน III = ฮป x โ ap (ฮป - โ - x) (ap (_โ k) (dfunext feโ h)) ๏ผโจ ap-ap _ _ (dfunext feโ h) โฉ ap (ฮป - โ - (k x)) (dfunext feโ h) ๏ผโจ ap-funext f g id h feโ (k x) โฉ ap (ฮป v โ v) (h (k x)) ๏ผโจ ap-id-is-id (h (k x)) โฉ h (k x) โ II = ap (dfunext feโ) (dfunext feโ III) \end{code} The following is taken from this thread: https://groups.google.com/forum/#!msg/homotopytypetheory/VaLJM7S4d18/Lezr_ZhJl6UJ \begin{code} transport-funext : {X : ๐ค ฬ } (A : X โ ๐ฅ ฬ ) (P : (x : X) โ A x โ ๐ฆ ฬ ) (fe : funext ๐ค ๐ฅ) (f g : ฮ A) (ฯ : (x : X) โ P x (f x)) (h : f โผ g) (x : X) โ transport (ฮป - โ (x : X) โ P x (- x)) (dfunext fe h) ฯ x ๏ผ transport (P x) (h x) (ฯ x) transport-funext A P fe f g ฯ h x = q โ r where l : (f g : ฮ A) (ฯ : โ x โ P x (f x)) (p : f ๏ผ g) โ โ x โ transport (ฮป - โ โ x โ P x (- x)) p ฯ x ๏ผ transport (P x) (happly p x) (ฯ x) l f .f ฯ refl x = refl q : transport (ฮป - โ โ x โ P x (- x)) (dfunext fe h) ฯ x ๏ผ transport (P x) (happly (dfunext fe h) x) (ฯ x) q = l f g ฯ (dfunext fe h) x r : transport (P x) (happly (dfunext fe h) x) (ฯ x) ๏ผ transport (P x) (h x) (ฯ x) r = ap (ฮป - โ transport (P x) (- x) (ฯ x)) (happly-funext fe f g h) transport-funext' : {X : ๐ค ฬ } (A : ๐ฅ ฬ ) (P : X โ A โ ๐ฆ ฬ ) (fe : funext ๐ค ๐ฅ) (f g : X โ A) (ฯ : (x : X) โ P x (f x)) (h : f โผ g) (x : X) โ transport (ฮป - โ (x : X) โ P x (- x)) (dfunext fe h) ฯ x ๏ผ transport (P x) (h x) (ฯ x) transport-funext' A P = transport-funext (ฮป _ โ A) P \end{code}