ch:cubical-demorgan: ch:cubical-demorgan

The De Morgan equations give $1-(r\wedge s)=(1-r)\vee (1-s)$, $1-(r\vee s)=(1-r)\wedge (1-s)$, $1-0=1$, $1-1=0$, and $1-(1-r)=r$. Thus reversal is an involutive order-reversing isomorphism. A homomorphism out of the free algebra is determined by the images of its names; reversal sends each name $i$ to $1-i$, so these equations determine it uniquely on every generated term.

Minimum and maximum form a bounded distributive lattice on $[0,1]$, and $1-x$ is an involution satisfying the two De Morgan laws. Freeness extends any assignment of names uniquely by interpreting the operations. Taking a name at $1/2$ shows $i\vee (1-i)=1/2\ne 1$, and $i\wedge (1-i)=1/2\ne 0$, so the algebra is not Boolean. The distinct free De Morgan terms $r=i\wedge (1-i)$ and $s=(i\wedge (1-i))\wedge (j\vee (1-j))$ have the same value under every $[0,1]$ assignment: $min(x,1-x)\le max(y,1-y)$. Thus passage to the Kleene algebra imposes a genuine quotient.

Write every term as a finite join of finite meets of literals by distributivity and De Morgan normalization. In the free bounded distributive lattice, a meet of literals lies below a finite join only if it lies below one summand: assign its literals true and choose incompatible literals false to refute any contrary inequality. Remove absorbed monomials and sort literals and monomials; the result is a unique antichain normal form. Equality is decided by computing these finite normal forms and comparing their sorted antichains.

From $p:{\mathsf{Path}}_A(a,b)$, Path-E gives $pi:A$ in $\mathrm{\Gamma },i:\mathbb{I}$. Application gives $f(pi):B$, and Path-I abstracts $i$; the endpoint computations use Path-$\beta$ followed by function application, yielding $fa$ and $fb$. Expanding definitions, ${\mathsf{ap}}_g({\mathsf{ap}}_{f}p)=\lambda i.g(f(pi))$ is literally ${\mathsf{ap}}_{g\circ f}p$, and ${\mathsf{ap}}_{\lambda x.x}p=\lambda i.pi\equiv p$ by path eta. Identity-type functoriality needs path induction and is only propositional.

For $q(i,j)=p(i\vee j)$, the faces are $q(0,j)=p(j)$, $q(1,j)=b$, $q(i,0)=p(i)$, and $q(i,1)=b$. Since $i\vee (1-i)$ evaluates to $1$ at both endpoints, abstraction gives a loop at $b$. It is not judgmentally ${\mathsf{refl}}_b$: the free De Morgan normal form $i\vee (1-i)$ is not the constant $1$, so for a neutral path $p$ the body does not reduce to the constant body $b$.

For $p:{\mathsf{Path}}_A(a,b)$, the type line is $i\mapsto B(pi)$. The term line $i\mapsto f(pi)$ has endpoints $fa$ and $fb$ by the two path beta rules, so it inhabits ${\mathsf{PathP}}_{(}(i,.)B(pi))(fa)(fb)$. If the line is constant $B$, PathP formation, abstraction, application, beta, and eta reduce respectively to the ordinary Path rules because every endpoint conversion is reflexive.

Distribute conjunction over disjunction to obtain a join of meets of atoms $(i=0)$ and $(i=1)$. Delete any meet containing both atoms for one name, since it equals $0_{\mathbb{F}}$, and delete absorbed monomials. The remaining finite antichain of consistent partial endpoint assignments is canonical: an assignment satisfies the formula exactly when it extends one of these monomials. Enumerating the finitely many endpoint assignments, or comparing the canonical antichains, decides equality of face formulas.

On a DNF, $\mathrm{\forall }i$ retains precisely the information common to the $i=0$ and $i=1$ restrictions; equivalently it is the greatest formula not mentioning $i$ below the original. For the displayed formula, the two restrictions are respectively $1\vee (j=1)=1$ and $(j=0)\vee (j=1)$. Their meet is therefore $(j=0)\vee (j=1)$. It satisfies the adjunction, and any $i$-free lower bound must lie below both restrictions, hence below this meet.

If $0_{\mathbb{F}}=1_{\mathbb{F}}$, the empty face is true. The system with no branches then has any prescribed type by the inconsistent-context rule, and two such terms agree because restriction to the true empty face collapses all judgments. This does not threaten consistency: there is no derivation of $0_{\mathbb{F}}=1_{\mathbb{F}}$ in the empty dimension context, just as empty elimination is harmless unless a term of $\mathbf{0}$ is supplied.

Define fill by composition with the extra branch $(i=0)\mapsto a$. At $i=0$, this face becomes $1_{\mathbb{F}}$, so Sys-sel selects $a$. On the original extent $\phi$, selection chooses the tube $u$. At $i=1$, the definition is exactly the original composition term, since the cap branch is the one required by Comp. These are the three asserted equalities.

First fill the first projection to obtain a line $a(i):A$. On $\phi$, the third fill equality gives $a(i)={\mathsf{pr}}_1(u(i))$. Therefore ${\mathsf{pr}}_2(u(i))$, originally in $B({\mathsf{pr}}_1(u(i)))$, converts to an element of $B(a(i))$. It is consequently a partial element of the line of types $B[a(i)/x]$ with extent $\phi$, and its cap at the source agrees with the second projection of the original cap. The second composition is well typed.

At $i=0$, the first system branch is true and the composite selects $p(j)$; at its target this is $p(1)=b$ with the orientation chosen for the inverse. At $i=1$, the constant branch is true and selects $a$. The overlap at both branches is compatible by the endpoints of $p$. Hence abstraction is a path from $b$ to $a$. Unlike the De Morgan definition $i\mapsto p(1-i)$, this construction uses only endpoint equations and composition, so it remains available in the Cartesian theory.

Use the connection square $(i,j)\mapsto p(i\vee j)$. Its bottom and left faces are $p$, while its top and right faces are constant at $b$. Compose the open square in the remaining direction; the resulting line in the path type has one endpoint the concatenation $p\cdot {\mathsf{refl}}_b$ and the other $p$. For associativity, paste the three connection squares for the constituent paths into the boundary of a cube and compose its open face. The two opposite lids are the two parenthesizations, producing the associativity path.

Induct externally on the numeral. The natural-number transport clause sends $\mathsf{0}$ to $\mathsf{0}$ judgmentally. Its successor clause gives ${\mathsf{transp}}^i\mathbb{N}(\mathsf{suc}\overline{n})\equiv \mathsf{suc}({\mathsf{transp}}^i\mathbb{N}\overline{n})$, which reduces by the induction hypothesis to $\mathsf{suc}\overline{n}$. The argument applies only to constructor-headed numerals; it does not add a schematic regularity rule for neutral terms.

Under restriction by $\phi$, admissible context restriction makes the face true. Glue-form-$1$ therefore reduces the Glue type to the partial type $T$. The introduction rule similarly reduces $\mathsf{glue}[\phi \mapsto t]a$ to $t$ by system selection. Applying unglue-$\beta$ and the same restriction yields $\mathsf{unglue}(t)=f(t)$ on the face. These are the two claimed face computations.

For $y:B$, the fiber of ${\mathrm{id}}_B$ is ${\mathrm{\Sigma }}_{x:B}(x=y)$, centered at $(y,{\mathsf{refl}}_y)$ and contracted by singleton contraction: path induction on $p:x=y$ reduces every $(x,p)$ to the center. This supplies ${\mathsf{id}}_B^{\simeq }$. In the Glue line $E$, the face $i=0$ selects the glued type $A$ by Glue-form-$1$; at $i=1$ the system is empty/identity and Glue reduces to $B$. Hence $E[0/i]\equiv A$ and $E[1/i]\equiv B$.

Fix $b:B$. Apply the extension operation to the empty partial element of ${\mathsf{fib}}_f(b)$ to obtain a center $c_b$. For any $w:{\mathsf{fib}}_f(b)$, apply extension to the partial element that equals $c_b$ on one endpoint and $w$ on the other; the resulting line is a path $c_b=w$. The endpoint rules of extension provide the two boundaries. Thus every fiber has a center and a contraction, so $f$ is an equivalence.

At $i=0$, the face $(i=0)$ is true, so restriction of the Glue system selects the $A$ branch; Glue-form-$1$ gives $\mathsf{ua}(f)(0)\equiv A$. At $i=1$, the $(i=1)$ branch selects $B$ with the identity equivalence, and the other face is false; system selection followed by Glue-form-$1$ gives $\mathsf{ua}(f)(1)\equiv B$. Compatibility on the impossible overlap is automatic.

For $\phi =(i=0)\vee (i=1)$, no $i$-free face lies below it, so $\delta =\mathrm{\forall }i.\phi =0_{\mathbb{F}}$. The transport clause therefore uses the nonconstant Glue-composition branch. At the target $i=1$ the face is true and extension for the identity equivalence contracts the singleton fiber, producing a term connected to $f(a)$. The Glue beta rule and that contraction yield a path ${\mathsf{transp}}^i(\mathsf{ua}(f)i)a=f(a)$ in $B$, which is the propositional computation rule for univalence.

Let $T:{\mathrm{\Sigma }}_{X}P(X)\to {\mathrm{\Sigma }}_{X}Q(X)$ be the total map induced by $t$ over the identity base. If both total spaces are contractible, $T$ is an equivalence. For fixed $X$ and $q:Q(X)$, its fiber is equivalent, by the fiberwise-total-space lemma, to the fiber of $t_X$ at $q$: a path in the base component of $T$ must be ${\mathsf{refl}}_X$, and transport removes it. Fibers of the equivalence $T$ are contractible, so every fiber of $t_X$ is contractible and each $t_X$ is an equivalence.

For dimensions $i,j$, an open square with missing $i=1$ face has tube $\phi =(i=0)\vee (j=0)\vee (j=1)$ and compatible faces $u_0(j),v_0(i),v_1(i)$, with the two corner equalities $u_0(0)=v_0(0)$ and $u_0(1)=v_1(0)$. Composition in $i$ with cap $u_0$ produces the lid $u_1(j)$. The tube computation rule restricts it to $v_0(1)$ at $j=0$ and $v_1(1)$ at $j=1$; the cap rule recovers $u_0$ when the endpoints coincide. Glue the Boolean swap on $i=0$ to $\mathbf{2}$ on the total face. Glue transport computes by the forward equivalence, so the two endpoint calculations are $\mathsf{tt}\mapsto \mathsf{ff}$ and $\mathsf{ff}\mapsto \mathsf{tt}$.