📥 Download raw
module Padova2025.Cubical.Issues.FunctionExtensionality where

Function extensionality

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General

Let us consider the following three function definitions.

example₁ : Bool → Bool
example₁ x = x

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

example₃ : Bool → Bool
example₃ false = false
example₃ true  = true
-- Yes, identical to the definition of example₂.

Obviously, these functions have the same values on all inputs:

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

Not provably the same. However, in standard Agda we can not prove that the functions themselves are the same—the following holes cannot be filled (and the proposal refl does not typecheck):

_ : example₁ ≡ example₂
_ = ?

_ : example₂ ≡ example₃
_ = ?

Not provably distinct. On the other hand, in Agda we can also not prove the three functions above to be distinct, that is we cannot write down terms of type exampleᵢ ≡ exampleⱼ → ⊥. Agda is (like any other reasonable formal system) incomplete. This particular instance of incompleteness is particularly worrying to some, as it pertains to such a basic part of Agda. The equality type is underspecified.

A principle. The principle that functions with equal values are themselves equal is known as function extensionality. Blackboard mathematics has it, while standard Agda does not.

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

Postulating function extensionality

We may, if we prefer, postulate function extensionality:

postulate
  funext : FunctionExtensionality

Adding function extensionality to Martin-Löf type theory preserves its consistency. Moreover, if one entertains the idea of a platonic heaven, then one can rest assured that the resulting type theory still provides an apt language for talking about the objects of the platonic heaven.

However, by postulating function extensionality we lose canonicity: With this postulate, it can happen that elements of inductively defined types do not reduce to a constructor call. A basic example is already provided by funext itself.

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

Avoiding function extensionality

For many purposes, function extensionality can easily be avoided by employing pointwise equality instead of true _≡_, as follows.

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

But it is also desireable to actually have function extensionality. Such a system is offered by Cubical Agda.

Exercise: Pointwise equality is an equivalence relation

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

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

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

Exercise: Types form a category

Let f, g and h be composable functions. Then we definitely have (h ∘ g) ∘ f ≗ h ∘ (g ∘ f). Does the same identity also hold with _≡_ in place of _≗_, or is function extensionality needed for that?

open import Padova2025.ProgrammingBasics.HigherOrder
open import Padova2025.ProgrammingBasics.DependentFunctions

Even though standard Agda does not have function extensionality, it does have eta equality: Every function f is judgmentally equal to the lambda λ x → f x. This principle is enough to verify that the (small) types form a category, up to true propositional equality and not only up to pointwise equality.

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

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

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

Having established that types form a category, a category theorist might enquire about its categorical properties. For instance, in blackboard mathematics, the category Set has an initial object, namely the empty set ∅: For every set X, there is exactly one map ∅ → X.

Does the category of types have an initial object? How about a terminal object?

No initial object

Agda does have the empty type ⊥, and for every type X there is a map ⊥-elim : ⊥ → X. Hence the category of types has a weakly initial object. However, without function extensionality, we cannot show that any two functions of type ⊥ → X are identical.

Terminal object

On the other hand, there is a terminal object. This is provided by the following declaration.

record 𝟙 : Set where
  constructor tt

Record types by default have (their own version of) eta equality. That is the reason why any two inhabitants are judgmentally equal:

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

As a corollary, any two functions to 𝟙 are judgmentally equal:

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

In constract, declaring 𝟙 as an ordinary inductive datatype (or disabling eta equality with the no-eta-equality keyword in the record declaraction) will provide us with a type in which any two inhabitants are propositionally but not judgmentally equal.

data 𝟙' : Set where
  tt : 𝟙'

𝟙'-isProp : (x y : 𝟙') → x ≡ y
𝟙'-isProp tt tt = refl
-- But without the pattern match, 𝟙'-isProp x y = refl, there is a type error.

Category of setoids

Even though the category of types is perhaps the first to reach out to when exploring the landscape of categories in Agda, the category of (small) setoids is for many applications actually much more sensible, less dependent on foundations (such as the availability or non-availability of function extensionality) and also much better behaved. For instance, the category of setoids is complete and cocomplete, locally cartesian closed, exact and extensive. It also validates a version of the axiom of choice. All of these assertions can be explored in great detail in the categories library in the module Categories.Category.Instance.Properties.Setoids and its submodules.