ch:cubical-cartesian: ch:cubical-cartesian

The only dimension terms in context $i,j$ are $0,1,i,j$. Constants fail one endpoint equation; $i$ has restrictions $0$ and $1$, so its second face is not $j$; and $j$ has both restrictions equal to $j$, so its first face is not $0$. Since the Cartesian interval has no equation identifying distinct constants or variables, these four cases exhaust the grammar and no connection term exists.

cof-reflect turns the true equation $r=s$ into judgmental equality of dimension terms. Congruence of substitution then gives the judgmental equality of cofibrations $\alpha [r/i]=\alpha [s/i]$. Convert the derivation of truth for the first formula along this equality to obtain $\mathrm{\Gamma }⊢\alpha [s/i]\mathsf{true}$.

Restricted contexts are pullbacks along the subobjects classified by their cofibrations. Two consecutive restrictions therefore classify the intersection $\phi \wedge \psi$, which is symmetric. Syntactically, weaken each truth hypothesis across the other and apply restriction substitution in the opposite order; proof irrelevance identifies the two derivations. Thus a constrained term carries the same two boundary equalities in either order, so the final pair is read componentwise and is well defined.

With empty tube, $\mathsf{com}$ has only the cap, so its source-equals-target boundary specializes to coe-id. With a constant type line, the dependent composite is homogeneous and its cap and tube equations are exactly hcom-cap and hcom-tube. Conversely encode coercion by an empty tube and homogeneous composition by a constant line. On the nominally empty overlap the premise is $0=1$; cof-absurd supplies the compatibility term required for the system.

Fill a square in coordinates $i,k$ with cap $p@k$, tube $i=0\mapsto a$ and $i=1\mapsto q@k$, using homogeneous composition in $i$. The remaining lid as $k$ varies has endpoints $a,c$ and is the composite $p\cdot q$; the cap and tube rules give all four faces. For inverse, use the degenerate cap at $a$ and the two side faces supplied by $p$ in opposite order. The lid runs from $b$ to $a$, and overlap compatibility follows from the endpoint equations of $p$.

Compose ${\mathsf{pr}}_1$ of the cap and tube in $A$ to obtain the first component $a_s$, and use the corresponding filler to obtain a line $a(i)$ from the cap’s first component to $a_s$. Convert every tube second component along the filler boundary into $B(a(i))$, then compose these heterogeneous second components to $b_s:B(a_s)$. Return $(a_s,b_s)$. At the cap, both components reduce by their cap rules; on each tube face, the filler selects the tube first component and the second composition selects its second component, proving the two boundary equations.

Fill $q$ to a square whose one side is the constant reflexivity line and whose opposite side is $q$. This gives a type line from $C(a,\mathsf{refl})$ to $C(b,q)$; coerce $c$ along it. When $q$ is reflexivity, the filler is produced by an $\mathsf{hcom}$ with degenerate boundary. There is a path from this filler to the constant square, hence a path from the result to $c$, but no rule makes the open $\mathsf{hcom}$ judgmentally constant. Thus the computation is propositional rather than judgmental.

Define the partial filler at coordinate $i$ by composing only as far as $i$, using the connection $i\wedge j$ (with orientation adjusted to the chapter’s formula). At $i=0$, absorption $0\wedge j=0$ makes composition the cap. On a tube face, Sys-sel selects the tube, and at $i=1$ the unit law $1\wedge j=j$ gives the original composite. Associativity and absorption of $\wedge$, plus its endpoint unit/zero laws, are the De Morgan equations used.

Reindex the filling coordinate by $i\mapsto 1-i$. A tube $u(i)$ becomes $u(1-i)$, its source face at $1$ becomes the new source at $0$, and its target at $0$ becomes the new target at $1$. Consequently $${\mathsf{comp}}_i^{1\to 0}A(i)[\phi \mapsto u(i)]a={\mathsf{comp}}_i^{0\to 1}A(1-i)[\phi (1-i)\mapsto u(1-i)]a,$$ up to the renaming of the bound dimension. Involution $1-(1-i)=i$ shows reversing twice returns the original composite.

The mnemonic Glue expression is $\mathsf{Glue}[(r=0)\mapsto (A,e)]B$. At $r=0$ its true face restricts to $A$, matching the primitive V boundary; at $r=1$ the face is false and the base is $B$, matching the other V boundary. Glue introduction and unglue thus suggest $\mathsf{Vin}$ and $\mathsf{Vout}$ and reproduce the same endpoint shapes.

This comparison is not a judgmental equality: definition 81.22 declares primitive $\mathsf{V}$, and no local formation or computation rule identifies it with a Glue term. Making the mnemonic internal requires the imported packages of convention 218.26: Angiuli’s complete $\mathsf{coe}/\mathsf{hcom}$ rules for V and universes, together with the ABCFHL Cartesian Glue/universe composition package. The endpoint comparison alone supplies neither package.

At $r=0$, the type is $A$ and ${\mathsf{Vin}}_0(a,e(a))\equiv a$, so uniqueness reads $v\equiv v$; at $r=1$ it similarly reduces through the $B$ component. For $\mathsf{Vout}(\mathsf{Vin}(a,b))$, beta returns the $B$ component. On $r=0$ that component is $e(a)$, agreeing with the Vout boundary; on $r=1$ it is $b$ on both routes. Hence every overlap has the same reduct and the rules introduce no ambiguous critical pair.

Transporting $\mathsf{ff}$ along the V line first uses the V-coercion rule, which exposes the underlying equivalence $e_{\mathsf{not}}$. Coercion in the constant Boolean family is identity, and Boolean computation gives $e_{\mathsf{not}}(\mathsf{ff})\equiv \mathsf{tt}$. With univalence as an opaque axiom, the first step is unavailable: there is no computation rule exposing the equivalence from transport along the postulated universe path, so the term remains stuck.

Take $M=p@i$ for a path variable $p$; it is a value while substitution $[0/i]$ makes it reduce to the endpoint. Similarly, a system or coercion blocked by a diagonal can be a value before substitution and constructor headed afterward, so evaluating first and then substituting yields a neutral value whereas substituting first and evaluating yields its endpoint. Computational membership quantifies over every further dimension substitution and requires coherent results there. Applying its coherence clause to $\psi$ identifies these two evaluations by $\doteq$, even though their raw value syntax differs.

With no dimension names, the only endomorphism of the dimension context is identity, so the restriction/coherence quantification has one trivial case. The Boolean clause evaluates both terms and relates them exactly when their values are the same constructor. Thus $M\doteq N\in \mathbf{2}[\cdot ]$ iff both evaluate to $\mathsf{tt}$ or both to $\mathsf{ff}$, which is the ordinary PER interpretation used in the elementary canonicity proof.

Add judgments for dimension terms, cofibrations and their entailment, constrained systems, path abstraction/application, Glue, and the Kan operations $\mathsf{coe},\mathsf{hcom}$. Synthesis exposes annotated eliminators; checking handles introductions and verifies every system branch and pairwise overlap. cof-case is dispatched by the finite cofibration-entailment procedure when checking a system. Normalization is invoked when comparing a synthesized type with an expected type and when comparing the types/terms on overlapping tubes. The claim is confined to ${\mathcal{C}}_{\mathrm{SA}}$.

$p@i$ is unstable on $(i=0)\vee (i=1)$, reducing there to the corresponding endpoint. $p@0$ is already an endpoint redex, so its instability locus is $1$ and it reduces to the left endpoint everywhere. The displayed $\mathsf{hcom}$ is blocked until either $r=s$, where the cap rule returns $x$, or $\phi$, where the tube rule returns $t$ (with the indicated substitution of its bound dimension). Its locus is therefore $(r=s)\vee \phi$; the overlap equality is a system well-formedness premise.

Take $A=B=\mathbf{2}$ and $e$ the negation equivalence. In ${\mathsf{V}}_i(\mathbf{2},\mathbf{2},e)$, coercion from $0$ to $1$ is the forward map of $e$, hence sends $\mathsf{tt}$ to $\mathsf{ff}$ and $\mathsf{ff}$ to $\mathsf{tt}$; coercion from $1$ to $0$ uses the inverse, which is again negation. Composing the two lines therefore fixes both constructors. In the De Morgan presentation the corresponding Glue line has the same endpoint fibers, and Glue transport is also the forward equivalence. Thus the two presentations agree on both closed Boolean transports, although their internal Kan constructions use different cofibration languages.