{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.Cubical.Issues.FunctionExtensionality where

函數外延性#

open import Padova2025-zh-TW.ProgrammingBasics.Booleans
open import Padova2025-zh-TW.ProgrammingBasics.Naturals.Base
open import Padova2025-zh-TW.ProvingBasics.Equality.Base
open import Padova2025-zh-TW.ProvingBasics.Equality.General

讓我們考慮下面三個函數定義。

example₁ : Bool → Bool
example₁ x = x

example₂ : Bool → Bool
example₂ false = false
example₂ true  = true

example₃ : Bool → Bool
example₃ false = false
example₃ true  = true
-- 對，和 example₂ 的定義一模一樣。

顯然，這些函數在所有輸入上都有相同的值：

all-same₁₂ : (x : Bool) → example₁ x ≡ example₂ x
all-same₁₂ false = refl
all-same₁₂ true  = refl

all-same₂₃ : (x : Bool) → example₂ x ≡ example₃ x
all-same₂₃ false = refl
all-same₂₃ true  = refl

無法證明相同。 然而，在標準 Agda 中我們無法證明這些函數本身是相同的——下面的 hole 無法被填上（而提議使用的 refl 也無法通過型別檢查）：

_ : example₁ ≡ example₂
_ = ?

_ : example₂ ≡ example₃
_ = ?

無法證明相異。 另一方面，在 Agda 中我們也無法證明上面這三個函數彼此相異，也就是說，我們無法寫出型別 exampleᵢ ≡ exampleⱼ → ⊥ 的 term。 Agda 和任何其他合理的形式系統一樣，是不完備的。 這個不完備性的特定實例讓某些人特別擔憂，因為它關係到 Agda 如此基本的一部分。相等型別是欠規定的（underspecified）。

一個原理。 「值相等的函數本身也相等」這個原理稱為函數外延性（function extensionality）。黑板數學有它，標準 Agda 則沒有。

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

公設化函數外延性#

如果我們願意，可以公設化函數外延性：

postulate
  funext : FunctionExtensionality

把函數外延性加到 Martin-Löf 型別論中，不會破壞它的一致性。此外，如果一個人接受通常那種柏拉圖天堂的想法，就可以放心， 所得到的型別論仍然是談論柏拉圖天堂中對象的合適語言。

然而，公設化函數外延性會讓我們失去典範性（canonicity）：有了這個公設，歸納定義型別的元素可能不會化約成建構子的呼叫。 一個基本的例子就是 funext 本身。

does-not-reduce-to-refl : example₁ ≡ example₂
does-not-reduce-to-refl = funext all-same₁₂

does-not-reduce-to-a-numeral : ℕ
does-not-reduce-to-a-numeral = check does-not-reduce-to-refl
  where
  check : {g : Bool → Bool} → example₁ ≡ g → ℕ
  check refl = zero

避免函數外延性#

在許多用途上，只要改用逐點相等取代真正的 _≡_， 就能輕易避免函數外延性，如下所示。

all-same₁₂' : example₁ ≗ example₂
all-same₁₂' = all-same₁₂

但實際擁有函數外延性也是令人嚮往的。Cubical Agda 提供了這樣的系統。

習題：逐點相等是等價關係#

≗-refl : {X Y : Set} {f : X → Y} → f ≗ f
≗-refl = {!!}

≗-refl : {X Y : Set} {f : X → Y} → f ≗ f
≗-refl x = refl

≗-sym : {X Y : Set} {f g : X → Y} → f ≗ g → g ≗ f
≗-sym = {!!}

≗-sym : {X Y : Set} {f g : X → Y} → f ≗ g → g ≗ f
≗-sym p x = sym (p x)

≗-trans : {X Y : Set} {f g h : X → Y} → f ≗ g → g ≗ h → f ≗ h
≗-trans = {!!}

≗-trans : {X Y : Set} {f g h : X → Y} → f ≗ g → g ≗ h → f ≗ h
≗-trans p q x = trans (p x) (q x)

習題：型別構成範疇#

設 f、g 與 h 是可合成的函數。那麼我們確實有 (h ∘ g) ∘ f ≗ h ∘ (g ∘ f)。 同樣的恆等式用 _≡_ 取代 _≗_ 後也成立嗎？還是需要函數外延性？

open import Padova2025-zh-TW.ProgrammingBasics.HigherOrder
open import Padova2025-zh-TW.ProgrammingBasics.DependentFunctions

∘-assoc : {X Y Z W : Set} → (f : X → Y) (g : Y → Z) (h : Z → W) → (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)
∘-assoc = {!!}

∘-assoc : {X Y Z W : Set} → (f : X → Y) (g : Y → Z) (h : Z → W) → (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)
∘-assoc f g h = refl

∘-identityˡ : {X Y : Set} → (f : X → Y) → id Y ∘ f ≡ f
∘-identityˡ = {!!}

∘-identityˡ : {X Y : Set} → (f : X → Y) → id Y ∘ f ≡ f
∘-identityˡ f = refl

∘-identityʳ : {X Y : Set} → (f : X → Y) → f ∘ id X ≡ f
∘-identityʳ = {!!}

∘-identityʳ : {X Y : Set} → (f : X → Y) → f ∘ id X ≡ f
∘-identityʳ f = refl

record 𝟙 : Set where
  constructor tt

_ : (x y : 𝟙) → x ≡ y
_ = λ x y → refl

_ : {X : Set} → {f g : X → 𝟙} → f ≡ g
_ = refl

data 𝟙' : Set where
  tt : 𝟙'

𝟙'-isProp : (x y : 𝟙') → x ≡ y
𝟙'-isProp tt tt = refl
-- 但如果沒有做 pattern matching，寫成 𝟙'-isProp x y = refl，就會出現型別錯誤。