Chapter 218Core route

Cubical Type Theory II: Cartesian Cubes and Computation

Without interval reversal, a coercion from $A (0)$ to $A (s)$ does not produce the backward coercion $A (s) \to A (0)$ needed to coerce a function. Cartesian cubical type theory therefore gives ${coe}^{r \to s}$ arbitrary source and target dimensions and separates coercion from homogeneous composition. A diagonal cofibration is a face equation between dimensions; such cofibrations make the resulting cap equation expressible, and a behavioral semantics proves canonicity.

The Cartesian interval and its cofibrations

Convention 81.1 — Judgment apparatus ¶

The Cartesian interval has only the dimension terms $0$ , $1$ , and variables, but dimension substitution remains unrestricted. Thus $[j / i]$ is allowed even when $j$ is already in scope. Contexts may be extended by $i : I$ and restricted by a cofibration $φ$ ; the judgments $Γ ⊢ r : I$ , $Γ ⊢ φ cof$ , and $Γ ⊢ φ true$ retain their meanings from chapter 80. We write $Γ ⊢ b : A ▹ (φ \mapsto t)$ for the pair of judgments $Γ ⊢ b : A$ and $Γ, φ ⊢ b \equiv t : A$ . Path abstraction $⟨ i ⟩ t$ and application $p @ r$ are as in definition 80.8; their formation premises are those of convention 26.14.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Convention 218.2 — Three signatures ¶

The chapter keeps three systems distinct.

$C_{teach}$: The displayed calculations use exactly the rules explicitly printed here.
$C_{A}$: Computational semantics, V-types, and universes use Angiuli’s Definitions 4.3–4.29 and Rules 4.78–4.104.
$C_{SA}$: Normalization uses the source’s universe-free $Π / Σ / Path / Glue / S^{1}$ signature.

The teaching fragment is not asserted to be an independently complete calculus. A theorem tagged $C_{A}$ or $C_{SA}$ imports the named source signature; a displayed local equation is then either a transcription of that signature or a representative derivation within it. No metatheorem transfers among the three rows without an explicit statement.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Definition 81.2 — The Cartesian interval ¶

The dimension terms of the Cartesian theory are generated by the rules

Γ ctx

Γ ⊢ 0 : I

i-zero

Γ ctx

Γ ⊢ 1 : I

i-one

(i : I) \in Γ

Γ ⊢ i : I

i-var

and by no others: relative to definition 80.1, the term formers $i \land j$ , $i \lor j$ , and $1 - i$ are removed, together with all equations of the De Morgan algebra. The structural rules for dimension variables (weakening, exchange, substitution) are those of chapter 80 and remain unrestricted.

Referenced from 5 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Remark 81.3 — Geometric reading ¶

A context of $n$ dimension variables denotes the $n$ -cube. Substitutions between such contexts are generated by faces ( $[0 / i]$ , $[1 / i]$ ), degeneracies (weakening), symmetries (exchange), and diagonals ( $[j / i]$ ); the resulting category is the Cartesian cube category, the free finite-product category on an interval object with two points [ABC^+21]. The De Morgan cube category already permits the substitution $[j / i]$ . What the Cartesian cofibration language adds is the face condition $i = j$ , which allows a term to reduce specifically on that diagonal. Connections and reversal, by contrast, are absent.

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Definition 81.4 — Cartesian cofibrations ¶

A Cartesian cofibration is a face condition generated by equations between dimension terms, disjunction, and universal quantification over the interval:

Γ ⊢ r : I

Γ ⊢ s : I

Γ ⊢ r = s cof

cof-eq

Γ ⊢ φ cof

Γ ⊢ ψ cof

Γ ⊢ φ \lor ψ cof

cof-disj

Γ, i : I ⊢ φ cof

Γ ⊢ \forall i . φ cof

cof-forall

The exact package is ABCFHL §2.4 [ABC^+21]. Besides formation, it has a proof-irrelevant entailment judgment $φ ⊢_{Γ} ψ$ , a separate judgmental equality $Γ; χ ⊢ φ \equiv ψ cof$ , and substitution in all three judgments. Entailment has hypothesis and weakening; both introductions for $\lor$ ; case analysis from $φ \lor ψ$ ; introduction of $\forall i . φ$ from a derivation with fresh $i$ , and specialization at every dimension term. For equality cofibrations it has congruence generated by equality of interval terms; equality reflection instead turns an entailed interval equation into judgmental equality of interval terms. Here $Γ ⊢ φ true$ abbreviates $⊤ ⊢_{Γ} φ$ . Its distinctive term-level consequences are reflection, collapse at $0 = 1$ , and case splitting; the additional propositional-univalence rule used by the identity-type extension of remark 81.21 produces equality in the separate cofibration-equality judgment [ABC^+21]:

Γ ⊢ r : I

Γ ⊢ r = r true

cof-refl

Γ ⊢ r = s true

Γ ⊢ r \equiv s : I

cof-reflect

Γ ⊢ 0 = 1 true

Γ ⊢ A type

Γ ⊢ abort : A

cof-absurd

Γ ⊢ φ \lor ψ true

Γ, φ ⊢ u : A

Γ, ψ ⊢ v : A

Γ, φ, ψ ⊢ u \equiv v : A

Γ ⊢ [φ \mapsto u, ψ \mapsto v] : A

cof-case

Γ, χ, φ ⊢ ψ true

Γ, χ, ψ ⊢ φ true

Γ; χ ⊢ φ \equiv ψ cof

cof-ext

The case-split term satisfies $Γ, φ ⊢ [φ \mapsto u, ψ \mapsto v] \equiv u : A$ and its mirror image, and any $b$ with the same restrictions equals the split; under $0 = 1$ every term equals $abort$ . Replacing the terms $u, v, b$ by types gives the type-formation and type-selection rules under a true disjunction. Cofibration equality converts restricted judgments, and all rules are stable under dimension substitution. Thus $φ \equiv ψ$ is not an undeclared connective of the cofibration grammar.

Referenced from 4 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Remark 81.5 — The delta in the cofibration language ¶

The scheme $r = s$ includes endpoint faces, diagonals, truth $0 = 0$ , and falsity $0 = 1$ . The diagonal $r = s$ lets homogeneous composition reduce to its cap when source and target agree; $\forall i . φ$ is required to detect the part of a $Glue$ extent that persists along an entire filling dimension. The selected calculus omits conjunction; adding it supports Swan’s identity type with strict computation on $refl$ (remark 81.21) [ABC^+21, Ang19].

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Remark 81.6 — Proof irrelevance and decidability ¶

No proof terms inhabit $Γ ⊢ φ true$ : like the conversion rule, it licenses judgments without leaving a trace in the term. This is tenable only because the grammar of cofibrations is deliberately impoverished — entailment between cofibrations over a fixed dimension context is decidable. Normalize a case by recording a partition of its finitely many dimension variables together with the blocks identified with $0$ or $1$ ; disjunction branches over cases, and $\forall i$ checks every extension of the partition by the fresh variable. There are finitely many such extensions, so this recursion decides the imported entailment rules. Decidability of type checking for the normalized fragment (corollary 81.34) depends on this.

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Exercise 81.1 ¶

★☆☆ Show that the Cartesian theory has no connection: there is no dimension term $t$ with $i : I, j : I ⊢ t : I$ such that $j : I ⊢ t [0 / i] \equiv 0 : I$ and $j : I ⊢ t [1 / i] \equiv j : I$ . (By definition 81.2, $t$ is one of $0$ , $1$ , $i$ , $j$ ; refute each case, using the fact that distinct constants and variables are not judgmentally equal: their raw dimension terms are distinct, and definition 81.2 has no equation that identifies them.)

Referenced from 3 locations

Exercise 81.2 ¶

★☆☆ Derive the transport rule for cofibrations: if $Γ, i : I ⊢ α cof$ , $Γ ⊢ r = s true$ , and $Γ ⊢ α [r / i] true$ , then $Γ ⊢ α [s / i] true$ . (Use cof-reflect and congruence of substitution in judgmentally equal dimension terms.)

Referenced from 3 locations

Exercise 81.3 ¶

★★☆ Show that consecutive restrictions commute: any judgment derivable in context $Γ, φ, ψ$ is derivable in $Γ, ψ, φ$ , and both restrict $Γ$ by the same subshape. Conclude that the iterated constrained judgment $Γ ⊢ b : A ▹ (φ, ψ \mapsto t, u)$ of convention 81.1 is well defined irrespective of the order of constraints: $b = t$ holds under $φ$ and $b = u$ holds under $ψ$ .

Referenced from 3 locations

Coercion and homogeneous composition

The Kan structure of the Cartesian theory consists of two operators: coercion moves an element along a line of types; homogeneous composition caps a tube within a single type.

Definition 81.7 — Cartesian Kan operations ¶

Every type of the Cartesian theory supports coercion, which moves an element along a line of types, and homogeneous composition, which caps a tube in one fixed type:

Γ, i : I ⊢ A type

Γ ⊢ r : I

Γ ⊢ s : I

Γ ⊢ a : A [r / i]

Γ ⊢ {coe}_{i . A}^{r \to s} (a) : A [s / i]

coe

Γ ⊢ r \equiv s : I

Γ ⊢ a : A [r / i]

Γ ⊢ {coe}_{i . A}^{r \to s} (a) \equiv a : A [s / i]

coe-id

Γ ⊢ A type

Γ ⊢ r : I

Γ ⊢ s : I

Γ ⊢ φ cof

Γ, φ, i : I ⊢ t : A

Γ ⊢ a : A

Γ, φ ⊢ t [r / i] \equiv a : A

Γ ⊢ {hcom}_{A}^{r \to s} [φ \mapsto i . t] (a) : A

hcom

Γ ⊢ r \equiv s : I

Γ ⊢ {hcom}_{A}^{r \to s} [φ \mapsto i . t] (a) \equiv a : A

hcom-cap

Γ ⊢ φ true

Γ ⊢ {hcom}_{A}^{r \to s} [φ \mapsto i . t] (a) \equiv t [s / i] : A

hcom-tube

(In hcom-cap and hcom-tube the typing premises of hcom are presupposed, per convention 26.14.) The data $φ \mapsto i . t$ is the tube, $a$ the cap; $r$ is the source and $s$ the target. Both operators commute with substitution — for dimension variables this is the uniformity of the Kan operation, automatic for a syntactic constant.

Referenced from 7 locations

Remark 81.8 ¶

${coe}_{i . A}^{r \to s}$ realizes, judgmentally, the principle that a family over the interval cannot distinguish its fibers; taking $r, s : = 0, 1$ and the line $i . C [p @ i / x]$ over a path $p$ yields transport, hence the recursor of the identity type (cf. definition 30.1). $hcom$ solves a filling problem: the tube prescribes faces on $φ$ moving in a fresh direction $i$ from the cap; the composite is the face at $i = s$ . Unlike the operator ${comp}^{0 \to 1}$ of definition 80.21, source and target are arbitrary dimension terms, and the two boundary equations exhaust the constraints: hcom-cap fires on the diagonal $r = s$ , a cofibration available only by definition 81.4.

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Construction 81.9 — Heterogeneous composition ¶

From the operations of definition 81.7 one defines composition in a line of types, for $Γ, i : I ⊢ A type$ , with tube and cap as in hcom but heterogeneously typed ( $t$ in $A$ , the cap $a$ in $A [r / i]$ , agreement at $[r / i]$ ): ${com}_{i . A}^{r \to s} [φ \mapsto i . t] (a) : = {hcom}_{A [s / i]}^{r \to s} [φ \mapsto j . {coe}_{i . A}^{j \to s} (t [j / i])] ({coe}_{i . A}^{r \to s} (a)) .$ Each tube entry coerces the face $t [j / i]$ from the fiber over $j$ into the fiber over $s$ ; the cap is coerced likewise; the composition is then homogeneous in $A [s / i]$ . The expected equations hold: on $φ$ the right-hand side equals ${coe}_{i . A}^{s \to s} (t [s / i]) \equiv t [s / i]$ by hcom-tube and coe-id; when $Γ ⊢ r \equiv s : I$ it equals ${coe}_{i . A}^{r \to s} (a) \equiv a$ by hcom-cap and coe-id; and the tube–cap compatibility at $j : = r$ follows from $Γ, φ ⊢ t [r / i] \equiv a : A [r / i]$ by congruence.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Proposition 81.10 ¶

If heterogeneous composition is taken as primitive, coercion and homogeneous composition are instances of it: ${coe}_{i . A}^{r \to s} (a)$ is ${com}_{i . A}^{r \to s}$ with the empty tube $φ : = (0 = 1)$ , and ${hcom}_{A}^{r \to s}$ is ${com}_{i . A}^{r \to s}$ with $i$ not free in $A$ . Hence a type theory may take either the pair $(coe, hcom)$ or the single operator $com$ as primitive; the two presentations are interderivable.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Proof of Proposition 81.10

Proof. For the empty-tube instance, the formation rule returns an element of $A [s / i]$ from the cap $a : A [r / i]$ ; its diagonal equation is coe-id. For the constant-line instance, every tube and the cap have type $A$ , and the two composition boundary equations are exactly hcom-cap and hcom-tube. Conversely, construction 81.9 derives heterogeneous composition from the pair and checks both equations there. Thus the two primitive signatures generate the same three operations and boundary equations; see [Ang19, ABC^+21] for the two choices. ◻

Construction 81.11 — Filling ¶

Let $j$ be fresh. The filler of a composition problem is composition to the variable $j$ : ${fill}_{i . A}^{r \to j} [φ \mapsto i . t] (a) : = {com}_{i . A}^{r \to j} [φ \mapsto i . t] (a),$ a term in context $Γ, j : I$ satisfying, by hcom-cap, hcom-tube, and substitution: $\begin{aligned} ({fill}_{i . A}^{r \to j} (\dots)) [r / j] & \equiv a, \\ ({fill}_{i . A}^{r \to j} (\dots)) [s / j] & \equiv {com}_{i . A}^{r \to s} (\dots), \\ Γ, φ, j : I ⊢ {fill}_{i . A}^{r \to j} (\dots) \equiv t [j / i] : A [j / i] . \end{aligned}$ In chapter 80 the filler is manufactured from $comp$ by reindexing the type line along a connection, $A [(j \land i) / i]$ (cf. definition 80.21); here it is a substitution instance of the composition operator itself. This is the precise sense in which the generalized source and target replace connections.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Remark 81.12 — Why arbitrary source ¶

One might fix $r : = 0$ and recover only targets $s$ . But the computation rule for $coe$ at $\prod_{x : A} B$ in construction 81.14 coerces the argument backwards, from $s$ to $j$ and to $r$ ; with reversal $1 - i$ absent, backwards coercions are not derivable from forward ones. Closure of $Π$ -types under the Kan operation therefore forces both endpoints of a composition to be arbitrary dimension terms [ABC^+21].

Concretely, the one-way candidate would have to start ${coe}_{i . \prod_{x : A} B}^{0 \to s} (f) \equiv λ x : A [s / i] . f (?) .$ The hole must have type $A [0 / i]$ , but the only available argument has type $A [s / i]$ ; a forward-only primitive cannot move it backwards. Allowing the source $s$ in ${coe}_{i . A}^{s \to 0} (x)$ fills exactly this hole and yields construction 81.14.

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

At each type former, $coe$ follows the dependent fibers and $hcom$ acts on constructor structure. For a dependent pair, coerce the first component first; its intermediate values determine the family in which to coerce the second.

Construction 81.13 — Coercion in Σ -types ¶

Let $Γ, i : I ⊢ \sum_{x : A} B type$ and $Γ ⊢ p : (\sum_{x : A} B) [r / i]$ . Write $\bar{a} (j) : = {coe}_{i . A}^{r \to j} ({pr}_{1} p)$ for the coercion of the first component to a variable endpoint $j$ , so that $\bar{a} (r) \equiv {pr}_{1} p$ by coe-id. The rule is ${coe}_{i . \sum_{x : A} B}^{r \to s} (p) \equiv (\bar{a} (s), {coe}_{j . B [j / i] [\bar{a} (j) / x]}^{r \to s} ({pr}_{2} p)) .$ The second coercion is along the line $j . B [j / i] [\bar{a} (j) / x]$ , which at $j = r$ is the type of ${pr}_{2} p$ and at $j = s$ is $B [s / i] [\bar{a} (s) / x]$ , as required. When $Γ ⊢ r \equiv s : I$ both components collapse by coe-id, and the pair equals $p$ by $η$ for $Σ$ (definition 27.9).

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Construction 81.14 — Coercion in Π -types ¶

With $Γ, i : I ⊢ \prod_{x : A} B type$ and $Γ ⊢ f : (\prod_{x : A} B) [r / i]$ : ${coe}_{i . \prod_{x : A} B}^{r \to s} (f) \equiv λ x . {coe}_{j . B [j / i] [{coe}_{i . A}^{s \to j} (x) / x]}^{r \to s} (f ({coe}_{i . A}^{s \to r} (x))) (x : A [s / i]) .$ The argument $x$ lives in the fiber over the target; it is coerced backwards to $r$ to be fed to $f$ , and the result is coerced forwards along the line of codomains over the backwards-coerced argument. At $j = r$ the line is the type of $f ({coe}_{i . A}^{s \to r} (x))$ ; at $j = s$ it is $B [s / i] [x / x]$ by coe-id. When $Γ ⊢ r \equiv s : I$ the term collapses to $λ x . f x \equiv f$ by coe-id and $η$ (definition 27.2).

Referenced from 4 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Construction 81.15 — Composition in path types ¶

Let $Γ, i : I, k : I ⊢ A type$ with endpoints $Γ, i : I ⊢ u : A [0 / k]$ and $Γ, i : I ⊢ v : A [1 / k]$ . Heterogeneous composition in the line of path types $i . {PathP}_{k . A} (u, v)$ is computed under the path binder, with the endpoint constraints adjoined to the tube: put $w_{k} : = [φ \mapsto i . t @ k, k = 0 \mapsto i . u, k = 1 \mapsto i . v] .$ Then ${com}_{i . {PathP}_{k . A} (u, v)}^{r \to s} [φ \mapsto i . t] (p) \equiv ⟨ k ⟩ {com}_{i . A}^{r \to s} w_{k} (p @ k) .$ The extra tube entries are compatible with $φ \mapsto i . t @ k$ because the path type of $t$ forces $t @ 0 \equiv u$ and $t @ 1 \equiv v$ . Coercion in path types is the instance $φ : = (0 = 1)$ . Definitional function extensionality survives from chapter 80 unchanged (theorem 80.29): it is a property of the $λ$ -calculus of dimension binders, not of the Kan structure.

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Construction 218.17 — Homogeneous composition in Σ ¶

For $C : = \sum_{x : A} B$ , tube $t : C$ over $φ, i : I$ , and cap $p : C$ , define the first-component filler $a (j) : = {fill}_{i . A}^{r \to j} [φ \mapsto i . {pr}_{1} (t)] ({pr}_{1} p) .$ It satisfies $a (r) \equiv {pr}_{1} p$ and, under $φ$ , $a (j) \equiv {pr}_{1} (t [j / i])$ . The canonical rule is $\begin{aligned} {hcom}_{\sum_{x : A} B}^{r \to s} [φ \mapsto i . t] (p) \\ \equiv (a (s), {com}_{j . B [a (j) / x]}^{r \to s} [φ \mapsto j . {pr}_{2} (t [j / i])] ({pr}_{2} p)) . \end{aligned}$ The filler equality converts the tube’s second component to the displayed dependent fiber. At $r = s$ , both components return the cap; on $φ$ , both return $t [s / i]$ . Thus this main-line rule, rather than an exercise, establishes the $Σ$ -Kan structure used by equivalence types.

Referenced from 5 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Construction 81.16 — Homogeneous composition in Π ; strict base types ¶

Homogeneous composition at $\prod_{x : A} B$ is pointwise. The constant families $i . 2$ and $i . N$ have identity coercions, while composition acts on constructors: $\begin{aligned} {hcom}_{\prod_{x : A} B}^{r \to s} [φ \mapsto i . t] (f) & \equiv λ x . {hcom}_{B}^{r \to s} [φ \mapsto i . t x] (f x), \\ {coe}_{i . 2}^{r \to s} (b) & \equiv b, \\ {hcom}_{2}^{r \to s} [φ \mapsto i . tt] (tt) & \equiv tt, \\ {hcom}_{2}^{r \to s} [φ \mapsto i . ff] (ff) & \equiv ff . \end{aligned}$ Likewise at $N$ , $hcom$ commutes with $0$ and $suc$ . These formulas define the $Π$ , $2$ , and $N$ cases used in this section. The $Σ$ - $hcom$ case is construction 218.17, and the universe case is remark 81.26; theorem 81.29 concerns the complete calculus $C_{A}$ .

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Remark 81.17 — Design space at base types ¶

The constructor-wise $2$ clauses preserve the canonical values used in theorem 81.31; the $N$ clauses preserve $0$ and $suc$ in the same way [ABC^+21].

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Exercise 81.4 ¶

★★☆ Verify proposition 81.10: check that the two instantiations are well typed and that each boundary equation of $com$ specializes to the corresponding equation of coe-id, hcom-cap, hcom-tube. Where is cof-absurd used?

Referenced from 3 locations

Exercise 81.5 ¶

★★★ Using ${hcom}^{0 \to 1}$ with tube cofibration $k = 0 \lor k = 1$ , construct from $p : {Path}_{A} (a, b)$ and $q : {Path}_{A} (b, c)$ a composite $p \cdot q : {Path}_{A} (a, c)$ , and from $p$ an inverse $p^{- 1} : {Path}_{A} (b, a)$ . Check all boundary conditions. (Draw the squares: the cap is $p @ k$ , resp. the degenerate line at $a$ .)

Referenced from 3 locations

Exercise 81.6 ¶

★★☆ Verify the cap and tube equations of construction 218.17, including the conversion that types the second tube on $φ$ .

Referenced from 3 locations

Exercise 81.7 ¶

★★★ Define the path-based eliminator: given $Γ, x : A, p : {Path}_{A} (a, x) ⊢ C type$ and $Γ ⊢ c : C [a / x] [⟨ i ⟩ a / p]$ , construct a term of $C [b / x] [q / p]$ for any $q : {Path}_{A} (a, b)$ , using $coe$ along a line built from the filler of $q$ . Show that its computation rule on the reflexivity path holds only up to a path, and locate the $hcom$ responsible. (This is the sense in which $Path$ is not $Id$ ; cf. remark 81.21.)

Referenced from 3 locations

De Morgan and Cartesian compared

Both theories construct universe paths from equivalences and compute transport along those paths; they differ in where they spend their structure.

Proposition 81.19 — Interderivability ¶

In a theory with connections and reversal, the fixed-direction operator ${comp}^{0 \to 1}$ of definition 80.21 derives the filler — by composing along the reindexed line $A [(j \land i) / i]$ with the cap constraint adjoined to the tube — and reversal derives composition $1 \to 0$ ; in a theory with both connections and diagonal cofibrations, ${comp}^{0 \to 1}$ and the operations of definition 81.7 are interderivable. The two displayed derivations do not transfer to either smaller signature: one mentions connections and reversal, the other a diagonal cofibration. No general non-definability claim is made.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Proof of Proposition 81.19 — Interderivability

Proof. For filling, reindex the line by the connection $j \land i$ and add the face $j = 0 \mapsto a$ to the tube; at $j = 0$ the connection makes the line constant at the cap, and at $j = 1$ it recovers the requested composite. Reindexing by $1 - i$ exchanges the two endpoints and hence derives composition from $1$ to $0$ . The full interderivation in the joint theory is the rule calculation of [ABC^+21]; its hypotheses are exactly connections plus diagonal cofibrations. The Cartesian derivation displayed here uses the diagonal equation hcom-cap, unavailable over $F$ ; the displayed De Morgan derivation uses connections, absent from definition 81.2. These observations bound these constructions only; failure of a construction is not a separation theorem. ◻

Remark 81.20 — Regularity ¶

A Kan operation is regular when composition along a degenerate line with a degenerate tube is the identity. Regularity would make $Path$ satisfy the computation rule of $Id$ on the nose, eliminating Swan’s detour; but no known model combines regularity with univalent universes, and the early De Morgan constructions that assumed it were found to fail exactly there [ABC^+21, Ang19]. The diagonal equations coe-id and hcom-cap are the surviving trace of regularity: the identity is recovered when source and target coincide, not when the problem is degenerate.

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Remark 81.21 — Swan identity types ¶

After extending the displayed Cartesian cofibration grammar with conjunction, both cubical theories recover the rules of definition 30.1 exactly — including the judgmental computation of $J$ on $refl$ — by Swan’s construction: an element of ${Id}_{A} (a, b)$ is a path together with a cofibration on which it is degenerate. The construction requires cofibrations closed under $\land$ and the extensionality rule cof-ext. Consequently the extended theories are extensions of the intensional base of chapter 26–chapter 30, and every construction of part IV can be interpreted [ABC^+21].

Referenced from 5 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Semantically, the two designs are cofibrantly generated notions of fibration in presheaves over two different cube categories; both cube categories are strict test categories, so both presheaf categories classically model the homotopy theory of spaces, but neither type-theoretic model structure is known to be Quillen equivalent to spaces — for the Cartesian operation as stated the answer is negative, repaired by the equivariant refinement of Awodey, Cavallo, Coquand, Riehl, and Sattler, which the syntax of this chapter also interprets [ABC^+21]. The Bezem–Coquand–Huber model, historically first, lives over a monoidal cube category without diagonals: there interval variables are substructural, and it is the absence of contraction — not of connections — that obstructs eliminators for higher inductive types. The Cartesian theory can thus be read as the closure of BCH under contraction, at the price of re-engineering every Kan operation.

Exercise 81.8 ¶

★★☆ In the De Morgan theory, verify that the filler defined from ${comp}^{0 \to 1}$ by the connection formula of proposition 81.19 satisfies the three equations of construction 81.11 (with $r, s : = 0, 1$ ). Which De Morgan algebra equations are used?

Referenced from 3 locations

Exercise 81.9 ¶

★★☆ In the De Morgan theory, derive composition from $1$ to $0$ by reindexing along the reversal, and state precisely the equation between the two composites of a tube and its reversed tube.

Referenced from 3 locations

V-types and universe paths

$Glue$ types transfer to the Cartesian theory verbatim once their composition structure uses diagonal cofibrations; the Cartesian literature also isolates a minimal universe-path primitive, the V-type, which we present in the fourfold order of convention 27.1.

Definition 81.22 — V-types ¶

Fix $Γ ⊢ r : I$ . The data of a V-type is a partial type and cubical equivalence on $r = 0$ over a total type ( $≃$ per definition 80.31):

Γ ⊢ r : I

Γ, r = 0 ⊢ A type

Γ ⊢ B type

Γ, r = 0 ⊢ e : A ≃ B

Γ ⊢ V_{r} (A, B, e) type

v-form

Γ, r = 0 ⊢ a : A

Γ ⊢ b : B

Γ, r = 0 ⊢ {pr}_{1} e a \equiv b : B

Γ ⊢ {Vin}_{r} (a, b) : V_{r} (A, B, e)

v-intro

Γ ⊢ v : V_{r} (A, B, e)

Γ ⊢ {Vout}_{r} (v) : B

v-elim

subject to the boundary equations $\begin{matrix} Γ, r = 0 ⊢ V_{r} (A, B, e) \equiv A type Γ, r = 1 ⊢ V_{r} (A, B, e) \equiv B type \\ Γ, r = 0 ⊢ {Vin}_{r} (a, b) \equiv a : A Γ, r = 1 ⊢ {Vin}_{r} (a, b) \equiv b : B \\ Γ, r = 0 ⊢ {Vout}_{r} (v) \equiv {pr}_{1} e v : B Γ, r = 1 ⊢ {Vout}_{r} (v) \equiv v : B \end{matrix}$ and the computation and uniqueness rules ${Vout}_{r} ({Vin}_{r} (a, b)) \equiv b, v \equiv {Vin}_{r} (v, {Vout}_{r} (v)),$ where in the uniqueness rule the first argument is $v$ read at $r = 0$ , where $V_{r} (A, B, e) \equiv A$ . The universe is closed under $V$ : a code former with the same rules.

Referenced from 6 locations

Remark 81.23 — Why the data is partial, and asymmetric ¶

The partiality in v-form is forced by diagonals: $r$ may be a variable occurring in $A$ , $B$ , $e$ , so one cannot demand that the “left” data be dimension-independent; and if $A$ were required only on $r = 0$ and $B$ only on $r = 1$ , the equivalence relating them could not be stated. The chosen shape — $A$ , $e$ partial on $r = 0$ , $B$ total — is the minimal one making both the equivalence and coercion across the line expressible [Ang19].

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Remark 81.24 — V versus Glue ¶

The primary presentation in $C_{A}$ is the primitive $V$ of definition 81.22. Its boundary behavior can be remembered by a Glue mnemonic: glue $(A, e)$ to the total $B$ on $r = 0$ ; at $r = 1$ the extent is empty and the result is $B$ . One may also draw a redundant identity branch $(B, {id}_{B})$ on $r = 1$ , but this chapter asserts neither judgmental equality nor an internal equivalence between those two Glue expressions and primitive $V$ . General Cartesian Glue/formal-composition packages do more work, including universe composition, and belong to the exact imported signatures in convention 218.2 [Ang19, ABC^+21].

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Convention 218.26 — Imported Kan closure for C_ A ¶

The complete $coe / hcom$ clauses for $Σ$ , $V$ , the universe hierarchy, base types, $0$ , and the circle are imported from Angiuli’s Rules 4.78–4.104 and Appendix A [Ang19]. The complete Cartesian Glue/universe package used in the proof-theoretic presentation is imported from ABCFHL §§2.12–2.15 [ABC^+21]. The local $Σ$ -equation construction 218.17 and the V-coercion equation below are transcriptions or consequences of those packages; they are not advertised as an exhaustive replacement for them. The V-coercion clause used by the theorem is fixed before use: $\begin{matrix} (V - coe) & {coe}_{i . V_{i} (A, B, e)}^{0 \to 1} (a) \equiv {coe}_{j . B}^{0 \to 1} (({pr}_{1} e) a) . \end{matrix}$

Referenced from 4 locations

Theorem 218.27 — Imported: computational universe paths in C_ A ¶

For Kan types $A, B : U$ and $e : A ≃ B$ , there are terms $ua (e) : = ⟨ i ⟩ V_{i} (A, B, e) : {Path}_{U} (A, B)$ and ${ua}_{β} (e, a) : {Path}_{B} ({coe}_{i . V_{i} (A, B, e)}^{0 \to 1} (a), ({pr}_{1} e) (a)) .$ These are the universe-path and transport clauses used from Angiuli’s Theorem 4.105. No claim that a separately defined $pathToEquiv$ is an equivalence is included here.

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Proof of Theorem 218.27 — Imported: computational universe paths in C_ A

Proof. The imported V-coercion rule first builds a V-element with v-intro. At $i = 1$ this element reduces to its $B$ -component, and its correcting homogeneous composition has the true tube $1 = 1 \mapsto ({pr}_{1} e) a$ . Rule hcom-tube therefore gives the right-hand side of (V- $coe$ ); the remaining faces ensure uniformity when the index is a variable.

Define ${ua}_{β} (e, a) : = ⟨ x ⟩ {coe}_{j . B}^{x \to 1} (({pr}_{1} e) a) .$ At $x = 0$ , equation (V- $coe$ ) gives the required transported endpoint; at $x = 1$ , coe-id gives $({pr}_{1} e) a$ . Thus ${ua}_{β} (e, a)$ has type ${Path}_{B} ({coe}_{i . V_{i} (A, B, e)}^{0 \to 1} (a), ({pr}_{1} e) a) .$ The boundary equations of v-form make $ua (e)$ a universe path, and the displayed calculation constructs ${ua}_{β}$ . The typing and Kan-coherence proof is imported from Theorem 4.105 of [Ang19]; the calculation above isolates its only nonformal endpoint, the unfolding of V-coercion. ◻

Remark 81.26 — Composition in the universe ¶

For the universe itself to be Kan, ${hcom}_{U}^{r \to s}$ must produce a type. The complete rule belongs to the packages of convention 218.26. Its load-bearing diagnostic clause converts the tube of type codes into equivalences by backwards coercion and glues them onto the cap. On $φ$ take $(T [s / i], {coe}_{i . T}^{s \to r})$ ; on $r = s$ take $(B, {id}_{B})$ . Writing $U$ for this compatible system, the clause is ${hcom}_{U}^{r \to s} [φ \mapsto i . T] (B) \equiv Glue U (B) .$ Here equip ${coe}_{i . T}^{s \to r}$ with inverse ${coe}_{i . T}^{r \to s}$ and the two filler homotopies witnessing the composites; equip ${id}_{B}$ with the contraction of each singleton fiber. The second component of the system — gluing $B$ along the diagonal cofibration $r = s$ — is what makes the equation hcom-cap hold at the universe; it is precisely here that the Cartesian cofibration $r = s$ is load-bearing, and this step was the discovery that unblocked the Cartesian model [Ang19, ABC^+21].

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

The diagonal component is forced. Without it the naive clause ${hcom}_{U}^{r \to s} [φ \mapsto i . T] (B) \overset{?}{=} Glue [φ \mapsto (T [s / i], {coe}_{i . T}^{s \to r})] B$ does not satisfy hcom-cap: after imposing $r = s$ , its right-hand side remains a Glue type rather than reducing to $B$ . Adding $r = s \mapsto (B, {id}_{B})$ makes that extent total on the diagonal, so $Glue [1 \mapsto (B, {id}_{B})] B \equiv B$ by Glue-form- $1$ . This is exactly hcom-cap.

Example 218.29 — Transporting Boolean negation ¶

Let $not : 2 ≃ 2$ . Equation (V- $coe$ ) gives the annotated closed calculation $\begin{aligned} {coe}_{i . V_{i} (2, 2, not)}^{0 \to 1} (tt) & \equiv {coe}_{j . 2}^{0 \to 1} (not (tt)) & by (V- coe), \\ \equiv not (tt) & by the constant- 2 coercion rule, \\ \equiv ff & by 2 - β . \end{aligned}$ Unlike transport along an opaque univalence axiom, this closed term reduces to a canonical constructor.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Exercise 81.10 ¶

★☆☆ Using the mnemonic of remark 81.24, match the two endpoint equations of primitive $V$ with the corresponding Glue faces. Explain why this boundary comparison does not establish a judgmental equality of type formers, and name the imported Kan package needed to make the comparison internal.

Referenced from 3 locations

Exercise 81.11 ¶

★★☆ Check the coherence of definition 81.22: on $r = 0$ the uniqueness rule asserts $v \equiv {Vin}_{0} (v, {pr}_{1} e v) \equiv v$ , and on $r = 1$ likewise. Show also that the $β$ - and boundary rules for $Vout$ agree on the overlaps $r = 0$ and $r = 1$ with the equations for $Vin$ — i.e. no critical pair of judgmental equalities is ambiguous.

Referenced from 3 locations

Exercise 81.12 ¶

★☆☆ Repeat example 218.29 with $ff$ , tracking the V-coercion, constant- $2$ coercion, and Boolean computation rules. Then explain exactly which first step is unavailable when univalence is postulated as an opaque axiom (definition 65.6).

Referenced from 3 locations

The computational semantics

Evaluation is not stable under dimension substitution: ${loop}_{i}$ is a value, but its face ${loop}_{i} [0 / i] ⟼ base$ . A computational cubical type system therefore relates a program to all of its substituted evaluations. Its inference rules are soundness theorems for that relation.

Definition 81.27 — Cubical programs ¶

The programs are the raw terms of this chapter (two sorts: dimension terms and ordinary terms), with free dimension variables permitted and free term variables excluded, under a deterministic weak-head operational semantics: judgments $M val$ and $M ⟼ M^{'}$ , with $M ⇓ V$ when $M ⟼^{*} V val$ . Representative steps: $\begin{aligned} (λ x . b) a & ⟼ b [a / x], \\ {loop}_{i} [0 / i] = {loop}_{0} & ⟼ base, \\ {coe}_{i . A}^{r \to s} (a) & ⟼ \dots & by the head of A . \end{aligned}$ Here the coercion step first evaluates $A$ under the dimension binder $i$ and then dispatches on its head constructor. Evaluation preserves free dimension variables but is not stable under dimension substitution: ${loop}_{i}$ is a value whose face ${loop}_{i} [0 / i]$ is not.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Definition 81.28 — Judgments as behaviors; schematic ¶

Let $Ψ$ range over dimension contexts and $ψ : Ψ^{'} \to Ψ$ over total dimension substitutions. A cubical type system is a relation $τ (Ψ; A_{0}, B_{0}, φ)$ , between values $A_{0}, B_{0}$ with dimensions in $Ψ$ and binary relations $φ$ on such values, that is symmetric, transitive, and assigns each type a unique relation, and whose value relations are PERs. The need for two substitutions is visible in the evaluation square $A ψ_{1} ψ_{2} ⇓ A_{12}, A ψ_{1} ⇓ A_{1}, A_{1} ψ_{2} ⇓ A_{12}^{'} .$ The two routes need not produce the same syntax, so $A_{12}$ and $A_{12}^{'}$ must belong to the same PER. Write $≐$ for these semantic behavior judgments; it is distinct from the formal equality $\equiv$ . Relative to $τ$ , the judgments are defined:

$A ≐ B type [Ψ]$ holds when for every $ψ_{1} : Ψ_{1} \to Ψ$ and $ψ_{2} : Ψ_{2} \to Ψ_{1}$ there are evaluations $\begin{aligned} A ψ_{1} & ⇓ A_{1}, & A ψ_{1} ψ_{2} & ⇓ A_{12}, & A_{1} ψ_{2} & ⇓ A_{12}^{'}, \\ B ψ_{1} & ⇓ B_{1}, & B ψ_{1} ψ_{2} & ⇓ B_{12}, & B_{1} ψ_{2} & ⇓ B_{12}^{'} . \end{aligned}$ One PER $φ_{ψ_{1} ψ_{2}}$ selected by $τ$ relates all five required pairs $(A_{12}^{'}, A_{12}), (A_{12}, A_{12}^{'}), (B_{12}^{'}, B_{12}), (B_{12}, B_{12}^{'}), (A_{12}, B_{12}) .$ Thus evaluating after two substitutions agrees with substituting into the first value and evaluating again, on each side and across the claimed type equality.
$M ≐ N \in A [Ψ]$ , presupposing $A type [Ψ]$ , holds when every pair of instances $M ψ_{1} ψ_{2}$ , $N ψ_{1} ψ_{2}$ evaluates into the corresponding $φ_{ψ_{1} ψ_{2}}$ , again coherently across further substitution.
$A$ is Kan when the family $φ_{ψ}$ is closed under $coe$ and $hcom$ : the operations of definition 81.7 applied to related data yield related results satisfying the boundary equations up to $≐$ .
Open judgments are defined by functionality: $a ≐ a^{'} \in A [Ψ ∣ Γ]$ means that equal closing instantiations of $Γ$ (themselves defined by induction on $Γ$ ) yield $≐$ -equal elements at every dimension substitution instance. For type families, equal closing instantiations instead yield $≐$ -equal types at every dimension substitution instance.

The double-substitution quantification in (1)–(2) is what replaces the head-expansion discipline of theorem 49.18’s proof: because evaluation and restriction do not commute (definition 81.27), coherence must be imposed on all faces of all instances, not checked once. The five-pair condition is Definition 4.5(1) of [Ang19]; clause (2) above is its element analogue, Definition 4.5(2), and open functionality is Definition 4.5(3–4).

Referenced from 4 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Theorem 81.29 — Existence and soundness ¶

Angiuli’s computational Cartesian calculus $C_{A}$ has a Kan cubical type system constructed as the least fixed point of a monotone operator on candidate type systems. It contains universe hierarchies of pretypes and Kan types closed under $Π$ , $Σ$ , path, $V$ , $2$ , $N$ , $0$ , and the higher-inductive circle, and validates the computational rules stated for that calculus. In particular $C_{A}$ is consistent.

Referenced from 4 locations

Proof of Theorem 81.29 — Existence and soundness

Proof. The construction is imported from Angiuli’s Definitions 4.3–4.10 (candidate judgments and their fixed points), Definition 4.29 (Kan closure), the type-former-by-type-former Rules 4.35–4.104, and Theorem 4.58 (consistency) [Ang19]. Those results construct the monotone operators, prove closure and coherence, and build the universe hierarchy. They discharge the theorem’s imported obligations.

Two representative verifications explain how the imported argument meets the equations displayed in this chapter. First, Boolean coercion evaluates immediately: ${coe}_{i . 2}^{r \to s} (M) ⇓ M$ . If $M$ and $M^{'}$ are related by the Boolean PER, their reducts are related by the same PER; when $r = s$ , the same reduction proves coe-id. On the diagonal $r = s$ , the V-type $hcom$ clause reduces its Glue system to the cap PER, so related caps remain related after composition. These checks illustrate coherent expansion; they do not stand in for the imported fixed-point and universe construction. Consistency is the local corollary of the imported empty-type PER: a closed inhabitant of $0$ would contradict Theorem 4.58. ◻

Remark 81.30 — The meaning-explanation reading ¶

$M ≐ N \in A [Ψ]$ asserts that every dimension instance of $M$ and $N$ evaluates to values related by $A$ ’s PER. A formal typing rule is sound when it preserves this relation. Pretypes omit the Kan-closure clause; Kan types include it, so strict pretypes and univalent Kan types can coexist.

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

This dimension-indexed PER construction refines the meaning-explanation tradition of Martin-Löf, Allen, and Nuprl; its fixed point and universe hierarchy are developed in [Ang19].

Exercise 81.13 ¶

★★☆ Exhibit a program $M$ and substitution $ψ$ with $M val$ but not $M ψ val$ , and a well-typed $M$ where evaluating-then-substituting and substituting-then-evaluating produce syntactically distinct values. Then show, directly from definition 81.28, that in any cubical type system the two results are nevertheless $≐$ -equal elements.

Referenced from 3 locations

Exercise 81.14 ¶

★☆☆ Show that in the empty dimension context the clauses of definition 81.28 collapse to PER semantics of the style used for theorem 49.18: the only $ψ$ are identities, coherence is vacuous, and $M ≐ N \in 2 [\cdot]$ holds iff $M$ and $N$ evaluate to a common canonical boolean.

Referenced from 3 locations

Canonicity and normalization

Theorem 81.31 — Canonicity for cubical type theory ¶

If $M \in 2 [\cdot]$ in Angiuli’s computational Cartesian calculus $C_{A}$ , with the context empty of dimension and term variables, then exactly one of $M ≐ tt \in 2 [\cdot] or M ≐ ff \in 2 [\cdot]$ holds; equivalently, deterministic evaluation of $M$ ends at exactly one Boolean constructor.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Proof of Theorem 81.31 — Canonicity for cubical type theory

Proof. Membership in the Boolean PER means that $M$ evaluates to $tt$ or $ff$ . Determinism gives uniqueness, and consistency separates the two constructors: identifying them would let Boolean elimination inhabit $0$ [Ang19]. ◻

Remark 81.32 — Architecture of the proof ¶

The operational proof reads a closed Boolean from its PER, whose coherence relates evaluation to every face. The normalization proof instead glues computability data to syntax and obtains a recursive normal form; comparing normal forms decides judgmental equality [Ang19, SA21]. Circle canonicity is the corresponding closed-element result [Ang19]: in the empty interval context no valid all-false tube shape can contribute an $hcom$ generator, so every closed computational circle element satisfies $M ≐ base \in S^{1} [\cdot]$ .

Referenced from 2 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Theorem 81.33 — Normalization; Sterling–Angiuli ¶

Let $C_{SA}$ be the universe-free Cartesian cubical calculus of [SA21]: its type formers are $Π$ , $Σ$ , path, $Glue$ , and the higher-inductive circle. Types and terms of $C_{SA}$ in atomic contexts admit a recursive normalization function that is sound and complete for judgmental equality. Here atomic contexts are generated from the empty context by dimension extension $Γ . I$ and typed variable extension $Γ . A$ ; their substitutions are generated by projections, the newest variable, older variables weakened through an extension, and dimension terms. They carry no primitive cofibration-restriction entries. The normal-form presentation is tight: every term has exactly one normal form and normalization is an isomorphism onto normal-form syntax.

Referenced from 5 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Proof of Theorem 81.33 — Normalization; Sterling–Angiuli

Proof. The gluing construction defines $nf (M)$ recursively and proves $nf (M) \equiv M$ . Completeness gives $M \equiv N$ exactly when the normal-form syntax $nf (M) = nf (N)$ , while reflection at stabilized neutrals handles cofibration-restricted contexts. These are Theorem 42, Corollaries 45–46, and Remark 48 of [SA21] for the signature in the statement. ◻

Corollary 81.34 — Decidability ¶

Judgmental equality of well-formed types and terms of $C_{SA}$ is decidable, and its type constructors are injective up to judgmental equality in the admissible sense.

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

Proof of Corollary 81.34 — Decidability

Proof. Compute and compare the unique normal forms from theorem 81.33; their outer constructors also give admissible constructor injectivity . ◻

Remark 81.35 — Stabilized neutrals ¶

The obstruction that delayed theorem 81.33 for years is that cubical neutrality is not absolute. In the base theory a variable-headed term stays neutral under all substitutions of variables for variables (definition 49.14 is stable along renamings); but the cubical neutral $p @ r$ , for a path variable $p$ , ceases to be neutral on the cofibration $(r = 0) \lor (r = 1)$ , where it is judgmentally an endpoint — and in the Cartesian theory even a diagonal substitution $[j / i]$ can awaken a redex, e.g. in ${coe}^{i \to j}$ . The proof therefore indexes each neutral by a cofibration recording its locus of instability, and the reflection map of the normalization model takes as input a neutral together with computability data on that locus — a pairing with no counterpart in the NbE of definition 49.23. Normal and neutral forms are otherwise as in chapter 49, extended by dimension binders, tubes, and systems [SA21].

Referenced from 3 locations

Cubical Type Theory II: Cartesian Cubes and Computation

The normalization theorem covers $C_{SA}$ , not every feature of Cubical Agda, cubicaltt, RedPRL, redtt, cooltt, or yacctt. Each implementation must separately check that its universes, higher inductives, and system-normalization rules preserve conversion. Brunerie’s number, extracted from $π_{4} (S^{3}) ≅ Z / 2 Z$ , is a practical stress test: canonicity predicts a closed numeral while normalization must process large cubical systems.

Exercise 81.15 ¶

★★★ Working only in $C_{SA}$ , use theorem 81.33 and decidability of cofibration entailment to outline a bidirectional type checker extending definition 48.16: what new judgment forms must be checked, and where is cof-case dispatched? Identify the two places where the algorithm invokes the normalization function.

Referenced from 3 locations

Exercise 81.16 ¶

★★☆ Compute the locus of instability, in the sense of remark 81.35, of the terms $p @ i$ , $p @ 0$ , and ${hcom}_{2}^{r \to s} [φ \mapsto i . t] (x)$ for a boolean variable $x$ : on which cofibration does each cease to be variable-blocked, and to what does it then reduce?

Referenced from 3 locations

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 218.17, then complete exercise 218.18.

Exercise 218.17 ¶

★★☆ Instantiate the V-type coercion rule at Boolean negation. Calculate the two endpoint coercions and the composite line, then compare the result with the corresponding Glue transport in the De Morgan system.

Referenced from 4 locations

Exercise 218.18 ¶

★★★ Practical project.cartesian-cofibration-checker Implement in Agda or Kappa finite Cartesian cofibration entailment and system-overlap checking. Preserve truth under all endpoint assignments. Accept diagonal, universal-quantification, and disjunction examples; reject an invalid shape for homogeneous composition and a disagreeing overlap. Mutation test: treat a diagonal as an endpoint equation and ensure the truth-table suite detects the changed entailment.

Referenced from 5 locations

Bibliographic notes

Cartesian cubical type theory has two intertwined sources. The computational line — judgments as behaviors of untyped programs — runs from Martin-Löf’s meaning explanations through Allen’s semantics of Nuprl to the Cartesian cubical programming language of Angiuli, Hou (Favonia), and Harper, consolidated in Angiuli’s dissertation [Ang19], from which section 81.5 is abstracted and where V-types, the valid-shape restriction on compositions, and the strengthened higher-inductive canonicity appear. The proof-theoretic line begins with Coquand’s 2014 note on a Kan operation for Cartesian cubical sets and the Brunerie–Licata formalism, and culminates in the syntax and mechanized cubical-sets model of Angiuli, Brunerie, Coquand, Hou (Favonia), Harper, and Licata [ABC^+21], our source for definition 81.4, definition 81.7, the $Glue$ -based universe, and the comparison of Kan operations; the diagonal cofibration as the enabling ingredient is due to Angiuli–Hou (Favonia)–Harper. The De Morgan counterpoint is Cohen–Coquand–Huber–Mörtberg [CCHM18], with canonicity due to Huber; our comparison follows [ABC^+21] and the textbook treatment of Angiuli and Gratzer [AG26], whose “programming exercises” shaped section 81.2. Normalization for cubical type theory is Sterling–Angiuli [SA21], built on synthetic Tait computability [Ste21] and the gluing reformulation of computability [Coq19]; Gratzer’s dissertation extends the method to modal settings [Gra23], and Abel’s habilitation [Abe13] develops the non-cubical NbE refined here. The universe-path and transport computation exhibited here is the computational ingredient associated with the univalence axiom of [Uni13]; full book univalence (cf. chapter 65) is not claimed.