ch:univalent-set-mathematics: cardinals and ordinals

On representatives, the inverse of $(A + B) + C \to A + (B + C)$ sends $inl (inl a)$ to $inl a$ , $inl (inr b)$ to $inr (inl b)$ , and $inr c$ to $inr (inr c)$ ; the inverse of the commutation map exchanges the two summands, and the inverse of $0 + A \to A$ is $a \mapsto inr a$ . The product maps use the same reassociation and exchange of coordinates, with $a \mapsto (⋆, a)$ for the unit. The two distributivity inverses send $inl (a, b)$ and $inr (a, c)$ to $(a, inl b)$ and $(a, inr c)$ , and similarly on the other side. Case analysis for sums and componentwise calculation for products verify both composites.

For exponentials, the inverse of $(B + C \to A) \to (B \to A) \times (C \to A)$ is copairing, the inverse of $C \to (A \times B) \to (C \to A) \times (C \to B)$ pairs the two values, and the inverse of currying is evaluation on pairs. The empty- and unit-domain inverses are the unique empty function and evaluation at $⋆$ . Function extensionality verifies both composites. Truncation induction and univalence turn these equivalences into the cardinal equalities.

If $f : A ↪ A^{'}$ and $g : B ↪ B^{'}$ , the maps $f + g : A + B ↪ A^{'} + B^{'}$ and $f \times g : A \times B ↪ A^{'} \times B^{'}$ are injective by case analysis and componentwise injectivity. If $f : A ↪ A^{'}$ , then postcomposition $(C \to A) ⟶ (C \to A^{'}), h ⟼ f \circ h$ is injective by function extensionality and injectivity of $f$ . Eliminating the representative injections into the propositional target proves compatibility with $+$ and $\cdot$ and base monotonicity $| A |^{| C |} \leq | A^{'} |^{| C |}$ .

Fix $u : acc (a)$ and induct on $u$ with motive $P (a, u) : = \prod_{v : acc (a)} u = v .$ In the constructor case write $u = {acc}_{<} (a, h_{1})$ and $v = {acc}_{<} (a, h_{2})$ . For every $b : A$ and $r : b < a$ , the induction hypothesis applied to $h_{1} (b, r)$ and $h_{2} (b, r)$ gives $h_{1} (b, r) = h_{2} (b, r)$ . Function extensionality in $r$ and then $b$ gives $h_{1} = h_{2}$ , so congruence of the accessibility constructor gives $u = v$ . Thus $acc (a)$ is a mere proposition. A dependent product of mere propositions is a mere proposition, so $\prod_{a : A} acc (a)$ is one as well.

For a simulation $f : A \to B$ , use well-founded induction on $a$ with the strengthened motive $P (a) : = \prod_{a^{'} : A} (f (a) = f (a^{'})) \to (a = a^{'}) .$ Given $f (a) = f (a^{'})$ and $c < a$ , simulation at $a^{'}$ gives, under a propositional truncation, $c^{'} < a^{'}$ with $f (c^{'}) = f (c)$ . Eliminate the truncation into the proposition $c = c^{'}$ and apply $P (c)$ . Conversely, a predecessor $c^{'} < a^{'}$ has an image predecessor $c < a$ , and $P (c)$ again gives $c = c^{'}$ . Extensionality of $A$ now gives $a = a^{'}$ , proving injectivity.

For simulations $f, g : A \to B$ , induct on $a$ . If $b < f (a)$ , simulation for $f$ gives $a^{'} < a$ with $f (a^{'}) = b$ ; the induction hypothesis changes this to $g (a^{'}) = b$ , hence $b < g (a)$ . The converse uses $g$ in the same way. Extensionality of $B$ gives $f (a) = g (a)$ , and function extensionality gives $f = g$ . If $f : A \to B$ and $g : B \to A$ are simulations, uniqueness applied to $g \circ f$ and ${id}_{A}$ , and then to $f \circ g$ and ${id}_{B}$ , proves that they are inverse relation isomorphisms.

Suppose $a : A$ and $p : e (a) = d$ . Function congruence at $a$ gives $e (a) (a) = d (a) = not (e (a) (a)) .$ Boolean elimination on $e (a) (a)$ reduces this equality either to $false = true$ or to $true = false$ ; Boolean separation refutes both cases. Thus the fiber of $e$ over $d$ is empty. If $e$ were surjective, its surjectivity witness at $d$ would give such an $a$ and equality. The empty target is a proposition, so the truncation may be eliminated into the contradiction. The construction uses function congruence and Boolean separation, but it never decides an arbitrary proposition and therefore does not use excluded middle.