The function extensionality axiom asserts that identifications of functions are equivalent to homotopies between them.
These are equivalent definitions of function extensionality:
- The function extensionality principle holds at $f$, where $f, g : \Pi_{(x: A)}B(x)$, the family of maps: $$ \begin{align} \text{identity-to-htpy} &: (f = g) \to (f \sim g) \\ \text{identity-to-htpy}(refl_f) &:= \text{refl-htpy}_f \\ \end{align} $$ is a family of equivalence.
- The total space, $\Sigma_{(g: \Pi_{(x: A)}B(x))} f \sim g$ is contractible.
- The principle of homotopy induction: $$ s \mapsto s(f, \text{refl-htpy}_f) : (\Pi_{(g: \Pi_{(x: A)}B(x))} \Pi_{(H: f \sim g)} P(g, H)) \to P(f, \text{refl-htpy}_f) $$ has a section.
- The weak function extensionality principle: for each $A$, and $B(x)$ over $A$: $$ (\Pi_{(x:A)}\text{is-contr}(B(x))) \to \text{is-contr}(\Pi_{(x:A)}B(x)) $$
Universal properties
Universal properties are characterizations of all maps out of or into a given type.
Here are some examples:
The universal property of Σ-types
$$ \begin{align} \text{ev-pair} &:& (\Pi_{(z: \Sigma_{(x:A)}B(x))} C(z)) & \to & \Pi_{(x:A)}(\Pi_{(y:B(x))} &\to& C(x,y)) \\ \text{ev-pair} &:=& f &\mapsto& λx. λy &.& f((x, y)) \end{align} $$
and its inverse is obtained by the induction principle of Σ-types.
$$ \text{ind}_\Sigma : (\Pi_{(x : A)} \Pi_{(y : B(x))} C(x, y)) → \Pi_{(z : Σ_{(x : A)} B(x))} C (z) $$
It characterizes maps out of a dependent pair type $\Sigma_{(x: A)}B(x)$.
Proof of this principle needs function extensionality, to show $ind_Σ ∘ \text{ev-pair} \sim id$.
The universal property of identity types
$$ \begin{align} \text{ev-refl} &:& (\Pi_{(x:A)} (x = a) \to B(x)) & \to & B(a) \\ \text{ev-pair} &:=& f &\mapsto& f(a, refl_a) \end{align} $$
and its inverse is obtained by the induction principle of identity types.
$$ \text{ind}_{=_a} : B(a, refl_a) \to \Pi_{(x:A)} \Pi_{(p:x = a)} B(x, p) $$
Composing with equivalences
For any $f : A → B$, these are equivalent:
- $f$ is an equivalence.
- For any $P$ over $B$: $$ \begin{align} (&\Pi_{(y:B)} P&(y)) &\to& (&\Pi_{(x:A)} P&(&f&(x))) \\ &h& &\mapsto& &h& ∘ &f& \end{align} $$
- For any $X$: $$ \begin{align} (B → X) &\to& (A → X) \\ g &\mapsto& g ∘ f \end{align} $$