ch:ott: ch:ott

The unique introduction of $\mathrm{\top }$ gives $\mathrm{\top }\to (\mathrm{\perp }\to \mathrm{\perp })$ by the identity function on an assumed contradiction, and any function $\mathrm{\perp }\to \mathrm{\perp }$ maps to the unique proof of $\mathrm{\top }$. For $f,g:\mathrm{\perp }\to \mathrm{\perp }$, function eta reduces equality to equality of $f(x)$ and $g(x)$ under $x:\mathrm{\perp }$; Irr identifies these proofs judgmentally. Thus $\mathrm{\perp }\to \mathrm{\perp }$ has the same introduction, elimination, and irrelevance rules as $\mathrm{\top }$.

Given $z:\mathrm{\exists }(x:P).Q(x)$ and a motive $C(z):\mathsf{SProp}$, with branch $d:{\mathrm{\Pi }}_{x:P}{\mathrm{\Pi }}_{y:Q(x)}C(⟨x,y⟩)$, define the eliminator by first using Ex-E1 to obtain a witness $x$ and then Ex-E2 to obtain the corresponding $y$. The produced proof has type $C(⟨x,y⟩)$; Irr converts it to $C(z)$ because all inhabitants of the existential proposition, and hence their motive fibers, are proof irrelevant. The constructor computation follows by both elimination computations and Irr.

A closed derivation of $\mathrm{\perp }$ already makes the theory inconsistent, so a metarule using only such a derivation to produce a closed inhabitant adds no new behavior in a consistent theory. By contrast, a variable $h:\mathbf{0}$ is a neutral relevant term; large elimination turns it into a neutral term of every data type. Declaring those proofs irrelevant can identify eliminations that compute through different relevant structures, so compatibility with reduction and confluence—hence decidable conversion and kernel rechecking—must be proved. The at-risk demand is normalization/ decidable judgmental equality, not merely logical consistency.

Reflexivity has motive $\lambda x.x{\approx }_{A}x$ in $\mathsf{SProp}$. Symmetry transports a proof along the swapped endpoint family, and transitivity transports along the second equality; all proof-dependent choices are repaired by Irr. For dependent $f$, take $e:A(t,u)$ to obtain the type equality ${\mathsf{ap}}_B(e):B(t)=B(u)$. Cast $ft$ along it, then use observational congruence of application and the transport rule for $f$ to produce $\mathsf{cast}(B(t),B(u),{\mathsf{ap}}_B(e),ft){\approx }_{B(u)}fu$. The motive is proposition-valued, so proof irrelevance closes the coherence.

For $n+0=n$, eliminate $n$ with motive $C(n)=n+0{\approx }_{\mathbb{N}}n$. The zero branch is reflexivity; the successor branch maps the induction proof through the successor clause of observational equality. For $0+n=n$, recurse in the argument on which addition is defined: the zero case is reflexivity and the successor case is again successor congruence. With the recursion orientation $m+0=m$ and $m+\mathsf{suc}n=\mathsf{suc}(m+n)$, the second construction is immediate by induction on $n$, whereas the first uses induction on $n$ to expose the left argument.

Universe equality of W-types consists of $e_A:A{\approx }_{\mathcal{U}}{A}^{\prime }$ and, after contravariantly casting an $a^{\prime }:A^{\prime }$ back to $A$, equality of arities $B(a){\approx }_{\mathcal{U}}{B}^{\prime }(a^{\prime })$. Equality of $\mathsf{sup}(a,f)$ and $\mathsf{sup}(a^{\prime },f^{\prime })$ consists of a root equality $r:a\sim a^{\prime }$ and pointwise equality of child functions after casting indices and subtree types along the arity equality. In the numeral encoding, distinct raw child functions have empty domains at zero and propositionally corresponding domains at successors; function observational equality therefore identifies them whenever they encode the same recursive children.

In the full rule the motive may mention the equality proof $e$. Replace it by the nondependent family obtained by fixing one proof $e_0$. For any other $e$, Irr gives $e\equiv e_0$, and context conversion changes the fixed-family result to the desired fiber at $e$. Thus nondependent transport followed by proof-irrelevance conversion derives the proof-dependent rule.

For $e:{\mathrm{\Pi }}_{x:A}B(x){\approx }_{\mathcal{U}}{\mathrm{\Pi }}_{x^{\prime }:A^{\prime }}{B}^{\prime }(x^{\prime })$, ${\mathsf{pr}}_{1}e$ equates $A$ with $A^{\prime }$. Given $a^{\prime }:A^{\prime }$, cast it contravariantly to $a:A$. The second component supplies $B(a){\approx }_{\mathcal{U}}{B}^{\prime }(a^{\prime })$ at this pair of related arguments. Hence $f(a):B(a)$ may be cast along that equality to $B^{\prime }(a^{\prime })$. Abstracting over $a^{\prime }$ gives a term of ${\mathrm{\Pi }}_{a^{\prime }:A^{\prime }}{B}^{\prime }(a^{\prime })$, as required.

If a neutral $n:\mathbb{N}$ were reduced by a general same-type cast rule, later substitution $n:=0$ would overlap Cast-Nat-Z, while $n:=\mathsf{suc}m$ would overlap Cast-Nat-S; without knowing the equality proof is reflexive, the two reduct schemes need not join. For a type variable $X$ there is no head constructor selecting a structural cast clause at all. Thus only Cast-Refl removes the cast when its equality evidence computes to reflexivity; otherwise the cast must remain neutral.

By definition ${\mathsf{subst}}_B(e,p)$ is cast from $B(t)$ to $B(u)$ along ${\mathsf{ap}}_B(e)$. For $e=\mathsf{refl}(t)$, the groupoid computation gives ${\mathsf{ap}}_B(e)=\mathsf{refl}(B(t))$. Cast-Refl reduces the cast to $p$, and observational reflexivity yields ${\mathsf{subst}}_B(\mathsf{refl}(t),p){\approx }_{B(t)}p$.

Reflexivity of $R$ is commutativity of addition; symmetry swaps the two sides; transitivity cancels the common middle summands after associating and commuting. These equalities are observational proofs in $\mathbb{N}$. For the displayed representatives the quotient rule reduces their equality to $$\mathsf{suc}0+\mathsf{suc}0{\approx }_{\mathbb{N}}\mathsf{suc}(\mathsf{suc}0)+0,$$ then addition computation reduces both sides to $\mathsf{suc}(\mathsf{suc}0)$. The natural observational-equality clause reduces this through two successor steps and the zero clause to $\mathrm{\top }$.

Precomposition sends $g:A/R\to C$ to $f=g\pi$; congruence of $g$ applied to the quotient path constructor supplies preservation of $R$. Conversely the quotient eliminator extends an $R$-respecting $f$ to $\overline{f}$ with $\overline{f}(\pi a)\equiv f(a)$. One composite is the computation rule. Quotient induction proves the other pointwise on $\pi a$, and function observational equality promotes it to equality of maps. Thus the two constructions are a bijection up to ${\approx }_{}$.

For heterogeneous evidence $(e,q)$, coercion is $\mathsf{cast}(S,T,e,s)$ and coherence is $q$; symmetry uses inverse type equality and inverse cast coherence, while transitivity composes the type equalities and uses cast composition. When $S\equiv T$, map ordinary observational equality $q:s\sim t$ to $({\mathsf{refl}}_S,q^{\prime })$, where Cast-Refl identifies $\mathsf{cast}(S,S,\mathsf{refl},s)$ with $s$. Conversely eliminate the existential and use proof irrelevance to replace $e$ by reflexivity before applying $q$. Without Cast-Refl, the forward pair would relate a stuck cast rather than $s$ itself.

In context $h:\mathrm{\perp }$, use proof elimination to form ${\mathsf{abort}}_{\mathbb{N}}(h):\mathbb{N}$. Its scrutinee is a neutral variable, so the term is a weak-head normal form, but its head is neither $\mathsf{0}$ nor $\mathsf{suc}$. Consistency excludes such a closed $h$ and is therefore necessary for closed numeral canonicity. In the intensional base, normalization first gives canonical closed forms and then implies consistency by observing that $\mathbf{0}$ has none; here the metatheorem uses consistency to rule out neutral proof eliminations.

Irr makes any two proofs of $\mathbf{2}{\approx }_{\mathcal{U}}\mathbf{2}$ judgmentally equal, and reflexivity inhabits the type. In the univalent base, encode–decode identifies universe loops at $\mathbf{2}$ with Boolean automorphisms, of which identity and swap are the two possibilities. Observational universe equality records only a proof-irrelevant structural comparison; its eliminator cannot recover the chosen automorphism, so the decode map distinguishing identity from swap is unavailable.

If $p,q:t{\approx }_{A}u$, Irr directly gives $p\equiv q$; no case split on the existence of equality is involved. For $P:\mathsf{SProp}$, Obs-Prop identifies $P{\approx }_{\mathsf{SProp}}\mathrm{\top }$ with logical equivalence $P\leftrightarrow \mathrm{\top }$, hence with $P$. A uniform decision procedure for that observational equality would therefore decide every proposition $P$. Proof irrelevance supplies uniqueness of evidence, not existence or decidability of evidence.

For $p:A\approx A^{\prime }$ and $q:\mathrm{\Pi }x:A.B(x)\approx B^{\prime }(\mathsf{cast}(p,x))$, casting $f:\mathrm{\Pi }x:A.B(x)$ forward is $${\mathsf{cast}}_{\mathrm{\Pi }}(p,q,f):=\lambda x^{\prime }:A^{\prime }.\mathsf{cast}(q(\mathsf{cast}(p^{-1},x^{\prime })))(f(\mathsf{cast}(p^{-1},x^{\prime }))).$$ The domain coercion is contravariant because $f$ consumes an $A$, while the result coercion is indexed by that coerced argument. For constant $B,B^{\prime }$ the formula becomes $\lambda x^{\prime }.\mathsf{cast}(q,f(\mathsf{cast}(p^{-1},x^{\prime })))$. If both equality codes are reflexive, both casts compute away and $\mathrm{\Pi }$-eta returns $f$; if only the codomain code is reflexive, the remaining operation is precomposition by the inverse domain cast.