ch:truncation-logic: ch:truncation-logic

For transport along reflexivity, path induction on $p$ leaves ${\mathsf{tr}}_{\mathsf{refl}}^P(u)=u$, the computation rule for $\mathsf{tr}$. For composition, induct first on $p$ and then on $q$; both sides reduce to $u$ by the same rule. For $\mathsf{ap}$, induct on $p$: ${\mathsf{ap}}_f({\mathsf{refl}}_x)\equiv {\mathsf{refl}}_{fx}$ is its computation rule. The inverse and concatenation laws for $\mathsf{ap}$ then follow by one or two further path inductions, with every base case reflexivity.

From a center $a_0:A$ and contraction $a_0=a$, the constant map $A\to \mathbf{1}$ and $\ast \mapsto a_0$ are inverse up to homotopy. An equivalence with $\mathbf{1}$ transports its center and contraction to $A$. Finally, an inhabited proposition $(a_0,h)$ is contractible with center $a_0$ and contraction $h(a_0,a)$; conversely every contractible type is a proposition by concatenating paths through its center.

Let $x_0$ be the center of $X$ and set $y_0=r(x_0)$. For $y:Y$, the contraction path $x_0=s(y)$ gives ${\mathsf{ap}}_r(x_0=s(y)):y_0=r(sy)$; concatenate with the retraction homotopy $r(sy)=y$. This contracts every $y$ to $y_0$, so $Y$ is contractible.

Take $A=\mathbf{0}$. For any $x,y:A$ there are no such endpoints, so ${\mathrm{\Pi }}_{x,y:A}\mathsf{isContr}(x=y)$ is inhabited by empty elimination; nevertheless $A$ has no center and is not contractible. Extending the hierarchy below $-2$ would iterate a vacuous endpoint condition and add no new meaningful property, so contractibility is chosen as the base rather than defining a weaker “$-3$-type.”

Let $(a_0,c)$ contract $A$. The maps $P(a_0)\to {\mathrm{\Sigma }}_{x}P(x)$ and back are $u\mapsto (a_0,u)$ and $(x,v)\mapsto {\mathsf{tr}}_{c(x{)}^{-1}}^{P}v$. The first round trip is transport along reflexivity. For the second, the base path is $c(x):a_0=x$; its fiber component starts at ${\mathsf{tr}}_{c(x)}^P({\mathsf{tr}}_{c(x{)}^{-1}}^{P}v)$ and ends at $v$. Thus inverse transport must occur first and forward transport second; functoriality and $c(x{)}^{-1}\cdot c(x)=\mathsf{refl}$ give the required fiber path.

Regard $A\times B$ as the constant-family sum ${\mathrm{\Sigma }}_{a:A}B$ and apply closure of $n$-types under $\mathrm{\Sigma }$. For $n=0$, the $\mathrm{\Sigma }$-path theorem gives $((a,b)=(a^{\prime },b^{\prime }))\simeq {\mathrm{\Sigma }}_{p:a=a^{\prime }}(b=b^{\prime })$. Since $A$ and $B$ are sets, both the base path type and every fiber path type are propositions; a $\mathrm{\Sigma }$ of a proposition with propositional fibers is a proposition.

Coproduct encode–decode identifies same-summand paths with paths in $A$ or $B$ and mixed-summand paths with $\mathbf{0}$. For $n\ge 0$, these code types are $(n-1)$-types, so every identity type of $A+B$ is an $(n-1)$-type and $A+B$ is an $n$-type. At $n=-1$ take $A=B=\mathbf{1}$: both summands are propositions but $\mathbf{1}+\mathbf{1}\simeq \mathbf{2}$ has two distinct points and is not a proposition.

Let $r:X\to Y$, $s:Y\to X$, and $ϵ:rs\sim {\mathrm{id}}_Y$, with $X$ a proposition. For $y,y^{\prime }:Y$, concatenate ${ϵ}_y^{-1}$, the path ${\mathsf{ap}}_r(h(sy,s{y}^{\prime }))$ supplied by propositionality of $X$, and ${ϵ}_{y^{\prime }}$. This yields $y=y^{\prime }$, so $Y$ is a proposition.

The function type $A\to B$ is a set because its pointwise identity types are propositions and function extensionality transfers that fact to paths of functions. Now $A\simeq B={\mathrm{\Sigma }}_{f:A\to B}\mathsf{isEquiv}(f)$. The base is a set and each $\mathsf{isEquiv}(f)$ is a proposition, so closure of sets under dependent sums makes $A\simeq B$ a set.

Define $d$ by double recursion. Set $d(0,0)=\mathsf{inl}(\mathsf{refl})$; the cases $(0,\mathsf{suc}n)$ and $(\mathsf{suc}m,0)$ are negative because the path-code theorem maps such a path to $\mathbf{0}$. For successors, map a positive path by ${\mathsf{ap}}_{\mathsf{suc}}$ and map a negative witness $k$ to $p\mapsto k(\mathsf{sucInjective}(p))$. The same path-code theorem supplies successor injectivity, so all four clauses are total.

Fix $x:X$ and use $\mathsf{J}$ on $p:x=x$ with motive $$C(y,p):=\prod _{q:x=y:p=q}.$$ At $y=x,p={\mathsf{refl}}_x$, the branch is $\lambda q.h({\mathsf{refl}}_x,q)$, where $h$ is the hypothesis that each path type is a proposition. Thus $\mathsf{J}(C,-,x,p)(q):p=q$. The computation rule at $p=\mathsf{refl}$ is judgmental, and abstracting over $x,p,q$ gives $K$.

Propositional-truncation recursion defines $\Vert f\Vert (|a|)=|f(a)|$; the target is a proposition, so it supplies all path coherence. Identity and composition follow by function extensionality and truncation induction. The map $\Vert A\times B\Vert \to \Vert A\Vert \times \Vert B\Vert$ uses the two projections. For the inverse, eliminate first from $\Vert A\Vert$ and then from $\Vert B\Vert$ into the proposition $\Vert A\times B\Vert$, sending $(a,b)$ to $|(a,b)|$. Truncation induction proves the round trips.

Flatten $\Vert \Vert A\Vert \Vert$ by truncation recursion extending the identity on $\Vert A\Vert$; its inverse is the constructor $t\mapsto |t|$. Both composites agree by truncation induction into propositions. Similarly, the unique map $\Vert \mathbf{1}\Vert \to \mathbf{1}$ and $\ast \mapsto |\ast |$ are inverse: one composite is judgmental and the other follows because $\Vert \mathbf{1}\Vert$ is a proposition.

Dependent truncation elimination sends $f:{\mathrm{\Pi }}_{a:A}Q(|a|)$ to $\overline{f}:{\mathrm{\Pi }}_{t:\Vert A\Vert }Q(t)$ with the specified constructor computation. Precomposition is one inverse by that computation. For the other, dependent function extensionality reduces equality of sections to pointwise equality, and every $Q(t)$ is a proposition. Hence the precomposition map is an equivalence, with inverse dependent elimination.

Suppose $s_A:\Vert A\Vert \to A$ were polymorphic. Naturality under equivalences, obtained by identity induction in the universe, says that for the Boolean swap $e$, $e(s_{\mathbf{2}}(t))=s_{\mathbf{2}}(\Vert e\Vert (t))$. Since $\Vert \mathbf{2}\Vert$ is a proposition, $\Vert e\Vert$ is the identity. Thus $s_{\mathbf{2}}(t)$ is fixed by swap. Boolean case analysis shows neither constructor is fixed, a contradiction. Therefore no such polymorphic family exists.

For fixed $x,y$, a decision of $x=y$ determines the usual weakly constant endomap of $x=y$: return the chosen positive proof, or eliminate a supplied path against the negative branch. The type asserting weak constancy is a proposition, so the merely given decision can be untruncated into such an endomap. The collapse lemma makes $x=y$ a proposition. Since this holds for all $x,y$, $X$ is a set.

From a choice function $c:{\mathrm{\Pi }}_x\Vert P(x)\Vert \to P(x)$, map $g:{\mathrm{\Pi }}_x\Vert P(x)\Vert$ to $x\mapsto c_x(gx)$ and then truncate the resulting section. Conversely, given $\Vert {\mathrm{\Pi }}_{x}P(x)\Vert$, eliminate it into the proposition ${\mathrm{\Pi }}_x\Vert P(x)\Vert$ and send $f$ to $x\mapsto |f(x)|$. Both composites are equal because their codomains are propositions. These maps establish the stated equivalence between the two choice formulations.

LEM implies double-negation elimination: for propositional $A$, split on $A+\mathrm{\neg }A$; the positive branch returns its witness and the negative branch contradicts $\mathrm{\neg }\mathrm{\neg }A$. Conversely apply the restricted principle to the proposition $A+\mathrm{\neg }A$ and the constructively provable $\mathrm{\neg }\mathrm{\neg }(A+\mathrm{\neg }A)$. This yields $A+\mathrm{\neg }A$ for every proposition $A$, which is LEM in its proposition-restricted form.

For $u,v:A+\mathrm{\neg }A$, eliminate on both. Two positive cases agree because $A$ is a proposition; two negative cases agree by function extensionality into $\mathbf{0}$; mixed cases are impossible because the negative witness applies to the positive one. Hence $A+\mathrm{\neg }A$ is a proposition. A dependent product of propositions is a proposition, so ${\mathrm{\Pi }}_{A:\mathcal{U}}(\mathsf{isProp}(A)\to A+\mathrm{\neg }A)$ is a proposition.

The constructor map $P+Q\to \Vert P+Q\Vert =P\vee Q$ is one direction. Because $P+Q$ is a proposition under the disjointness hypothesis—same-side paths use propositionality and mixed sides contradict $\mathrm{\neg }(P\times Q)$— truncation elimination supplies $P\vee Q\to P+Q$. The two composites are equal by propositionality, so the maps form an equivalence.

Since $\Vert A{\Vert }_m$ is an $m$-type and hence an $n$-type for $m\le n$, the $n$-truncation eliminator extends the constructor $A\to \Vert A{\Vert }_m$ to a map $\Vert A{\Vert }_n\to \Vert A{\Vert }_m$. Applying $m$-truncation gives $\Vert \Vert A{\Vert }_n{\Vert }_m\to \Vert A{\Vert }_m$. The inverse is induced by $a\mapsto |{|}_m(|a{|}_n)$. Truncation induction and the uniqueness of maps into an $m$-type prove both composites equal to the identity.

For $f:A\to B$, recursion into the $n$-type $\Vert B{\Vert }_n$ defines $\Vert f{\Vert }_n(|a{|}_n)=|f(a){|}_n$; uniqueness proves the identity and composition laws. The projections define a map from $\Vert ({\Vert }_{n}A\times B)$ to the product of truncations. The reverse map is obtained by eliminating successively from both truncations into the $n$-type $\Vert ({\Vert }_{n}A\times B)$ and pairing representatives. Successive truncation inductions prove the two round trips.

If $A$ is connected, $\Vert A\Vert$ is inhabited and each $\Vert x=y\Vert$ is inhabited by the definition of $0$-connectedness. In the other direction choose merely $a_0:A$. For any $x:A$, the assumed $\Vert a_0=x\Vert$ shows that every two points have the same image in the set truncation; hence $\Vert A{\Vert }_0$ is an inhabited proposition and therefore contractible. This is precisely connectedness.

An equivalence is injective: if $ex=ey$, apply its inverse and the two section paths to obtain $x=y$. Case-analyze $e(\mathsf{tt})$. If it is $\mathsf{tt}$, injectivity excludes $e(\mathsf{ff})=\mathsf{tt}$, so Boolean exhaustiveness forces $e(\mathsf{ff})=\mathsf{ff}$ and function extensionality gives $e=\mathrm{id}$. If it is $\mathsf{ff}$, the same argument forces the other value to be $\mathsf{tt}$, giving $e=e_{\mathsf{not}}$. These cases are mutually exclusive by Boolean separation.

A quasi-inverse supplies both factors by taking the same inverse. From a left inverse $g$ and a right inverse $h$, naturality of the homotopies gives $g\simeq h$; replace one by the other to obtain a quasi-inverse. When $f$ is an equivalence, each type ${\mathrm{\Sigma }}_g(gf\simeq \mathrm{id})$ and ${\mathrm{\Sigma }}_h(fh\simeq \mathrm{id})$ is contractible: its center is the inverse extracted from the contractible fibers, and inverse maps with the indicated law are unique. Their product is contractible, hence a proposition. If it is empty it is also a proposition, so $\mathsf{biinv}(f)$ is always a proposition.

There is a canonical map $\mathsf{qinv}(f)\to \mathsf{isEquiv}(f)$, hence by truncation elimination a map $\Vert \mathsf{qinv}(f)\Vert \to \mathsf{isEquiv}(f)$ because the target is a proposition. Conversely, an equivalence has a chosen inverse extracted from its fiber centers, so it gives $|q|$ in the truncated quasi-inverse type. Both types are propositions and the two maps preserve their inhabitants, hence they are inverse equivalences.

Propositional-truncation elimination gives $\overline{f}:\Vert A\Vert \to P$ with $\overline{f}(|a|)\equiv f(a)$. If $g$ is another factor, function extensionality reduces $g=\overline{f}$ to pointwise equality, supplied by $\mathsf{isProp}(P)$. For $f:A\to S$ with $S$ a set, the set-truncation eliminator analogously gives $\overline{f}:\Vert A{\Vert }_0\to S$. Its only higher coherence compares the images of two parallel paths; the constructor ${\mathsf{sq}}_0(p,q)$ supplies that comparison, and $\mathsf{isSet}(S)$ makes the required equality of paths unique.