In axiomatic HoTT, transport along 𝗎𝖺(𝑒) has no head rule. Cubical type theory represents a path 𝑎=𝑏 by a term 𝑝(𝑖) with 𝑝(0)≡𝑎 and 𝑝(1)≡𝑏; transport then computes by the Kan operations of the family 𝑝(𝑖). We use De Morgan cubes, and the 𝖦𝗅𝗎𝖾 former turns equivalences into computational paths in the universe.
The interval
The interval enters the syntax not as a type but as a new sort of context entry; its elements form an algebra of formal points of [0,1].
Fix a countably infinite set of names (dimension variables) 𝑖,𝑗,𝑘,…, disjoint from the term variables of definition 26.1. The interval 𝕀 is the free De Morgan algebra on the names: the set of expressions 𝑟,𝑠::=0∣1∣𝑖∣1−𝑟∣𝑟∧𝑠∣𝑟∨𝑠 taken modulo the laws of a bounded distributive lattice with bottom 0, top 1, meet ∧, join ∨, together with the laws making 1−(−) a De Morgan involution: 1−0=1,1−1=0,1−(1−𝑟)=𝑟,1−(𝑟∨𝑠)=(1−𝑟)∧(1−𝑠),1−(𝑟∧𝑠)=(1−𝑟)∨(1−𝑠). The intended reading is 𝑟∧𝑠=min(𝑟,𝑠), 𝑟∨𝑠=max(𝑟,𝑠), 1−𝑟 the reversal of the unit interval.
As a bounded distributive lattice, 𝕀 is free on the set of literals{𝑖,1−𝑖∣𝑖aname}, with no relations between 𝑖 and 1−𝑖. Consequently every 𝑟∈𝕀 equals a finite join of finite meets of literals, and equality in 𝕀 is decidable.
Proof of Proposition 80.2 — Normal form; decidability
Proof. The De Morgan laws push every occurrence of 1−(−) down to the generators, so each element is a lattice polynomial in literals; distributivity yields the disjunctive normal form. For decidability it suffices to decide 𝑟≤𝑠 on normal forms: in a free distributive lattice a meet 𝑚 of generators satisfies 𝑚≤⋁𝑙𝑚𝑙 if and only if 𝑚≤𝑚𝑙 for some 𝑙, i.e. 𝑚𝑙 uses only literals of 𝑚 for some 𝑙. For the nontrivial direction, if no 𝑚𝑙 is contained in 𝑚, assign every literal of 𝑚 the value 1 and, for each 𝑚𝑙, choose one additional literal and assign it 0; freeness extends this to a lattice valuation separating the two sides. Sorting each meet, deleting absorbed meets, and sorting the resulting antichain therefore produces a canonical finite normal form, whose syntactic comparison decides equality. ◻
In 𝕀 neither 𝑟∧(1−𝑟)=0 nor 𝑟∨(1−𝑟)=1 holds in general. By freeness, any valuation of names in the De Morgan algebra [0,1] extends to a homomorphism 𝕀→[0,1]; the valuation 𝑖↦12 sends 𝑖∧(1−𝑖) to 12≠0 (exercise 80.2). Geometrically: a point of the square need not lie on its boundary.
A dimension context is a context that may also declare interval names. As always, the notation Γ,𝑖:𝕀 carries the freshness condition 𝑖∉dom(Γ), cf. definition 26.22):
Γ𝖼𝗍𝗑
Γ,𝑖:𝕀𝖼𝗍𝗑
Ctx-Dim
The judgment Γ⊢𝑟:𝕀 holds when Γ𝖼𝗍𝗑 and every name occurring in 𝑟 is declared in Γ; the judgment Γ⊢𝑟≡𝑠:𝕀 holds when in addition 𝑟=𝑠 in the algebra 𝕀. Both are defined judgments of the metatheory, not inductively generated by new rules.
The dimension substitution𝑒[𝑟/𝑖] substitutes the interval expression 𝑟 for the dimension name 𝑖; 𝑒[0/𝑖] and 𝑒[1/𝑖] are its two faces. By contrast, 𝐴[𝜑↦𝑢] is the type 𝐴 with the boundary equation 𝑎=𝑢 imposed under the face formula 𝜑.
A judgment in a context declaring 𝑛 names is an 𝑛-cube: a type Γ,𝑖:𝕀⊢𝐴𝗍𝗒𝗉𝖾 is a line of types, a term Γ,𝑖:𝕀,𝑗:𝕀⊢𝑡:𝐴 a square of elements, and so on. The interval operations act by substitution:
No rule makes 𝕀 a type: it has no code in U, cannot be quantified over by Π or Σ, and has no eliminator — one cannot branch on whether 𝑟=0 or 𝑟=1, and remark 80.3 shows these cases are not exhaustive. Names are bound only by the dedicated binders ⟨𝑖⟩(−) (§ 80.2) and 𝖼𝗈𝗆𝗉𝑖 (§ 80.4). Because dimensions are substituted only by homomorphisms 𝕀→𝕀, interval and face equations remain valid after [𝑟/𝑖]; in particular the endpoint equations of a path remain true.
Variants of the algebra. This chapter uses the free De Morgan algebra, whose finite-name fragments are finite and decidable. The Cartesian calculus drops reversal and connections and postulates different Kan operations [ABC^+21]. The intermediate Kleene variant is compared in [CCHM18].
★☆☆ Show from definition 80.1 that 1−(−):𝕀→𝕀 is an isomorphism onto the order-dual of 𝕀 (it exchanges ∧ with ∨ and 0 with 1), and that it is determined uniquely by its action on names.
★★★ Verify that [0,1] with min, max, 𝑥↦1−𝑥 is a De Morgan algebra, and that every function from names to [0,1] extends uniquely to a homomorphism 𝕀→[0,1]. Conclude the claims of remark 80.3, and exhibit 𝑟≠𝑠 in 𝕀 whose [0,1]-interpretations agree (so the extension of proposition 80.2 to Kleene algebras is a genuine quotient).
★★★ Complete the proof of proposition 80.2: prove the primality of meets of generators in a free bounded distributive lattice, and describe the resulting decision procedure for 𝑟=𝑠 in 𝕀.
Cubical type theory has the type formers 𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏) and, for a line of types 𝑖.𝐴 (the name 𝑖 bound in 𝐴), the dependent path type𝖯𝖺𝗍𝗁𝖯𝑖.𝐴(𝑎0,𝑎1). Path abstraction ⟨𝑖⟩𝑡 binds 𝑖 in 𝑡; path application 𝑡𝑟 applies 𝑡 to 𝑟∈𝕀. The rules (premises compressed per convention 26.14; the congruence and substitution rules of definition 26.22 extend to the new formers):
Γ⊢𝐴𝗍𝗒𝗉𝖾Γ⊢𝑎:𝐴Γ⊢𝑏:𝐴
Γ⊢𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏)𝗍𝗒𝗉𝖾
Path-form
Γ,𝑖:𝕀⊢𝑡:𝐴
Γ⊢⟨𝑖⟩𝑡:𝖯𝖺𝗍𝗁𝐴(𝑡[0/𝑖],𝑡[1/𝑖])
Path-intro
Γ⊢𝑡:𝖯𝖺𝗍𝗁𝐴(𝑢0,𝑢1)Γ⊢𝑟:𝕀
Γ⊢𝑡𝑟:𝐴
Path-elim
Γ,𝑖:𝕀⊢𝑡:𝐴Γ⊢𝑟:𝕀
Γ⊢(⟨𝑖⟩𝑡)𝑟≡𝑡[𝑟/𝑖]:𝐴
Path-β
Γ⊢𝑡:𝖯𝖺𝗍𝗁𝐴(𝑢0,𝑢1)
Γ⊢𝑡0≡𝑢0:𝐴
Path-_0
Γ⊢𝑡:𝖯𝖺𝗍𝗁𝐴(𝑢0,𝑢1)
Γ⊢𝑡1≡𝑢1:𝐴
Path-_1
Γ,𝑖:𝕀⊢𝑡𝑖≡𝑢𝑖:𝐴
Γ⊢𝑡≡𝑢:𝖯𝖺𝗍𝗁𝐴(𝑢0,𝑢1)
Path-η
For the dependent version, with Γ,𝑖:𝕀⊢𝐴𝗍𝗒𝗉𝖾:
Γ,𝑖:𝕀⊢𝐴𝗍𝗒𝗉𝖾Γ⊢𝑎0:𝐴[0/𝑖]Γ⊢𝑎1:𝐴[1/𝑖]
Γ⊢𝖯𝖺𝗍𝗁𝖯𝑖.𝐴(𝑎0,𝑎1)𝗍𝗒𝗉𝖾
PathP-form
Γ,𝑖:𝕀⊢𝑡:𝐴
Γ⊢⟨𝑖⟩𝑡:𝖯𝖺𝗍𝗁𝖯𝑖.𝐴(𝑡[0/𝑖],𝑡[1/𝑖])
PathP-intro
Γ⊢𝑝:𝖯𝖺𝗍𝗁𝖯𝑖.𝐴(𝑎0,𝑎1)Γ⊢𝑟:𝕀
Γ⊢𝑝𝑟:𝐴[𝑟/𝑖]
PathP-elim
with 𝛽, 𝜕 and 𝜂 rules exactly as for 𝖯𝖺𝗍𝗁 (endpoints at the types 𝐴[0/𝑖], 𝐴[1/𝑖]). When 𝑖 is not free in 𝐴, we identify 𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏)≡𝖯𝖺𝗍𝗁𝖯𝑖.𝐴(𝑎,𝑏); only the dependent former is primitive.
In context Γ,𝑖:𝕀,𝑗:𝕀 the terms 𝑝(𝑖∧𝑗) and 𝑝(𝑖∨𝑗) are squares: DiagramDiagram (horizontal direction 𝑖, vertical 𝑗; unlabeled equalities are constant paths). For instance the four faces of 𝑝(𝑖∧𝑗) are 𝑝(𝑖∧0)≡𝑝0≡𝑎 (bottom), 𝑝𝑖 (top), 𝑎 (left), 𝑝𝑗 (right). Connections manufacture squares whose boundary mixes 𝑝 with constant paths — the key device below.
Let Γ⊢𝑝:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏). Then 𝜃𝑝:=⟨𝑖⟩(𝑝𝑖,⟨𝑗⟩𝑝(𝑖∧𝑗))inhabits𝖯𝖺𝗍𝗁∑𝑥:𝐴𝖯𝖺𝗍𝗁𝐴(𝑎,𝑥)((𝑎,𝗋𝖾𝖿𝗅𝑎),(𝑏,𝑝)). Indeed at 𝑖=0 the value is (𝑝0,⟨𝑗⟩𝑝0)≡(𝑎,𝗋𝖾𝖿𝗅𝑎), and at 𝑖=1 it is (𝑝1,⟨𝑗⟩𝑝𝑗)≡(𝑏,𝑝), the last step by Path-𝜂. (Compare the corresponding construction for 𝖨𝖽 in chapter 30, which needs 𝖩; here two connections suffice.)
The rules of definition 80.8 give maps into path types and evaluation at points of 𝕀, but no transport: nothing yet carries an element of 𝐵[𝑎/𝑥] to 𝐵[𝑏/𝑥] along 𝑝:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏), and the eliminator 𝖩 of definition 30.1 is not derivable. In the fourfold order of convention 27.1 the elimination form present (Path-elim) is that of a function type on 𝕀, not that of an identity type. The missing structure is supplied uniformly for every type by Kan composition (§ 80.4).
★★☆ Write out the equality derivations showing Γ⊢𝖺𝗉𝑓(𝑝):𝖯𝖺𝗍𝗁𝐵(𝑓𝑎,𝑓𝑏) in construction 80.10, naming each rule. Then show that 𝖺𝗉 is judgmentally functorial: 𝖺𝗉𝑔(𝖺𝗉𝑓(𝑝))≡𝖺𝗉𝑔∘𝑓(𝑝) and 𝖺𝗉𝜆𝑥.𝑥(𝑝)≡𝑝. Contrast with the merely propositional functoriality available for 𝖨𝖽 in chapter 30.
★★☆ Compute the four faces of 𝑝(𝑖∨𝑗) in example 80.11. Then show ⟨𝑖⟩𝑝(𝑖∨(1−𝑖)) inhabits 𝖯𝖺𝗍𝗁𝐴(𝑏,𝑏), and explain why it is not judgmentally equal to 𝗋𝖾𝖿𝗅𝑏 (use proposition 80.2).
★★☆ Verify the typing of 𝖺𝗉𝖽 in construction 80.10(3): exhibit the line of types over which it is a dependent path, and check both endpoint equalities. Show also that over a constant line, PathP-* specializes rule-by-rule to Path-*.
To state the composition operation we must speak of partial types and elements — data given only on a union of faces of a cube. The shapes of partiality are recorded by a lattice of formulas.
The face lattice𝔽 is the distributive lattice generated by the symbols (𝑖=0) and (𝑖=1), for 𝑖 a name, subject to (𝑖=0)∧(𝑖=1)=0𝔽. Its elements, the face formulas, are generated by 𝜑,𝜓::=0𝔽∣1𝔽∣(𝑖=0)∣(𝑖=1)∣𝜑∧𝜓∣𝜑∨𝜓. There is a lattice map 𝕀→𝔽, written 𝑟↦(𝑟=1), sending 𝑖↦(𝑖=1) and 1−𝑖↦(𝑖=0); we set (𝑟=0):=(1−𝑟=1). Every 𝜑 is the join of the irreducible elements below it, an irreducible element being a conjunction of atoms in distinct names; equality in 𝔽 is decidable by distributing to DNF, deleting monomials containing both (𝑖=0) and (𝑖=1), and comparing the remaining finite antichains. Substitution 𝜑[𝑟/𝑖] acts by (𝑖=1)↦(𝑟=1), (𝑖=0)↦(𝑟=0). The judgment Γ⊢𝜑:𝔽 holds when Γ𝖼𝗍𝗑 and all names of 𝜑 are declared in Γ.
In Γ,𝜑 add the equation 𝜑=1𝔽. Thus Γ,(𝑖=0)⊢𝑟≡𝑠:𝕀 holds exactly when Γ⊢𝑟[0/𝑖]≡𝑠[0/𝑖]:𝕀 does. A join of faces imposes the intersection of their congruences, and Γ,0𝔽 validates every equality. A substitution 𝜎:Δ→(Γ,𝜑) consists of 𝜎:Δ→Γ together with Δ⊢𝜑[𝜎]≡1𝔽:𝔽.
The following are admissible. Restriction by 1𝔽 changes nothing (Γ,1𝔽⊢J iff Γ⊢J); if 𝜑≤𝜓 in 𝔽 and Γ,𝜓⊢J then Γ,𝜑⊢J; iterated restriction is conjunction (Γ,𝜑,𝜓⊢J iff Γ,𝜑∧𝜓⊢J); and if 𝜑 does not mention 𝑖 then Γ,𝑖:𝕀,𝜑⊢J iff Γ,𝜑,𝑖:𝕀⊢J.
Proof. Each clause is induced by a substitution of restricted contexts. For 1𝔽 the identity substitution works in both directions. If 𝜑≤𝜓, the inclusion Γ,𝜑→Γ,𝜓 is well formed because 𝜓=1𝔽 follows from 𝜑=1𝔽; substitution of the given derivation along it gives the second clause. The contexts Γ,𝜑,𝜓 and Γ,𝜑∧𝜓 impose the same congruence, so their identity lists define inverse substitutions. Finally, when 𝑖 does not occur in 𝜑, the identity assignments define substitutions (Γ,𝑖:𝕀,𝜑)→(Γ,𝜑,𝑖:𝕀) and back; both satisfy the face premise because 𝜑 does not contain 𝑖. Substituting along these two maps proves the exchange equivalence. ◻
For each name 𝑖 let ∀𝑖:𝔽→𝔽 be the lattice map sending (𝑖=0) and (𝑖=1) to 0𝔽 and fixing the other generators. Then for 𝜓 not mentioning 𝑖: 𝜓≤𝜑 iff 𝜓≤∀𝑖.𝜑. Moreover 𝜑=(∀𝑖.𝜑)∨(𝜑∧(𝑖=0))=∨(𝜑∧(𝑖=1)),𝜑∧(𝑖=0)≤𝜑[0/𝑖],𝜑∧(𝑖=1)≤𝜑[1/𝑖].
Proof. Write 𝜑 as a join of irreducibles (definition 80.14). An irreducible 𝑐 either does not mention 𝑖 — then ∀𝑖.𝑐=𝑐 — or contains exactly one atom in 𝑖, say (𝑖=0); then ∀𝑖.𝑐=0𝔽 and 𝑐=𝑐∧(𝑖=0)≤𝜑∧(𝑖=0). This proves the decomposition, each disjunct being ≤𝜑 because ∀𝑖.𝜑≤𝜑 on irreducibles. For the adjunction, if 𝜓 is independent of 𝑖, every irreducible summand of 𝜓 is also independent of 𝑖; hence 𝜓≤𝜑 holds exactly when those summands occur among the 𝑖-free summands retained by ∀𝑖.𝜑. The two face inequalities follow by substituting 0 and 1 into the summands that contain the corresponding atom. ◻
A two-face system [𝜑0↦𝑡0,𝜑1↦𝑡1] is defined when 𝑡0=𝑡1 on 𝜑0∧𝜑1; it is total when 𝜑0∨𝜑1=1𝔽. A system is a formal amalgam [𝜑1↦𝑡1,…,𝜑𝑛↦𝑡𝑛] of terms (or types) given on faces; 𝑛=0 is allowed, giving the empty system []. The rules below carry the common side condition Γ⊢𝜑1∨⋯∨𝜑𝑛≡1𝔽:𝔽 (for 𝑛=0: Γ⊢0𝔽≡1𝔽:𝔽, so the empty system lives only in inconsistently restricted contexts):
Let Γ⊢𝐴𝗍𝗒𝗉𝖾 and Γ,𝜑⊢𝑢:𝐴; we call 𝑢 a partial element of 𝐴 of extent 𝜑. The notation Γ⊢𝑎:𝐴[𝜑↦𝑢]abbreviatesΓ⊢𝑎:𝐴andΓ,𝜑⊢𝑎≡𝑢:𝐴, read: 𝑎extends the partial element 𝑢. With several faces, 𝐴[𝜑1↦𝑢1,…,𝜑𝑘↦𝑢𝑘] imposes one constraint per listed face: 𝑎=𝑢𝑘 in Γ,𝜑𝑘 for every 𝑘. The notation [] is the empty list of constraints.
Let Γ⊢𝐴𝗍𝗒𝗉𝖾 and 𝜑=(𝑖=0)∨(𝑖=1) in Γ,𝑖:𝕀. A partial element of extent 𝜑 is, by Sys-glob and definition 80.15, exactly a pair of elements 𝑎0,𝑎1:𝐴; an element of 𝐴[(𝑖=0)↦𝑎0,(𝑖=1)↦𝑎1] in Γ,𝑖:𝕀 is exactly a path from 𝑎0 to 𝑎1, up to the abstraction of Path-intro.
★★★ Establish the disjunctive normal form for 𝔽 claimed in definition 80.14 (note the relation (𝑖=0)∧(𝑖=1)=0𝔽 kills monomials mentioning both atoms of one name) and derive a decision procedure for 𝜑=𝜓 in 𝔽.
★☆☆ Show that in a context Γ with Γ⊢0𝔽≡1𝔽:𝔽, every type is inhabited (by the empty system) and every judgmental equality holds. Why does this not threaten consistency? (Compare the role of 𝟎-elimination, definition 28.7.)
Being extensible — convention 80.19 — is the cubical generalization of being connected by a path; the composition operation asserts, with a term, that extensibility is preserved along lines of types. It is the entire Kan structure of the theory.
For every line of types there is an operation 𝖼𝗈𝗆𝗉𝑖, binding the name 𝑖 in its type and system arguments:
Γ⊢𝜑:𝔽Γ,𝑖:𝕀⊢𝐴𝗍𝗒𝗉𝖾Γ,𝜑,𝑖:𝕀⊢𝑢:𝐴Γ⊢𝑎0:𝐴[0/𝑖][𝜑↦𝑢[0/𝑖]]
Γ⊢𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝑢]𝑎0:𝐴[1/𝑖][𝜑↦𝑢[1/𝑖]]
Comp
subject to the judgmental equality (a strengthening of the boundary constraint in the conclusion): Γ⊢𝖼𝗈𝗆𝗉𝑖𝐴[1𝔽↦𝑢]𝑎0≡𝑢[1/𝑖]:𝐴[1/𝑖], and to the substitution clause extending definition 26.1: for a substitution 𝜎 into Γ and 𝑗 fresh, (𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝑢]𝑎0)[𝜎]=𝖼𝗈𝗆𝗉𝑗(𝐴[𝜎,𝑗/𝑖])[𝜑[𝜎]↦𝑢[𝜎,𝑗/𝑖]](𝑎0[𝜎]). The judgmental equalities computing 𝖼𝗈𝗆𝗉𝑖𝐴 by cases on the shape of 𝐴 are listed in definition 80.25 and §§ 80.5–80.6.
Read 𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝑢]𝑎0 as: an open box in the line 𝐴, with sides 𝑢 prescribed over the extent 𝜑 for all 𝑖, and bottom 𝑎0 at 𝑖=0 agreeing with the sides; the composition is the missing lid at 𝑖=1, agreeing with the sides. The substitution clause is the uniformity of the operation: lids are computed compatibly with all faces, degeneracies, connections and reversals — the feature distinguishing the constructive cubical models from classical Kan simplicial sets. When 𝜑 is the boundary formula ⋁𝑘(𝑖𝑘=0)∨(𝑖𝑘=1) of the names of Γ, one recovers the classical Kan box-filling condition.
Let Γ⊢𝑝:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏) and Γ⊢𝑞:𝖯𝖺𝗍𝗁𝐴(𝑏,𝑐). Then 𝑝⋅𝑞:=⟨𝑖⟩𝖼𝗈𝗆𝗉𝑗𝐴[(𝑖=0)↦𝑎,(𝑖=1)↦𝑞𝑗](𝑝𝑖):𝖯𝖺𝗍𝗁𝐴(𝑎,𝑐), the lid of the square (direction 𝑖 horizontal, 𝑗 vertical): Diagram At 𝑖=0 the system’s first branch has extent 1𝔽, so the composite is 𝑎; at 𝑖=1 it is 𝑞1≡𝑐. The groupoid laws of theorem 30.20 hold for ⋅ up to 𝖯𝖺𝗍𝗁, as the box calculation below shows.
With the data of Comp and 𝑗 fresh, define in Γ,𝑖:𝕀𝖿𝗂𝗅𝗅𝑖𝐴[𝜑↦𝑢]𝑎0:=𝖼𝗈𝗆𝗉𝑗(𝐴[𝑖∧𝑗/𝑖])[𝜑↦𝑢[𝑖∧𝑗/𝑖],(𝑖=0)↦𝑎0]𝑎0. The connection 𝑖∧𝑗 replays the composition only up to level 𝑖; writing 𝑣 for the filler, one derives Γ⊢𝑣[0/𝑖]≡𝑎0:𝐴[0/𝑖],Γ⊢𝑣[1/𝑖]≡𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝑢]𝑎0:𝐴[1/𝑖],Γ,𝜑,𝑖:𝕀⊢𝑣≡𝑢:𝐴. Thus not only the lid but the interior of an open box is constructible by the following direct substitutions: 𝑣[0/𝑖]0∧𝑗=0;𝑡ℎ𝑒(𝑖=0)𝑓𝑎𝑐𝑒𝑖𝑠𝑡𝑜𝑡𝑎𝑙=𝑎0,𝑣[1/𝑖]1∧𝑗=𝑗;𝑡ℎ𝑒(𝑖=0)𝑓𝑎𝑐𝑒𝑖𝑠𝑒𝑚𝑝𝑡𝑦=𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝑢]𝑎0,𝑣|𝜑𝐶𝑜𝑚𝑝−𝑓𝑎𝑐𝑒=𝑢[𝑖∧1/𝑖]≡𝑢. Note that 𝖿𝗂𝗅𝗅𝑖 does not bind 𝑖: the filler is a line in 𝑖.
For each type former of the frozen base Π,Σ,ℕ,𝟐,𝟎,𝟏,+,𝖯𝖺𝗍𝗁,𝖯𝖺𝗍𝗁𝖯, 𝖼𝗈𝗆𝗉 has the following canonical-head judgmental equalities. Together with construction 80.38, definition 80.41, this list is the exact computation contract used in this chapter. A composition whose partial system has no uniform constructor head is neutral; the rules do not inspect a face formula to choose a constructor. Throughout, Γ,𝜑,𝑖:𝕀⊢𝑢:𝐶 and Γ⊢𝑐0:𝐶[0/𝑖][𝜑↦𝑢[0/𝑖]] are the data of Comp at the line 𝐶.
Dependent products, 𝐶≡∏𝑥:𝐴𝐵: given Γ⊢𝑎1:𝐴[1/𝑖], let 𝑤:=𝖿𝗂𝗅𝗅𝑖(𝐴[1−𝑖/𝑖])[]𝑎1(inΓ,𝑖:𝕀),𝑣:=𝑤[1−𝑖/𝑖](so𝑣[1/𝑖]≡𝑎1), a line in 𝐴 ending at 𝑎1; then put 𝐷:=𝐵[𝑣/𝑥], 𝑢𝑣:=𝑢𝑣, and 𝑑0:=𝑐0(𝑣[0/𝑖]). Then Γ⊢(𝖼𝗈𝗆𝗉𝑖𝐶[𝜑↦𝑢]𝑐0)𝑎1≡𝖼𝗈𝗆𝗉𝑖𝐷[𝜑↦𝑢𝑣]𝑑0:𝐷[1/𝑖].
Dependent sums, 𝐶≡∑𝑥:𝐴𝐵: let 𝑢1:=𝗉𝗋1(𝑢), 𝑢2:=𝗉𝗋2(𝑢), 𝑎0:=𝗉𝗋1(𝑐0), and 𝑏0:=𝗉𝗋2(𝑐0). Then let 𝑎:=𝖿𝗂𝗅𝗅𝑖𝐴[𝜑↦𝑢1]𝑎0,𝑐1:=𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝑢1]𝑎0,𝑐2:=𝖼𝗈𝗆𝗉𝑖(𝐵[𝑎/𝑥])[𝜑↦𝑢2]𝑏0. Then Γ⊢𝖼𝗈𝗆𝗉𝑖𝐶[𝜑↦𝑢]𝑐0≡(𝑐1,𝑐2):𝐶[1/𝑖].
Natural numbers, 𝐶≡ℕ (constant in 𝑖): put 𝑛1:=𝖼𝗈𝗆𝗉𝑖ℕ[𝜑↦𝑛]𝑛0. Recursion gives Γ⊢𝖼𝗈𝗆𝗉𝑖ℕ[𝜑↦𝟢]𝟢≡𝟢:ℕ,Γ⊢𝖼𝗈𝗆𝗉𝑖ℕ[𝜑↦𝗌𝗎𝖼(𝑛)](𝗌𝗎𝖼(𝑛0))≡𝗌𝗎𝖼(𝑛1):ℕ.
Finite base types and coproducts: the canonical-head rules are 𝖼𝗈𝗆𝗉𝑖𝟐[𝜑↦𝗍𝗍]𝗍𝗍≡𝗍𝗍,𝖼𝗈𝗆𝗉𝑖𝟐[𝜑↦𝖿𝖿]𝖿𝖿≡𝖿𝖿,𝖼𝗈𝗆𝗉𝑖𝟏[𝜑↦⋆]⋆≡⋆. For a coproduct put 𝑎1:=𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝑢]𝑎0,𝑐1:=𝖼𝗈𝗆𝗉𝑖𝐶[𝜑↦𝑢]𝑐0. Its two canonical-head clauses are 𝖼𝗈𝗆𝗉𝑖(𝐴+𝐶)[𝜑↦𝗂𝗇𝗅(𝑢)]𝗂𝗇𝗅(𝑎0)≡𝗂𝗇𝗅(𝑎1),𝖼𝗈𝗆𝗉𝑖(𝐴+𝐶)[𝜑↦𝗂𝗇𝗋(𝑢)]𝗂𝗇𝗋(𝑐0)≡𝗂𝗇𝗋(𝑐1). There is no canonical introduction case for 𝟎. Mixed Boolean or coproduct systems and compositions on variables remain neutral; the normal-form grammar declares each such expression neutral.
Path types, 𝐶≡𝖯𝖺𝗍𝗁𝐴(𝑣0,𝑣1) (all of 𝐴,𝑣0,𝑣1 may depend on 𝑖): for 𝑗 fresh, put 𝑤𝑗:=[𝜑↦𝑢𝑗,(𝑗=0)↦𝑣0,(𝑗=1)↦𝑣1],𝑑𝑗:=𝖼𝗈𝗆𝗉𝑖𝐴𝑤𝑗(𝑐0𝑗). Then Γ⊢𝖼𝗈𝗆𝗉𝑖𝐶[𝜑↦𝑢]𝑐0≡⟨𝑗⟩𝑑𝑗:𝐶[1/𝑖]. For 𝐶≡𝖯𝖺𝗍𝗁𝖯(𝑗.𝐴,𝑣0,𝑣1), the same displayed equation is used with 𝐴 allowed to depend on 𝑗; this is the complete 𝖯𝖺𝗍𝗁𝖯 clause. The clauses for 𝖦𝗅𝗎𝖾 and U are construction 80.38 and definition 80.41.
Composition with the empty constraint is transport along a line of types: for Γ,𝑖:𝕀⊢𝐴𝗍𝗒𝗉𝖾 and Γ⊢𝑎:𝐴[0/𝑖], 𝗍𝗋𝖺𝗇𝗌𝗉𝑖𝐴𝑎:=𝖼𝗈𝗆𝗉𝑖𝐴[]𝑎:𝐴[1/𝑖], and ⟨𝑖⟩𝖿𝗂𝗅𝗅𝑖𝐴[]𝑎 is a dependent path 𝖯𝖺𝗍𝗁𝖯𝑖.𝐴(𝑎,𝗍𝗋𝖺𝗇𝗌𝗉𝑖𝐴𝑎) connecting 𝑎 to its transport.
If 𝑖 is not free in 𝐴, the equality 𝗍𝗋𝖺𝗇𝗌𝗉𝑖𝐴𝑎≡𝑎 is not a rule of the theory: it fails in the intended model ([CCHM18], App. C, exhibits the geometric obstruction), and adding it naively breaks the uniformity of definition 80.21. Transport over a degenerate line is only path-equal to the identity (construction 80.26). This is the price of the cubical reading; its consequence for the eliminator 𝖩 appears in theorem 80.28.
Let Γ⊢𝐴𝗍𝗒𝗉𝖾, Γ⊢𝑎:𝐴 and Γ,𝑥:𝐴,𝛼:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑥)⊢𝐶𝗍𝗒𝗉𝖾. For all Γ⊢𝑑:𝐶[𝑎/𝑥,𝗋𝖾𝖿𝗅𝑎/𝛼], Γ⊢𝑏:𝐴 and Γ⊢𝑝:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏) there is a term Γ⊢𝖩𝖯𝖺𝗍𝗁(𝑑;𝑝):𝐶[𝑏/𝑥,𝑝/𝛼], and the computation rule of Id-comp holds up to a path: 𝖯𝖺𝗍𝗁𝐶[𝑎/𝑥,𝗋𝖾𝖿𝗅𝑎/𝛼](𝖩𝖯𝖺𝗍𝗁(𝑑;𝗋𝖾𝖿𝗅𝑎),𝑑) is inhabited.
Proof. Let 𝜃𝑝 be the singleton path of construction 80.12 and put 𝖩𝖯𝖺𝗍𝗁(𝑑;𝑝):=𝗍𝗋𝖺𝗇𝗌𝗉𝑖(𝐶[𝗉𝗋1(𝜃𝑝𝑖)/𝑥,𝗉𝗋2(𝜃𝑝𝑖)/𝛼])𝑑. The line transports over is 𝐶 pulled back along 𝜃𝑝; its faces are 𝐶[𝑎/𝑥,𝗋𝖾𝖿𝗅𝑎/𝛼] at 𝑖=0 and 𝐶[𝑏/𝑥,𝑝/𝛼] at 𝑖=1 by the endpoint computations in construction 80.12, so the transport has the stated type. For the computation rule: 𝜃𝗋𝖾𝖿𝗅𝑎≡⟨𝑖⟩(𝑎,𝗋𝖾𝖿𝗅𝑎) is constant, so 𝖩𝖯𝖺𝗍𝗁(𝑑;𝗋𝖾𝖿𝗅𝑎)≡𝗍𝗋𝖺𝗇𝗌𝗉𝑖𝐶′𝑑 with 𝐶′:=𝐶[𝑎/𝑥,𝗋𝖾𝖿𝗅𝑎/𝛼] degenerate in 𝑖; the required path is the inverse (construction 80.10) of the filler path of construction 80.26. By remark 80.27 the equality is in general not judgmental. ◻
Proof of Proposition 217.29 — Cubical groupoid laws
Proof. Use the derived eliminator of theorem 80.28 in the ordinary path-induction proofs of the five groupoid laws. The reflexivity cases are not judgmental because regularity fails, but construction 80.24 gives them. For example, put ℎ(𝑘,𝑖):=𝖿𝗂𝗅𝗅𝑘𝐴[(𝑖=0)↦𝑎,(𝑖=1)↦𝑎]𝑎. Then ℎ(0,𝑖)≡𝑎, while ℎ(1,𝑖)≡(𝗋𝖾𝖿𝗅𝑎⋅𝗋𝖾𝖿𝗅𝑎)(𝑖); its 𝑖=0,1 faces are 𝑎. Thus ⟨𝑘⟩⟨𝑖⟩ℎ(1−𝑘,𝑖):𝖯𝖺𝗍𝗁𝖯𝖺𝗍𝗁𝐴(𝑎,𝑎)(𝗋𝖾𝖿𝗅𝑎⋅𝗋𝖾𝖿𝗅𝑎,𝗋𝖾𝖿𝗅𝑎) is the reflexivity case for the right-unit law. The same filler, with the two side branches exchanged, gives the left-unit base case. Path elimination on 𝑝 propagates these terms to arbitrary paths. The two inverse laws follow by path elimination on 𝑝, with the same base filler; associativity follows by three path eliminations, and in the doubly reflexive base its two parenthesizations are joined through 𝗋𝖾𝖿𝗅𝑎 by the unit paths just constructed. Every displayed 𝖿𝗂𝗅𝗅 has a bottom and side system and computes its lid. ◻
Let Γ⊢𝐴𝗍𝗒𝗉𝖾, Γ,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾 and 𝑓,𝑔:∏𝑥:𝐴𝐵. The terms 𝖿𝗎𝗇𝖾𝗑𝗍(𝑝):=⟨𝑖⟩𝜆𝑥.𝑝𝑥𝑖and𝗁𝖺𝗉𝗉𝗅𝗒(𝑞):=𝜆𝑥.⟨𝑖⟩𝑞𝑖𝑥 are well typed, 𝖿𝗎𝗇𝖾𝗑𝗍:∏𝑥:𝐴𝖯𝖺𝗍𝗁𝐵(𝑓𝑥,𝑔𝑥)⟶𝖯𝖺𝗍𝗁∏𝑥:𝐴𝐵(𝑓,𝑔),𝗁𝖺𝗉𝗉𝗅𝗒:𝖯𝖺𝗍𝗁∏𝑥:𝐴𝐵(𝑓,𝑔)⟶∏𝑥:𝐴𝖯𝖺𝗍𝗁𝐵(𝑓𝑥,𝑔𝑥), and they are judgmentally mutually inverse: 𝗁𝖺𝗉𝗉𝗅𝗒(𝖿𝗎𝗇𝖾𝗑𝗍(𝑝))≡𝑝 and 𝖿𝗎𝗇𝖾𝗑𝗍(𝗁𝖺𝗉𝗉𝗅𝗒(𝑞))≡𝑞.
Proof of Theorem 80.29 — Function extensionality, judgmental
Proof. Typing of 𝖿𝗎𝗇𝖾𝗑𝗍(𝑝): in Γ,𝑖:𝕀 we have 𝜆𝑥.𝑝𝑥𝑖:∏𝑥:𝐴𝐵; its face at 0 is 𝜆𝑥.𝑝𝑥0≡𝜆𝑥.𝑓𝑥≡𝑓 by Path-𝜕0 and Π-𝜂 (definition 27.2), likewise 𝑔 at 1. The first round trip is 𝗁𝖺𝗉𝗉𝗅𝗒(𝖿𝗎𝗇𝖾𝗑𝗍(𝑝))≡𝑃𝑎𝑡ℎ−𝛽,Π−𝛽𝜆𝑥.⟨𝑖⟩𝑝𝑥𝑖≡Π−𝜂,𝑃𝑎𝑡ℎ−𝜂𝑝, and the second is 𝖿𝗎𝗇𝖾𝗑𝗍(𝗁𝖺𝗉𝗉𝗅𝗒(𝑞))≡𝑃𝑎𝑡ℎ−𝛽,Π−𝛽⟨𝑖⟩𝜆𝑥.𝑞𝑖𝑥≡Π−𝜂,𝑃𝑎𝑡ℎ−𝜂𝑞. ◻
The proof used only definition 80.8 and the 𝛽𝜂-rules of Π: no Kan structure, no interval algebra beyond weakening. The principle not built into the base, with exact independence transfer still open (remark 111.89), and recovered from univalence only through a delicate argument (theorem 65.18) is, cubically, a rearrangement of binders. The dependent-path instance has an equally explicit form. If Γ⊢𝐴𝗍𝗒𝗉𝖾, Γ,𝑖:𝕀,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾, 𝑓0:∏𝑥:𝐴𝐵[0/𝑖], and 𝑓1:∏𝑥:𝐴𝐵[1/𝑖], then 𝜆𝑝.⟨𝑖⟩𝜆𝑥.𝑝𝑥𝑖:(∏𝑥:𝐴𝖯𝖺𝗍𝗁𝖯𝑖.𝐵(𝑓0𝑥,𝑓1𝑥))→𝖯𝖺𝗍𝗁𝖯𝑖.∏𝑥:𝐴𝐵(𝑓0,𝑓1), with inverse 𝜆𝑞.𝜆𝑥.⟨𝑖⟩𝑞𝑖𝑥. In either composite, Path-𝛽 and Π-𝛽 expose the rearranged binders, and Path-𝜂 and Π-𝜂 reduce the result judgmentally to the input.
★★☆ Verify that the Σ-clause of definition 80.25 is well typed: check that 𝗉𝗋2(𝑢) is a partial element of 𝐵[𝑎/𝑥] of extent 𝜑, using the third filler equality of construction 80.24.
★☆☆ Define an inversion of paths using 𝖼𝗈𝗆𝗉 but neither 1−𝑟 nor connections: 𝑝−1:=⟨𝑖⟩𝖼𝗈𝗆𝗉𝑗𝐴[(𝑖=0)↦𝑝𝑗,(𝑖=1)↦𝑎]𝑎. Check the faces, and compare with construction 80.10. (This is the derivation available when the interval algebra has no reversal or connections.)
★★★ Using a connection square and one composition, construct 𝖯𝖺𝗍𝗁𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏)(𝑝⋅𝗋𝖾𝖿𝗅𝑏,𝑝) for the concatenation of example 80.23, and sketch the corresponding construction for associativity. (Cf. theorem 30.20; the cubical proofs need no induction.)
★☆☆ Show by definition 80.25 that for every closed numeral ――𝑛, 𝗍𝗋𝖺𝗇𝗌𝗉𝑖ℕ――𝑛≡――𝑛 — regularity holds at ℕ on canonical forms, though not as a schematic rule (remark 80.27).
Composition asserts that extensibility is preserved along paths; the 𝖦𝗅𝗎𝖾 former asserts that it is preserved under equivalences, and is the engine of univalence. We first fix the cubical notions of contractibility and equivalence and three derived operations.
For Γ⊢𝑇𝗍𝗒𝗉𝖾, Γ⊢𝐴𝗍𝗒𝗉𝖾, 𝑓:𝑇→𝐴 and 𝑎:𝐴: 𝗂𝗌𝖢𝗈𝗇𝗍𝗋(𝐴):=∑𝑥:𝐴∏𝑦:𝐴𝖯𝖺𝗍𝗁𝐴(𝑥,𝑦),𝖿𝗂𝖻𝑓(𝑎):=∑𝑥:𝑇𝖯𝖺𝗍𝗁𝐴(𝑎,𝑓𝑥),𝗂𝗌𝖤𝗊𝗎𝗂𝗏(𝑓):=∏𝑎:𝐴𝗂𝗌𝖢𝗈𝗇𝗍𝗋(𝖿𝗂𝖻𝑓(𝑎)),𝑇≃𝐴:=∑𝑓:𝑇→𝐴𝗂𝗌𝖤𝗊𝗎𝗂𝗏(𝑓). These are the definitions of definition 62.21 with 𝖯𝖺𝗍𝗁 in place of the identity type. For 𝑒:𝑇≃𝐴 we write 𝑒𝑡 for 𝗉𝗋1(𝑒)𝑡.
Let Γ⊢𝑤:𝗂𝗌𝖢𝗈𝗇𝗍𝗋(𝐴) and Γ,𝜑⊢𝑢:𝐴. Then 𝖾𝗑𝗍(𝑤)[𝜑↦𝑢]:=𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝗉𝗋2(𝑤)𝑢𝑖]𝗉𝗋1(𝑤):𝐴[𝜑↦𝑢]. Conversely, if 𝐴 admits an extension operation — for every 𝜑 and every partial element 𝑢 of extent 𝜑, in every context extending Γ, a total element of 𝐴[𝜑↦𝑢] — then 𝗂𝗌𝖢𝗈𝗇𝗍𝗋(𝐴) is inhabited.
Proof of Lemma 80.32 — Contractible types are extensible
Proof. Forward: 𝗉𝗋2(𝑤)𝑢:𝖯𝖺𝗍𝗁𝐴(𝗉𝗋1(𝑤),𝑢) over Γ,𝜑, so the composition is defined and equals 𝗉𝗋2(𝑤)𝑢1≡𝑢 on 𝜑. Conversely put 𝑥:=𝖾𝗑𝗍[] (extent 0𝔽); given 𝑦:𝐴, work in Γ,𝑖:𝕀 with 𝜑:=(𝑖=0)∨(𝑖=1) and 𝑢:=[(𝑖=0)↦𝑥,(𝑖=1)↦𝑦]; then ⟨𝑖⟩𝖾𝗑𝗍[𝜑↦𝑢] is a path from 𝑥 to 𝑦. ◻
Let Γ,𝑖:𝕀⊢𝑓:𝑇→𝐴, Γ⊢𝜑:𝔽, Γ,𝜑,𝑖:𝕀⊢𝑡:𝑇 and Γ⊢𝑡0:𝑇[0/𝑖][𝜑↦𝑡[0/𝑖]]. Put 𝑐1:=𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝑓𝑡](𝑓[0/𝑖]𝑡0) and 𝑐2:=𝑓[1/𝑖](𝖼𝗈𝗆𝗉𝑖𝑇[𝜑↦𝑡]𝑡0). Then, with 𝑣:=𝖿𝗂𝗅𝗅𝑖𝑇[𝜑↦𝑡]𝑡0 and 𝑗 fresh, 𝗉𝗋𝖾𝗌𝑖𝑓[𝜑↦𝑡]𝑡0:=⟨𝑗⟩𝖼𝗈𝗆𝗉𝑖𝐴[𝜑∨(𝑗=1)↦𝑓𝑣](𝑓[0/𝑖]𝑡0) inhabits 𝖯𝖺𝗍𝗁𝐴[1/𝑖](𝑐1,𝑐2) and is the constant path ⟨𝑗⟩(𝑓𝑡)[1/𝑖] on 𝜑.
Proof of Lemma 80.33 — Functions preserve composition up to a path
Proof. On 𝜑, 𝑣≡𝑡 (construction 80.24), so the constraint is consistent; at 𝑗=0 the extra face vanishes and the body is 𝑐1; at 𝑗=1 the constraint has extent 1𝔽, so the composition equals (𝑓𝑣)[1/𝑖]≡𝑐2 by the filler equalities. On the overlap 𝜑∧(𝑗=0) both descriptions reduce to (𝑓𝑡)[1/𝑖]. On 𝜑∧(𝑗=1) the filler equation 𝑣[1/𝑖]≡𝖼𝗈𝗆𝗉𝑖𝑇[𝜑↦𝑡]𝑡0 gives the same term. Thus the system is compatible, and restricting the displayed path to 𝜑 leaves the constant path ⟨𝑗⟩(𝑓𝑡)[1/𝑖]. ◻
Let Γ⊢𝑒:𝑇≃𝐴 with underlying 𝑓. Given Γ⊢𝑎:𝐴, Γ,𝜑⊢𝑡:𝑇 and Γ,𝜑⊢𝑝:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑓𝑡), the operation 𝖾𝗑𝗍𝑒[𝜑↦(𝑡,𝑝)]𝑎:=𝖾𝗑𝗍(𝗉𝗋2(𝑒)𝑎)[𝜑↦(𝑡,𝑝)]:𝖿𝗂𝖻𝑓(𝑎)[𝜑↦(𝑡,𝑝)] extends the partial fiber element (𝑡,𝑝). Conversely, a function 𝑓:𝑇→𝐴 admitting such an operation (naturally in the context) is an equivalence.
Proof of Lemma 80.34 — Equivalences are fiberwise extensible
Proof. Forward: instance of lemma 80.32 at the contractible type 𝖿𝗂𝖻𝑓(𝑎). Conversely, for each 𝑎:𝐴, apply the extension operation to the empty partial element to obtain a center 𝑐𝑎:𝖿𝗂𝖻𝑓(𝑎). For 𝑧:𝖿𝗂𝖻𝑓(𝑎), in a fresh dimension 𝑖 extend the endpoint system [(𝑖=0)↦𝑐𝑎,(𝑖=1)↦𝑧]; abstraction in 𝑖 is a path from 𝑐𝑎 to 𝑧. Thus every fiber is contractible, which is precisely 𝗂𝗌𝖤𝗊𝗎𝗂𝗏(𝑓). ◻
The endpoint data alone cannot replace Glue. The tempting universe line [(𝑖=0)↦𝐴,(𝑖=1)↦𝐵] is not a type in the unrestricted context 𝑖:𝕀: Sys-form requires the extents to cover, but (𝑖=0)∨(𝑖=1)≠1𝔽 by proposition 80.2. Glue repairs the missing interior by supplying a total type underneath the partial endpoint data.
The former 𝖦𝗅𝗎𝖾, with introduction 𝗀𝗅𝗎𝖾 and elimination 𝗎𝗇𝗀𝗅𝗎𝖾, glues a partial type 𝑇 onto a total type 𝐴 along a partial equivalence 𝑓. Presuppositions are compressed per convention 26.14. The raw eliminator is written 𝗎𝗇𝗀𝗅𝗎𝖾𝜑,𝑓: its annotation records the partial equivalence, and substitution acts on 𝜑, 𝑓, and the argument.
On the extent 𝜑 the Glue type is𝑇: from Glue-form-1 and lemma 80.16, Γ,𝜑⊢𝑏:𝑇 for any 𝑏:𝖦𝗅𝗎𝖾[𝜑↦(𝑇,𝑓)]𝐴 — this establishes the premise 𝑓𝑏 in Glue-elim and the constraint 𝜑↦𝑏 in Glue-𝜂 well formed — and 𝗎𝗇𝗀𝗅𝗎𝖾 extends 𝑓: Γ,𝜑⊢𝗎𝗇𝗀𝗅𝗎𝖾𝑏≡𝑓𝑏:𝐴. Thus 𝗎𝗇𝗀𝗅𝗎𝖾:𝖦𝗅𝗎𝖾[𝜑↦(𝑇,𝑓)]𝐴→𝐴 is a total function restricting on 𝜑 to the partial equivalence 𝑓; that it is itself an equivalence is lemma 80.43.
Let Γ⊢𝑓:𝐴≃𝐵 and let 𝗂𝖽≃𝐵:𝐵≃𝐵 be the identity function with the contractibility of its fibers 𝖿𝗂𝖻𝗂𝖽(𝑦)≡∑𝑥:𝐵𝖯𝖺𝗍𝗁𝐵(𝑦,𝑥) given by construction 80.12. In Γ,𝑖:𝕀 put 𝐸:=𝖦𝗅𝗎𝖾[(𝑖=0)↦(𝐴,𝑓),(𝑖=1)↦(𝐵,𝗂𝖽≃𝐵)]𝐵. By Sys-sel and Glue-form-1, 𝐸[0/𝑖]≡𝐴 and 𝐸[1/𝑖]≡𝐵: an equivalence has become a line of types. (Once U reflects 𝖦𝗅𝗎𝖾, ⟨𝑖⟩𝐸 is a path in the universe — construction 80.42.)
The naive lid of a Glue composition would be 𝗀𝗅𝗎𝖾[𝜑[1/𝑖]↦𝑡′1]𝑎′1. It is not available: 𝑡′1 is constructed only under 𝛿:=∀𝑖.𝜑, whereas the lid requires data on the generally larger face 𝜑[1/𝑖]. The fiber extension in the next construction enlarges 𝑡′1 to that face, and the final composition in 𝐴[1/𝑖] repairs its image so that Glue introduction applies.
Let Γ,𝑖:𝕀⊢𝐵𝗍𝗒𝗉𝖾 with 𝐵≡𝖦𝗅𝗎𝖾[𝜑↦(𝑇,𝑓)]𝐴 (all data may depend on 𝑖), and let Γ,𝜓,𝑖:𝕀⊢𝑏:𝐵, Γ⊢𝑏0:𝐵[0/𝑖][𝜓↦𝑏[0/𝑖]] be composition data. Write 𝑎:=𝗎𝗇𝗀𝗅𝗎𝖾𝑏, 𝑎0:=𝗎𝗇𝗀𝗅𝗎𝖾𝑏0 and 𝛿:=∀𝑖.𝜑 (lemma 80.17); on 𝛿 the pair (𝑇,𝑓) is a line, on 𝜑[1/𝑖] only its face at 1 exists. Define 𝑎′1:=𝖼𝗈𝗆𝗉𝑖𝐴[𝜓↦𝑎]𝑎0(inΓ)𝑡′1:=𝖼𝗈𝗆𝗉𝑖𝑇[𝜓↦𝑏]𝑏0(inΓ,𝛿)𝜔:=𝗉𝗋𝖾𝗌𝑖𝑓[𝜓↦𝑏]𝑏0(inΓ,𝛿)(𝑡1,𝛼):=𝖾𝗑𝗍𝑓[1/𝑖][𝛿↦(𝑡′1,𝜔),𝜓↦(𝑏[1/𝑖],⟨𝑗⟩𝑎′1)]𝑎′1(inΓ,𝜑[1/𝑖])𝑎1:=𝖼𝗈𝗆𝗉𝑗(𝐴[1/𝑖])[𝜑[1/𝑖]↦𝛼𝑗,𝜓↦𝑎[1/𝑖]]𝑎′1(inΓ) and set 𝖼𝗈𝗆𝗉𝑖𝐵[𝜓↦𝑏]𝑏0≡𝗀𝗅𝗎𝖾[𝜑[1/𝑖]↦𝑡1]𝑎1, an element of 𝐵[1/𝑖][𝜓↦𝑏[1/𝑖]]. When Γ,𝑖:𝕀⊢𝜑≡1𝔽:𝔽 this agrees with 𝖼𝗈𝗆𝗉𝑖𝑇[𝜓↦𝑏]𝑏0, as required by Glue-form-1.
Two boundary checks close the construction. On 𝛿∧𝜓, the two proposed fiber elements reduce to (𝑏[1/𝑖],⟨𝑗⟩𝑎[1/𝑖]) by the boundary equations for 𝖼𝗈𝗆𝗉 and 𝗉𝗋𝖾𝗌; on 𝜓, the final 𝐴-composition reduces to 𝑎[1/𝑖], so Glue 𝜂 makes the result 𝑏[1/𝑖]. If 𝜑=1𝔽 throughout the line, then 𝛿=1𝔽 and Glue-form-1 reduces the whole construction to the displayed composition in 𝑇[CCHM18].
★★☆ Write out 𝗂𝖽≃𝐵 of example 80.37 in full: give the contraction of 𝖿𝗂𝖻𝗂𝖽(𝑦) by specializing construction 80.12, and check the two judgmental equalities 𝐸[0/𝑖]≡𝐴, 𝐸[1/𝑖]≡𝐵.
★★☆ Complete the converse of lemma 80.34: from the extension operation build, for each 𝑎:𝐴, the center and contraction of 𝖿𝗂𝖻𝑓(𝑎), following the proof of lemma 80.32.
The theory has a universe U à la Russell (cf. definition 29.1; we work with one level, the hierarchy and lifts being as in chapter 29):
Γ𝖼𝗍𝗑
Γ⊢U𝗍𝗒𝗉𝖾
-form
Γ⊢𝐴:U
Γ⊢𝐴𝗍𝗒𝗉𝖾
-Russell
and every former of the theory is reflected: if the constituents are in U, so are ∏𝑥:𝐴𝐵, ∑𝑥:𝐴𝐵, 𝐴+𝐵, ℕ, 𝟐, 𝟏, 𝟎, 𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏), 𝖯𝖺𝗍𝗁𝖯𝑖.𝐴(𝑎0,𝑎1) and 𝖦𝗅𝗎𝖾[𝜑↦(𝑇,𝑓)]𝐴.
For every Γ,𝑖:𝕀⊢𝐸𝗍𝗒𝗉𝖾, with 𝐴:=𝐸[0/𝑖] and 𝐵:=𝐸[1/𝑖], the derived operator 𝖾𝗊𝗎𝗂𝗏𝑖(𝐸):𝐴≃𝐵 has underlying map 𝑥↦𝗍𝗋𝖺𝗇𝗌𝗉𝑖𝐸𝑥. We import the contraction of its fibers exactly from CCHM §7.1, the paragraph beginning “Next, given an element” [CCHM18]. There the terms 𝜃0,𝜃1,𝜔,𝛿, their contexts, and all overlap equations are displayed; they assemble a path in 𝖿𝗂𝖻𝗍𝗋𝖺𝗇𝗌𝗉𝑖𝐸(𝑦) from the chosen center to an arbitrary (𝑥,𝛽). This paragraph therefore fixes a sharply bounded derived operator; the prose summary is not used as its contraction proof. The source’s orientation is retained throughout: 𝖾𝗊𝗎𝗂𝗏𝑖(𝐸):𝐸[0/𝑖]≃𝐸[1/𝑖].
For composition data Γ,𝜑,𝑖:𝕀⊢𝐸:U, Γ⊢𝐴0:U[𝜑↦𝐸[0/𝑖]]: Γ⊢𝖼𝗈𝗆𝗉𝑖U[𝜑↦𝐸]𝐴0≡𝖦𝗅𝗎𝖾[𝜑↦(𝐸[1/𝑖],𝖾𝗊𝗎𝗂𝗏𝑖(𝐸[1−𝑖/𝑖]))]𝐴0:U, where 𝖾𝗊𝗎𝗂𝗏𝑖(𝐸[1−𝑖/𝑖]):𝐸[1/𝑖]≃𝐸[0/𝑖] by construction 80.40 and 𝐸[0/𝑖]≡𝐴0 on 𝜑. Thus the universe is Kan because 𝖦𝗅𝗎𝖾 turns the transport equivalences of its constituent lines into a genuine type.
For Γ⊢𝑓:𝐴≃𝐵 with 𝐴,𝐵:U, define (via example 80.37 and definition 80.39) 𝗎𝖺(𝑓):=⟨𝑖⟩𝖦𝗅𝗎𝖾[(𝑖=0)↦(𝐴,𝑓),(𝑖=1)↦(𝐵,𝗂𝖽≃𝐵)]𝐵:𝖯𝖺𝗍𝗁U(𝐴,𝐵), with faces 𝗎𝖺(𝑓)0≡𝐴 and 𝗎𝖺(𝑓)1≡𝐵 judgmentally by Sys-sel followed by Glue-form-1: after [0/𝑖] the first extent is 1𝔽 and the Glue type reduces to 𝐴; after [1/𝑖] the second extent is 1𝔽 and it reduces to 𝐵.
Proof. By the converse of lemma 80.34 it suffices, for Γ⊢𝑎:𝐴, Γ,𝜓⊢𝑏:𝐵 and Γ,𝜓⊢𝛼:𝖯𝖺𝗍𝗁𝐴(𝑎,𝗎𝗇𝗀𝗅𝗎𝖾𝑏), to produce ˜𝑏:𝐵[𝜓↦𝑏] and ˜𝛼:𝖯𝖺𝗍𝗁𝐴(𝑎,𝗎𝗇𝗀𝗅𝗎𝖾˜𝑏)[𝜓↦𝛼]. On 𝜑: 𝑓 is an equivalence, 𝑏:𝑇 and 𝛼:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑓𝑏) (remark 80.36), so lemma 80.34 yields Γ,𝜑⊢𝑡:𝑇[𝜓↦𝑏] and Γ,𝜑⊢𝛽:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑓𝑡)[𝜓↦𝛼]. Set ˜𝑎:=𝖼𝗈𝗆𝗉𝑖𝐴[𝜑↦𝛽𝑖,𝜓↦𝛼𝑖]𝑎,˜𝑏:=𝗀𝗅𝗎𝖾[𝜑↦𝑡]˜𝑎,˜𝛼:=⟨𝑖⟩𝖿𝗂𝗅𝗅𝑖𝐴[𝜑↦𝛽𝑖,𝜓↦𝛼𝑖]𝑎. By Glue-𝛽, 𝗎𝗇𝗀𝗅𝗎𝖾˜𝑏≡˜𝑎; the filler equalities of construction 80.24 give the endpoints of ˜𝛼 and the constraints on 𝜓. ◻
Proof of Lemma 217.45 — Fiberwise maps over contractible totals
Proof. The induced total map 𝑇:∑𝑥:𝑋𝑃𝑥→∑𝑥:𝑋𝑄𝑥 sends (𝑥,𝑝) to (𝑥,𝑡𝑥𝑝). Any map between contractible types is an equivalence: choose the constant map at the source center as a quasiinverse and use the two contractions for the homotopies; then use theorem 62.27. For 𝑞:𝑄(𝑥), the fiber of 𝑡𝑥 over 𝑞 is equivalent to the fiber of 𝑇 over (𝑥,𝑞) because 𝑇 preserves the first projection judgmentally. The latter is contractible, so 𝑡𝑥 is an equivalence [Uni13]. ◻
consequently, every fiberwise map 𝑡:∏𝐵:U𝖯𝖺𝗍𝗁U(𝐴,𝐵)→(𝐴≃𝐵) is an equivalence on each fiber. In particular this holds for 𝑡𝐵(𝑝):=𝖾𝗊𝗎𝗂𝗏𝑖(𝑝); hence 𝖯𝖺𝗍𝗁U(𝐴,𝐵)≃(𝐴≃𝐵), with the orientation 𝐴≃𝐵 fixed by construction 80.40.
Proof. Part (1) is CCHM Corollary 10 [CCHM18]. Its proof applies the extension-to-contractibility direction of lemma 80.32 to a partial pair (𝑇,𝑓):∑𝑋:U𝑋≃𝐴. The total extension is
(𝖦𝗅𝗎𝖾[𝜑↦(𝑇,𝑓)]𝐴,𝗎𝗇𝗀𝗅𝗎𝖾),
and lemma 80.43 gives its equivalence component. The path witnessing agreement with (𝑇,𝑓) on 𝜑, including its composition and boundary reductions, is part of the cited corollary. We import that path rather than treating the displayed pair alone as a contraction proof.
For (2), the two total spaces are contractible by construction 80.12 and (1): the target total ∑𝐵:U𝐴≃𝐵 is equivalent, by inversion of equivalences, to the contractible total in (1). Hence lemma 217.45 makes every such 𝑡 an equivalence. For 𝑡𝐵(𝑝):=𝖾𝗊𝗎𝗂𝗏𝑖(𝑝), the endpoint convention of construction 80.40 gives exactly 𝐴≃𝐵. This is CCHM Corollary 11 [CCHM18]. ◻
Definition 65.6 asserts that a specific map 𝗂𝖽𝗍𝗈𝖾𝗊𝗏, defined by 𝖩-transport, is an equivalence. In cubical type theory 𝖩 is the derived operator of theorem 80.28, and the resulting 𝗂𝖽𝗍𝗈𝖾𝗊𝗏 is a fiberwise map between the two contractible total spaces of theorem 80.44(2); it is therefore an equivalence, and the univalence axiom holds verbatim — but now with proof, not postulate. Consequently, earlier results stated only with Π-, Σ-, universe-, natural-number-, and path structure — for example theorem 65.22 — transfer to this frozen signature. Results using propositional or 𝑛-truncations, quotients, or higher inductive types require adjoining those individual signatures and their Kan clauses; the finer note below records that separate extension boundary.
Unlike UA, the theorem just proved introduces no constant without computation rules: 𝗎𝖺(𝑓) is a 𝖦𝗅𝗎𝖾 type, transport along it unfolds by construction 80.38 and definition 80.41, and 𝗍𝗋𝖺𝗇𝗌𝗉𝑖(𝗎𝖺(𝑓)𝑖)𝑎 is path-equal to 𝑓𝑎 by the Glue calculation. For 𝑓=𝗌𝗐𝖺𝗉:𝟐≃𝟐, the term 𝗍𝗋𝖺𝗇𝗌𝗉𝑖(𝗎𝖺(𝑓)𝑖)𝗍𝗍 is connected by the path computed from Glue composition to 𝖿𝖿; no judgmental reduction of that Boolean term is claimed.
Let 𝗌𝗐𝖺𝗉:𝟐≃𝟐 exchange the two constructors and put 𝑢:=𝗍𝗋𝖺𝗇𝗌𝗉𝑖(𝗎𝖺(𝗌𝗐𝖺𝗉)𝑖)𝗍𝗍. In construction 80.38 take 𝜓=0𝔽 and 𝜑=(𝑖=0)∨(𝑖=1). Then 𝛿=∀𝑖.𝜑=0𝔽, so the 𝑡′1 branch disappears; at 𝑖=1 the remaining equivalence is 𝗂𝖽≃𝟐. Its fiber extension contracts the singleton over 𝗌𝗐𝖺𝗉(𝗍𝗍), and the final 𝐴-composition returns its path component. Thus the rule produces ⟨𝑗⟩𝛼𝑗:𝖯𝖺𝗍𝗁𝟐(𝑢,𝗌𝗐𝖺𝗉(𝗍𝗍)),𝗌𝗐𝖺𝗉(𝗍𝗍)≡𝖿𝖿. The result is computed from Glue composition; it is not a postulated equation about an opaque univalence constant.
Identity types, higher inductive types, implementations. The theory as presented has no 𝖨𝖽; theorem 80.28 recovers 𝖩 with a propositional computation rule only. Swan’s construction repairs this: define 𝖨𝖽𝐴𝑎𝑏 as the type of pairs (𝜔,𝜑) with 𝜔:𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏)[𝜑↦⟨𝑖⟩𝑎] — a path marked with an extent on which it is known to be constant. With 𝗋𝖾𝖿𝗅𝑎:=(⟨𝑖⟩𝑎,1𝔽), the eliminator defined by a composition over the marked extent satisfies 𝖩(𝑑;𝗋𝖾𝖿𝗅𝑎)≡𝑑 judgmentally, and 𝖨𝖽𝐴𝑎𝑏≃𝖯𝖺𝗍𝗁𝐴(𝑎,𝑏), so univalence transfers to 𝖨𝖽[CCHM18]. Higher inductive types also extend the theory: the circle of definition 68.8 is added with constructors 𝖻𝖺𝗌𝖾, 𝗅𝗈𝗈𝗉(𝑟) and a homogeneous composition constructor 𝗁𝖼𝗈𝗆𝗉, and its eliminator computes on all three (ibid., §9.2). Splitting 𝖼𝗈𝗆𝗉 into 𝗁𝖼𝗈𝗆𝗉 and 𝗍𝗋𝖺𝗇𝗌𝗉 is also how Cubical Agda organizes the primitives; the Cartesian systems of Angiuli et al. make this split fundamental [ABC^+21].
★☆☆ Verify in detail the two faces of 𝗎𝖺(𝑓) claimed in construction 80.42: restrict the system under [0/𝑖] and [1/𝑖], compute the resulting face formulas, and apply Sys-sel and Glue-form-1.
★★★ Unfold 𝗍𝗋𝖺𝗇𝗌𝗉𝑖(𝗎𝖺(𝑓)𝑖)𝑎 using construction 80.38 with 𝜓=0𝔽, and exhibit a path to 𝑓𝑎 in 𝐵. (Compute 𝛿=∀𝑖.𝜑=0𝔽 for 𝜑=(𝑖=0)∨(𝑖=1); the interesting branch is 𝜑[1/𝑖]=1𝔽, where 𝖾𝗑𝗍𝗂𝖽≃𝐵 contracts a singleton.)
★★☆ Spell out the fiberwise-equivalence criterion used in theorem 80.44(2): given families 𝑃,𝑄 over U with contractible total spaces and a fiberwise map 𝑡, show each 𝖿𝗂𝖻𝑡𝑋 is contractible by transporting contractions along the total-space equivalence. (Cf. [Uni13], Thm. 4.7.7.)
★★★ Write the complete boundary of a two-dimensional open box, construct its lid by composition, and restrict the result to every face. Then use Glue to calculate transport of both Boolean constructors along the swap line.
★★★Practical project.demorgan-face-normalizer Implement in Agda or Kappa normalization and entailment for finite De Morgan face formulas and compatibility checking for systems. Preserve formula equivalence under every endpoint assignment. Normalize the connection and reversal examples, accept a compatible square boundary, and reject two branches that disagree on their overlap. Mutation test: omit the overlap check and ensure the malformed system is then accepted.
The system of this chapter is that of Cohen, Coquand, Huber and Mörtberg [CCHM18], from which our definition 80.1, definition 80.8, definition 80.14, definition 80.18, definition 80.21, definition 80.25, definition 80.35, definition 80.41 are taken with only notational change (they write 𝑡(𝑖0), 𝑡(𝑖/𝑟) for our 𝑡[0/𝑖], 𝑡[𝑟/𝑖], and separate system braces from constraint braces); the derived operations of § 80.5 are their §5, and theorem 80.44 assembles their Theorem 9 and Corollaries 10–11. The paper grew out of the first constructive cubical model of univalence by Bezem, Coquand and Huber, formulated in a substructural cube category without diagonals; the De Morgan structure — connections and reversal, after the cubes with connections of Brown and Higgins — was adopted precisely to make the filling of construction 80.24 derivable from composition and to accommodate higher inductive types (see the introduction of [CCHM18] for this history). The accompanying Haskell implementation cubicaltt typechecks all the constructions of this chapter, and the same rules underlie Cubical Agda. The marked identity type of the final finer block is due to Swan. Uniformity of composition (remark 80.22) descends from the earlier work and ultimately from the uniform Kan condition; the semantics in De Morgan cubical sets is developed in §8 of [CCHM18] and is best approached with the categories-with-families apparatus of chapter 54 (definition 54.16, theorem 54.28). Canonicity for this theory was proved by Huber by an operational-semantic argument; normalization and decidability came later, by the synthetic Tait computability of Sterling and Angiuli [SA21], stated for the Cartesian variant. Further Cartesian rules are developed in [ABC^+21], and Angiuli’s thesis gives their computational interpretation [Ang19]. Our route through interval, paths, partiality, composition, and Glue follows the draft account of Angiuli and Gratzer [AG26], which develops the design space between judgmental structure and type-level operations. The univalence-as-contractibility formulation of theorem 80.44(1) is the one they, following Escardó, emphasize. The homotopy-theoretic background and the fiberwise criterion are in the HoTT Book [Uni13], Chapter 4.
Diagram
Diagram (horizontal direction 
Diagram At