Every binder forces the same substitution calculation: variables shift, successive replacements compose, and extending a context adds one final component. As long as substitution remains an operation outside the syntax, each new type former requires those facts to be proved again. Put the replacement operations into the language itself and impose the equations that the repeated calculations establish. The construction succeeds if assigning meanings to the primitive operations then determines the meaning of every well-formed expression, with no choice left over.
The substitution calculus
We replace named variables by two combinators (𝐩 for weakening, 𝐪 for the last variable) and close substitutions under composition; every equation that definition 26.22 proves about the calculus becomes a rule of the calculus.
For example, if Γ⊢𝑎:𝐴 and Δ⊢𝛾:Γ, the new syntax contains 𝑎[𝛾] at type 𝐴[𝛾]. A further substitution Ξ⊢𝛿:Δ must satisfy 𝑎[𝛾][𝛿]≡𝑎[𝛾∘𝛿]. This equation is the reason composition belongs to the syntax.
Fix a finitary dependent signature S. It consists of disjoint sets Sty and Stm of type and term operation symbols. Each symbol comes with a finite metavariable telescope. Every metavariable is a type or term judgment in a context formed by finitely many explicit extensions, and each classifier may mention only earlier metavariables. A type symbol has a type-judgment schema as output; a term symbol has a term-judgment schema whose classifier is built from the preceding inputs. These data fix the arity, binding depth, sorts, and output boundary of every operation before any raw expression is formed. Equations are additional rules and are not part of the grammar.
The substitution calculus over S is the explicit multi-sorted algebraic syntax whose operations make substitution uniform for contexts, types, terms, and substitutions.
In this definition, 𝐴[𝛾] is an explicit algebraic constructor, together with 𝗂𝖽, ∘, 𝐩, 𝐪, ⟨𝛾,𝑎⟩, and 𝛾+. In the named syntax of definition 26.1, 𝐴[𝑎/𝑥] remains the capture-avoiding meta-operation. No judgment uses both forms.
Raw syntax. Contexts, substitutions, types and terms are generated by the grammar Γ,Δ::=⋅∣Γ.𝐴𝛾,𝛿::=𝗂𝖽∣𝛾∘𝛿∣𝐩∣⟨⟩∣⟨𝛾,𝑎⟩𝐴,𝐵::=𝐴[𝛾]∣𝐹(⃗𝐴;⃗𝑎)𝑎,𝑏,𝑓::=𝐪∣𝑎[𝛾]∣𝑔(⃗𝐴;⃗𝑎). Here 𝐹 ranges over Sty and 𝑔 over Stm. The metavectors contain exactly the input telescope prescribed by the selected symbol, so the language is fixed by S rather than extended by metavariable choice. No particular type former is present in the generic calculus. The first concrete instance, with Π, is specified in definition 54.9; the full Π/Σ/𝖨𝖽/𝖴 instance is fixed only after definition 54.24, by definition 116.28. There are no variable names and no binders: 𝜆(𝐴,𝑏) binds nothing; 𝐴 is its raw domain annotation, and the body 𝑏 lives in an extended context. This is the algebraic counterpart of 𝜆(𝑥:𝐴).𝑏.
Judgment forms. Besides the five judgment forms of the named theory (cf. definition 26.22), there is a judgment Δ⊢𝛾:Γ (“𝛾 is a substitution from Δ to Γ”), presupposing Δ𝖼𝗍𝗑 and Γ𝖼𝗍𝗑, and its equality form Δ⊢𝛾≡𝛾′:Γ, presupposing that both sides are substitutions from Δ to Γ (convention 26.14 applies verbatim). There is no context-equality judgment (remark 54.4).
(b) Action on types and terms. A substitution moves types and terms from its codomain to its domain:
Δ⊢𝛾:ΓΓ⊢𝐴𝗍𝗒𝗉𝖾
Δ⊢𝐴[𝛾]𝗍𝗒𝗉𝖾
Sb-Ty
Δ⊢𝛾:ΓΓ⊢𝑎:𝐴
Δ⊢𝑎[𝛾]:𝐴[𝛾]
Sb-Tm
(c) Category structure.
Γ𝖼𝗍𝗑
Γ⊢𝗂𝖽:Γ
Sb-Id
Γ2⊢𝛾1:Γ1Γ1⊢𝛾0:Γ0
Γ2⊢𝛾0∘𝛾1:Γ0
Sb-Comp
Δ⊢𝛾:Γ
Δ⊢𝗂𝖽∘𝛾≡𝛾:Γ
Sb-IdL
Δ⊢𝛾:Γ
Δ⊢𝛾∘𝗂𝖽≡𝛾:Γ
Sb-IdR
Γ3⊢𝛾2:Γ2Γ2⊢𝛾1:Γ1Γ1⊢𝛾0:Γ0
Γ3⊢(𝛾0∘𝛾1)∘𝛾2≡𝛾0∘(𝛾1∘𝛾2):Γ0
Sb-Assoc
(d) Functoriality of the action. Substituting by 𝗂𝖽 is the identity, and substituting by a composite is iterated substitution:
Γ⊢𝐴𝗍𝗒𝗉𝖾
Γ⊢𝐴[𝗂𝖽]≡𝐴𝗍𝗒𝗉𝖾
Ty-Id
Γ⊢𝑎:𝐴
Γ⊢𝑎[𝗂𝖽]≡𝑎:𝐴
Tm-Id
Γ2⊢𝛾1:Γ1Γ1⊢𝛾0:Γ0Γ0⊢𝐴𝗍𝗒𝗉𝖾
Γ2⊢𝐴[𝛾0∘𝛾1]≡𝐴[𝛾0][𝛾1]𝗍𝗒𝗉𝖾
Ty-Comp
Γ2⊢𝛾1:Γ1Γ1⊢𝛾0:Γ0Γ0⊢𝑎:𝐴
Γ2⊢𝑎[𝛾0∘𝛾1]≡𝑎[𝛾0][𝛾1]:𝐴[𝛾0∘𝛾1]
Tm-Comp
The conclusion of Tm-Id is meta-well-typed only because of Ty-Id: a priori 𝑎[𝗂𝖽] has type 𝐴[𝗂𝖽], and the type equality allows it to be compared with 𝑎 at type 𝐴 via the conversion rule of definition 26.22. Equations and typing rules cannot be disentangled in dependent type theory.
(e) Weakening and the zeroth variable.
Γ⊢𝐴𝗍𝗒𝗉𝖾
Γ.𝐴⊢𝐩:Γ
Sb-Wk
Γ⊢𝐴𝗍𝗒𝗉𝖾
Γ.𝐴⊢𝐪:𝐴[𝐩]
Tm-Vz
A variable is a term of the form 𝐪[𝐩𝑘], where 𝐩𝑘 is the 𝑘-fold composite (𝐩0:=𝗂𝖽); the number 𝑘 is its de Bruijn index.
(f) The empty context is terminal.
Γ𝖼𝗍𝗑
Γ⊢⟨⟩:⋅
Sb-Emp
Γ⊢𝛿:⋅
Γ⊢𝛿≡⟨⟩:⋅
Sb-Emp-Uniq
(g) Substitution extension. A substitution into Γ.𝐴 is a substitution into Γ together with a term of the instantiated type 𝐴:
As in definition 26.22, each equality judgment of definition 54.2 is closed under reflexivity, symmetry and transitivity; every operation of the calculus is a congruence; and typing is closed under conversion: from Γ⊢𝑎:𝐴 and Γ⊢𝐴≡𝐵𝗍𝗒𝗉𝖾 infer Γ⊢𝑎:𝐵, and judgmentally equal contexts may be exchanged in any judgment. We use these closure rules whenever a displayed equality changes the type of a term.
No context-equality judgment is postulated because none is needed: two contexts can only be equal by having pairwise judgmentally equal types, and this relation is generated by the congruence closure of convention 54.3. If ⋅⊢𝐴≡𝐴′𝗍𝗒𝗉𝖾 then ⋅.𝐴 and ⋅.𝐴′ are interchangeable in every judgment.
A substitution Δ⊢𝛾:Γ points from Δ to Γ, while types and terms travel the other way, from Γ to Δ (Sb-Ty, Sb-Tm). Logically: 𝛾 proves every hypothesis of Γ from the hypotheses of Δ, so whatever holds under Γ holds under Δ. The action 𝐴↦𝐴[𝛾] is contravariant, as with preimages.
In this calculus substitution is derivable: the rules Sb-Ty and Sb-Tm belong to the system, and the group (d), (g) equations say how substitution computes. Under the named presentation, stability under substitution is admissible: it is a theorem proved by rule induction (the pattern of theorem 2.16) and can break when rules are added. Here an added former admits substitution only when its signature includes an equation commuting that former with −[𝛾]. For dependent products the required type equation is Π(𝐴,𝐵)[𝛾]≡Π(𝐴[𝛾],𝐵[𝛾+]).
For Δ⊢𝛾:Γ and Γ⊢𝐴𝗍𝗒𝗉𝖾, the lift of 𝛾 by 𝐴 is 𝛾+:=⟨𝛾∘𝐩,𝐪⟩,Δ.𝐴[𝛾]⊢𝛾+:Γ.𝐴. Well-typedness: Δ.𝐴[𝛾]⊢𝐪:𝐴[𝛾][𝐩] by Tm-Vz, and 𝐴[𝛾][𝐩]≡𝐴[𝛾∘𝐩] by Ty-Comp, as Sb-Ext requires. The lift leaves the zeroth variable alone and applies 𝛾 to the rest of the context; it is what “capture-avoiding” becomes when there is nothing to capture.
A Π-structure on the substitution calculus consists of formation, abstraction, application, computation, and uniqueness operations together with their substitution equations. The same pattern defines the Σ, identity, and universe structures used by theorem 54.27. We first give the Π-operations in full (convention 27.1).
The substitution ⟨𝗂𝖽,𝑎⟩ in Pi-Elim instantiates the zeroth variable of 𝐵 by 𝑎 and leaves Γ fixed: it is the algebraic form of 𝐵[𝑎/𝑥]. The right-hand side of Lam-Sb is well-typed by Pi-Sb — the same intertwining as in group (d) of definition 54.2.
Proof of Lemma 116.10 — Extension commutes with substitution
Proof. Apply Ext-Uniq to the left-hand side. Its weakening component is 𝐩∘(⟨𝛾,𝑎⟩∘𝛿)𝑆𝑏−𝐴𝑠𝑠𝑜𝑐=(𝐩∘⟨𝛾,𝑎⟩)∘𝛿𝐸𝑥𝑡−𝑊𝑘=𝛾∘𝛿. Its variable component is 𝐪[⟨𝛾,𝑎⟩∘𝛿]𝑇𝑚−𝐶𝑜𝑚𝑝≡𝐪[⟨𝛾,𝑎⟩][𝛿]𝐸𝑥𝑡−𝑉𝑧≡𝑎[𝛿]. The extension reconstructed from these two components is the right-hand side of the asserted equality. ◻
★★☆ Reconstruct lemma 116.10 without reading its proof. In particular, identify the one category equation and the one term equation needed to simplify the two components given by Ext-Uniq.
★★☆ Verify that App-Sb is meta-well-typed: show that both sides are terms of type 𝐵[⟨𝛾,𝑎[𝛾]⟩], exhibiting each rule and equation used. In particular show 𝛾+∘⟨𝗂𝖽,𝑎[𝛾]⟩≡⟨𝛾,𝑎[𝛾]⟩.
★★☆ Show that the general variable rule is derivable: if Γ⊢𝐴𝗍𝗒𝗉𝖾 and 𝐵1,…,𝐵𝑘 successively extend Γ.𝐴, then Γ.𝐴.𝐵1….𝐵𝑘⊢𝐪[𝐩𝑘]:𝐴[𝐩𝑘+1], generalizing example 54.7.
Let TΠΣ𝖨𝖽𝖴 denote the finitary named fragment of chapter 26–chapter 30 generated by the structural rules, Π-, Σ-, and intensional identity types, and the displayed predicative universe hierarchy. Its algebraic presentation has the same signature SΠΣ𝖨𝖽𝖴 as theorem 54.27. We give a forward translation covering that whole signature. Its converse is proved only for the structural-plus-Π subsignature, whose substitution-normalization proof is fully displayed; the larger converse is not used for soundness or initiality.
Define a translation (−)∗ from the named raw syntax of definition 26.1 to the algebraic raw syntax, by recursion:
named
algebraic
𝑥1:𝐴1,…,𝑥𝑛:𝐴𝑛 (context)
⋅.𝐴∗1.….𝐴∗𝑛
𝑥𝑛−𝑘 (declared 𝑘 entries from the right)
𝐪[𝐩𝑘]
∏𝑥:𝐴𝐵
Π(𝐴∗,𝐵∗)
∑𝑥:𝐴𝐵
Σ(𝐴∗,𝐵∗)
𝜆(𝑥:𝐴).𝑏
𝜆(𝐴∗,𝑏∗)
𝑓𝑎
𝖺𝗉𝗉(𝑓∗,𝑎∗)
𝐵[𝑎/𝑥] (𝑥 the last variable)
𝐵∗[⟨𝗂𝖽,𝑎∗⟩]
weakening by 𝑥:𝐴
−[𝐩]
The variable clause is relative to the ambient context: (𝑥𝑖)∗ in the context 𝑥1:𝐴1,…,𝑥𝑛:𝐴𝑛 is 𝐪[𝐩𝑛−𝑖]. The type clause for 𝐴∗𝑖 is computed in the context 𝑥1:𝐴1,…,𝑥𝑖−1:𝐴𝑖−1; the body 𝐵∗ of a Π-type in the context extended by 𝑥:𝐴. The same extended-context clause is used for Σ: if Γ,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾, then Σ(𝐴∗,𝐵∗) is formed from Γ∗⊢𝐴∗𝗍𝗒𝗉𝖾 and Γ∗.𝐴∗⊢𝐵∗𝗍𝗒𝗉𝖾. Identity types translate by 𝖨𝖽𝐴(𝑎,𝑏)↦𝖨𝖽𝐴∗(𝑎∗,𝑏∗); the remaining nonbinding constructors translate recursively. The named domain annotation becomes the first argument of the algebraic abstraction. Conversely, reconstruction copies that argument back into 𝜆(𝑥:𝐴).𝑏, normally printed 𝜆𝑥.𝑏.
In the empty context, with U a universe (definition 29.1) and 𝖤𝗅 its decoding, (𝜆𝑥.𝜆𝑦.𝑦)∗=𝜆(U,𝜆(𝖤𝗅(𝐪),𝐪)):Π(U,Π(𝖤𝗅(𝐪),𝖤𝗅(𝐪[𝐩]))). the algebraic type of the polymorphic identity function. The inner occurrence of 𝑥 costs one weakening because a declaration (𝑦) has intervened; the named syntax hides exactly this bookkeeping.
In the structural substitution calculus extended by exactly the Π operations and equations of definition 54.9, every derivable algebraic context, substitution, type, and term is judgmentally equal to one in substitution-normal form: substitutions are extension lists, and the action −[𝛾] in a type or term occurs only in subterms of the shape 𝐪[𝐩𝑘].
Proof. Put 𝑣𝑘:=𝐪[𝐩𝑘]. A normalized substitution from Δ to 𝑥1:𝐴1,…,𝑥𝑚:𝐴𝑚 is the typed extension list [𝑎1,…,𝑎𝑚]:=⟨⋯⟨⟨⟨⟩,𝑎1⟩,𝑎2⟩⋯,𝑎𝑚⟩. Let 𝗏𝖺𝗋𝗌Γ=[𝑣𝑚−1,…,𝑣0] for a context of length 𝑚, and let 𝗌𝗁𝗂𝖿𝗍 increment every free de Bruijn index in a normal expression.
Define normalizers 𝑁Γ,𝑁𝑆,𝑁𝑇,𝑁𝑡 on derivable contexts, substitutions, types, and terms by 𝑁Γ(⋅)=⋅,𝑁Γ(Γ.𝐴)=𝑁Γ(Γ).𝑁𝑇(𝐴),𝑁𝑆(⟨⟩)=[],𝑁𝑆(𝗂𝖽Γ)=𝗏𝖺𝗋𝗌Γ,𝑁𝑆(𝐩Γ,𝐴)=𝗌𝗁𝗂𝖿𝗍(𝗏𝖺𝗋𝗌Γ),𝑁𝑆(⟨𝛾,𝑎⟩)=⟨𝑁𝑆(𝛾),𝑁𝑡(𝑎)⟩,𝑁𝑆(𝛾∘𝛿)=𝐶[𝑁𝑆(𝛾),𝑁𝑆(𝛿)],𝑁𝑇(𝐴[𝛾])=𝐸𝑇[𝑁𝑇(𝐴),𝑁𝑆(𝛾)],𝑁𝑡(𝑎[𝛾])=𝐸𝑡[𝑁𝑡(𝑎),𝑁𝑆(𝛾)]. They preserve all other constructors recursively. In particular, 𝑁𝑇(Π(𝐴,𝐵))=Π(𝑁𝑇(𝐴),𝑁𝑇(𝐵)),𝑁𝑡(𝜆(𝐴,𝑏))=𝜆(𝑁𝑇(𝐴),𝑁𝑡(𝑏)),𝑁𝑡(𝖺𝗉𝗉(𝑓,𝑎))=𝖺𝗉𝗉(𝑁𝑡(𝑓),𝑁𝑡(𝑎)).
The hereditary action 𝐸 looks up variables and distributes through constructors. For 𝛾=[𝑎1,…,𝑎𝑚], 𝐸𝑡[𝑣𝑘,𝛾]=𝑎𝑚−𝑘(0≤𝑘<𝑚),𝗅𝗂𝖿𝗍(𝛾)=[𝗌𝗁𝗂𝖿𝗍(𝑎1),…,𝗌𝗁𝗂𝖿𝗍(𝑎𝑚),𝑣0]. Its binding clauses are 𝐸𝑇[Π(𝐴,𝐵),𝛾]=Π(𝐸𝑇[𝐴,𝛾],𝐸𝑇[𝐵,𝗅𝗂𝖿𝗍(𝛾)]),𝐸𝑡[𝜆(𝐴,𝑏),𝛾]=𝜆(𝐸𝑇[𝐴,𝛾],𝐸𝑡[𝑏,𝗅𝗂𝖿𝗍(𝛾)]),𝐸𝑡[𝖺𝗉𝗉(𝑓,𝑎),𝛾]=𝖺𝗉𝗉(𝐸𝑡[𝑓,𝛾],𝐸𝑡[𝑎,𝛾]). Atomic constants are fixed and every nonbinding argument is acted on recursively. Composition is pointwise hereditary action: 𝐶[[𝑎1,…,𝑎𝑚],𝛿]=[𝐸𝑡[𝑎1,𝛿],…,𝐸𝑡[𝑎𝑚,𝛿]],𝐶[[],𝛿]=[]. The lookup equations are Ext-Vz and iterated Ext-Wk; list composition is lemma 116.10; and the normal form of the algebraic lift 𝛾+=⟨𝐩∘𝛾,𝐪⟩ is the displayed 𝗅𝗂𝖿𝗍(𝛾).
This mutual recursion is well founded. In 𝐸[𝑒,𝛾] use the proper-subexpression order on 𝑒, followed at a variable by its index and the list length. In 𝐶[𝛾,𝛿] use the length of 𝛾; each entry calls 𝐸 on its own proper expression tree. The fusion equation 𝐸[𝐸[𝑎,𝛾],𝛿]=𝐸[𝑎,𝐶[𝛾,𝛿]] is then proved, rather than used as a recursive clause, by induction on 𝑎. The variable case is list lookup; the binder case uses 𝗅𝗂𝖿𝗍(𝐶[𝛾,𝛿])=𝐶[𝗅𝗂𝖿𝗍(𝛾),𝗅𝗂𝖿𝗍(𝛿)]; application uses its two induction hypotheses.
Simultaneous induction on a derivation proves that 𝑁 preserves all presupposed indices, that every input is judgmentally equal to its normal form, and that judgmentally equal inputs have the same normal form. For substitutions, identity and weakening use 𝗏𝖺𝗋𝗌 and shifted 𝗏𝖺𝗋𝗌; the empty substitution is []; extension appends one term; and composition uses 𝐶. The category equations become equality of lists by fusion. The extension equations become last-entry lookup, prefix lookup, empty-list uniqueness, and reconstruction from a prefix and final entry. The type and term action equations are the defining clauses of 𝐸; Pi-Sb, Lam-Sb, and App-Sb are its three constructor cases. For every equality-closure rule, its premise identifies inputs with the same normal form, so its conclusion does as well.
Thus every derivable object is equal to its normal form. Its substitutions are extension lists, and every remaining action in a type or term lies in a variable 𝑣𝑘, as required. ◻
if the judgments Γ𝖼𝗍𝗑,Γ⊢𝐴𝗍𝗒𝗉𝖾,Γ⊢𝑎:𝐴 are derivable in TΠΣ𝖨𝖽𝖴, then their translations are derivable in the substitution calculus, and judgmental equalities are preserved;
in the structural-plus-Π subsignature, every algebraic context, type, term, or equality judgment is, up to judgmental equality, the translation of a named one; and if two named judgments have judgmentally equal translations, then after 𝛼-renaming their named expressions are judgmentally equal;
in that same subsignature, meta-substitution becomes composition: (𝑏[𝑎/𝑥])∗≡𝑏∗[⟨𝗂𝖽,𝑎∗⟩] whenever Γ,𝑥:𝐴⊢𝑏:𝐵 and Γ⊢𝑎:𝐴.
Proof of Theorem 54.13 — Equivalence of the presentations
Proof.Translation preserves judgments. Induct on the named derivation. The structural cases use the action, weakening, and extension rules of definition 54.2. For the binder case, a premise Γ,𝑥:𝐴⊢𝑏:𝐵 translates to Γ∗.𝐴∗⊢𝑏∗:𝐵∗, so Pi-Intro gives Γ∗⊢𝜆(𝐴∗,𝑏∗):Π(𝐴∗,𝐵∗), the translation of Γ⊢𝜆(𝑥:𝐴).𝑏:∏𝑥:𝐴𝐵. The Σ binder uses the same extended-context premise, while identity cases translate their arguments recursively. The same induction carries the substitution invariant used in clause (3): translating a named substitution into the last variable agrees judgmentally with algebraic substitution extension. Thus it proves clause (1). No normalization or reconstruction theorem is used in this direction.
Reconstruction. By lemma 54.12, every algebraic object has a substitution-normal representative. Reconstruct named syntax simultaneously for contexts, substitutions, types, and terms. Choose fresh context names from left to right. The variable 𝐪[𝐩𝑘] becomes the variable declared 𝑘 places from the right. In particular, 𝜆(𝐴,𝑏)∘:=𝜆(𝑥:𝐴∘).𝑏∘, where 𝑥 is fresh and 𝑏∘ is reconstructed in Γ∘,𝑥:𝐴∘. An extension-list substitution becomes the corresponding simultaneous named substitution. Call the resulting operation (−)∘.
Induction on normal syntax gives ((𝑒∗)∘)=𝛼𝑒,(𝑑∘)∗≡𝑑. The variable round trips are Ext-Vz and Ext-Wk. For an abstraction, the fresh name chosen in reconstruction may differ from the original name, but lifting leaves the new last variable fixed; hence the first equation holds up to 𝛼-equivalence and the second holds judgmentally. Induction on an algebraic derivation now gives the reconstructed context, type, or term judgment for every premise and conclusion. Applying (−)∘ to an equality between two translations proves faithfulness. This establishes clause (2).
Meta-substitution becomes composition. Put 𝜎:=⟨𝗂𝖽,𝑎∗⟩. Simultaneous induction on 𝑏 and its type proves (𝑏[𝑎/𝑥])∗≡𝑏∗[𝜎]. The variable cases are Ext-Vz and Ext-Wk. If 𝑏=𝜆(𝑦:𝐶).𝑐, with 𝑦 fresh for 𝑎, the induction hypothesis in the extended context gives (𝑐[𝑎/𝑥])∗≡𝑐∗[𝜎+]. Therefore Lam-Sb gives ((𝜆(𝑦:𝐶).𝑐)[𝑎/𝑥])∗≡𝜆(𝐶∗[𝜎],𝑐∗[𝜎+])≡𝜆(𝐶∗,𝑐∗)[𝜎]. The nonbinding former cases use their displayed substitution equations. This proves clause (3) and completes the simultaneous argument required in clause (1). ◻
The full named signature translates soundly to the algebraic presentation; the converse equivalence established here is the structural-plus-Π case of theorem 54.13. The named syntax remains the default presentation. The algebraic presentation is needed here because quotienting its explicit substitution equations makes contexts, substitutions, types, and terms into CwF data by construction. Nothing below uses a converse translation for Σ, identity, or universe syntax.
★☆☆ Let Γ=(𝑓:𝐴→𝐵,𝑥:𝐴) and let 𝜎=[𝑔,𝑎]:Δ→Γ, with 𝑔:𝐴→𝐵 and 𝑎:𝐴 in Δ. Use the clauses in lemma 54.12 to normalize 𝖺𝗉𝗉(𝑣1,𝑣0)[𝜎]. Then lift 𝜎 under a fresh 𝑦:𝐶 and compute the images of 𝑣0,𝑣1,𝑣2 separately.
The substitution rules have the shape of functions between collections of judgments. Their identity and composition equations require the following small semantic interface.
A category has objects, identity arrows, associative composition, and the two unit laws. A functor preserves those data and equations; the opposite category Cop reverses arrows. An object 1 is terminal when every object has exactly one arrow to it. A commuting square is a pullback when every pair of arrows into its lower-left and upper-right corners with equal composites factors through its upper-left corner in exactly one way. An isomorphism is an arrow with a two-sided inverse. These descriptions are the complete interface used below; no result from a separate category-theory chapter is needed.
The syntax quotients and categories from this point through the initiality theorem are external sets in the ambient ZFC metatheory of convention 48.28. Their construction uses no inaccessible cardinal, and no soundness or underivability claim is internal to the object theory.
Read definition 54.2 semantically — sets for judgments, functions for rules, equality for judgmental equality — and the result is a piece of category theory.
The category 𝐅𝐚𝐦 has as objects pairs (𝑋,(𝑈𝑥)𝑥∈𝑋) of a set 𝑋 and an 𝑋-indexed family of sets, and as morphisms (𝑋,𝑈)→(𝑌,𝑉) pairs (𝑓,𝑔) of a function 𝑓:𝑋→𝑌 and a family of functions 𝑔𝑥:𝑈𝑥→𝑉𝑓(𝑥).
a category C with a chosen terminal object 𝟏; its objects are called contexts (Γ,Δ,…) and its morphisms substitutions;
for each context Γ a set Ty(Γ) of types, and for each 𝛾:Δ→Γ a function −[𝛾]:Ty(Γ)→Ty(Δ), functorially: 𝐴[𝗂𝖽]=𝐴 and 𝐴[𝛾∘𝛿]=𝐴[𝛾][𝛿];
for each Γ and 𝐴∈Ty(Γ) a set Tm(Γ,𝐴) of terms, and for each 𝛾:Δ→Γ a function −[𝛾]:Tm(Γ,𝐴)→Tm(Δ,𝐴[𝛾]), functorially: 𝑎[𝗂𝖽]=𝑎 and 𝑎[𝛾∘𝛿]=𝑎[𝛾][𝛿];
comprehension: for each Γ and 𝐴∈Ty(Γ), a context Γ.𝐴, a substitution 𝐩𝐴:Γ.𝐴→Γ and a term 𝐪𝐴∈Tm(Γ.𝐴,𝐴[𝐩𝐴]), universal: for every 𝛾:Δ→Γ and 𝑎∈Tm(Δ,𝐴[𝛾]) there is a unique ⟨𝛾,𝑎⟩:Δ→Γ.𝐴 with 𝐩𝐴∘⟨𝛾,𝑎⟩=𝛾,𝐪𝐴[⟨𝛾,𝑎⟩]=𝑎.
Equivalently (and this is Dybjer’s original formulation), items 2–3 are a functor 𝑇:Cop→𝐅𝐚𝐦. It sends Γ to (Ty(Γ),𝐴↦Tm(Γ,𝐴)) and 𝛾 to reindexing by 𝛾; identity and composition in 𝐅𝐚𝐦 unfold exactly to the four displayed substitution equations.
The first model is already concrete. Given a set Γ, take Ty(Γ) to be set-valued families on Γ, take Tm(Γ,𝐴) to be sections ∏𝑥:Γ𝐴(𝑥), and reindex both families and sections by precomposition. Comprehension is the dependent sum ∑𝑥:Γ𝐴(𝑥), with first projection and second component. The two displayed equations of definition 54.16 are then ordinary equations of functions; proposition 54.31 verifies the full structure.
The definition is definition 54.2 read backwards. The dictionary is exact, rule by rule:
Judgmental equality is modeled by equality of sets’ elements, not by isomorphism. All equations of definition 54.16 (and of the type-former structures below) are strict. This is what makes CwFs match syntax on the nose; the price is paid when connecting them to naturally occurring categorical structures, where everything holds only up to isomorphism and a coherence theorem is needed (cf. the biequivalence theorems of Clairambault–Dybjer [CCD21] and the local-universes construction [AG26]). For example, if reindexing is implemented by chosen pullbacks, the two objects representing (𝐴[𝛾])[𝛿] and 𝐴[𝛾∘𝛿] come with a canonical isomorphism from the pullback universal property, but need not be literally the same chosen object. A strict CwF requires this comparison to be equality and requires the identity and associativity comparisons to cohere.
Proof. If 𝑎∈Tm(Γ,𝐴)=Tm(Γ,𝐴[𝗂𝖽]) then ――𝑎:Γ→Γ.𝐴 is defined, and 𝐩𝐴∘――𝑎=𝗂𝖽 by the first comprehension equation. Conversely a section 𝛾 yields 𝐪𝐴[𝛾]∈Tm(Γ,𝐴[𝐩𝐴][𝛾])=Tm(Γ,𝐴[𝐩𝐴∘𝛾])=Tm(Γ,𝐴) by functoriality. The composites are the identities: 𝐪𝐴[――𝑎]=𝑎 is the second comprehension equation, and ――――𝐪𝐴[𝛾]=⟨𝐩𝐴∘𝛾,𝐪𝐴[𝛾]⟩=𝛾 by uniqueness of ⟨−,−⟩. ◻
Proof of Lemma 54.20 — Comprehension is a pullback
Proof. By the first comprehension equation and associativity, 𝐩𝐴∘𝛾+=𝐩𝐴∘⟨𝛾∘𝐩𝐴[𝛾],𝐪𝐴[𝛾]⟩=𝛾∘𝐩𝐴[𝛾], so the square commutes.
Let 𝛿:Ξ→Δ and 𝜎:Ξ→Γ.𝐴 satisfy 𝛾∘𝛿=𝐩𝐴∘𝜎. Functoriality gives 𝐪𝐴[𝜎]∈Tm(Ξ,𝐴[𝛾][𝛿]), because 𝐴[𝐩𝐴][𝜎]=𝐴[𝐩𝐴∘𝜎]=𝐴[𝛾∘𝛿]. Hence the candidate mediator is ℎ:=⟨𝛿,𝐪𝐴[𝜎]⟩:Ξ⟶Δ.𝐴[𝛾]. The first triangle is the first comprehension equation. For the second, lemma 116.10 and the two comprehension equations give 𝛾+∘ℎ=⟨𝛾∘𝛿,𝐪𝐴[𝜎]⟩=⟨𝐩𝐴∘𝜎,𝐪𝐴[𝜎]⟩=𝜎.
If ℎ′ satisfies the same triangles, comprehension uniqueness first gives ℎ′=⟨𝛿,𝐪[ℎ′]⟩. Reindexing 𝐪𝐴 along 𝛾+∘ℎ′=𝜎 and using Tm-Comp and the second comprehension equation gives 𝐪[ℎ′]=𝐪𝐴[𝜎]. Thus ℎ′=ℎ. ◻
The pullback calculation shows the fact used below: comprehension represents terms after reindexing. A map into Γ.𝐴 is uniquely a map 𝛾 into Γ together with a term of 𝐴[𝛾].
★★☆ Spell out the equivalence between items 2–3 of definition 54.16 and a functor 𝑇:Cop→𝐅𝐚𝐦: define 𝑇 on objects and morphisms and show that the functor laws are exactly the four displayed equations.
★★☆ Show that comprehensions are unique up to unique isomorphism: if (Γ.𝐴,𝐩,𝐪) and (𝐸,𝑝′,𝑞′) both satisfy item 4 of definition 54.16 for the same Γ, 𝐴, there is a unique isomorphism Γ.𝐴≅𝐸 commuting with the projections and generic terms.
★★☆ Reconstruct lemma 54.20 from the CwF equations. Given 𝛿:Ξ→Δ and 𝜎:Ξ→Γ.𝐴 with 𝛾∘𝛿=𝐩𝐴∘𝜎, start from ⟨𝛿,𝐪𝐴[𝜎]⟩ and check the two triangles before proving uniqueness.
A CwF models only the backbone of type theory. Each selected former becomes an extra structure on a CwF: the same operations as the rules, the same equations, plus strict stability under substitution. We give Π, Σ, 𝖨𝖽 and universes. Adding an inductive former requires a separately displayed algebraic operation and all of its equations.
A CwF supports Π-types if for all Γ, 𝐴∈Ty(Γ) and 𝐵∈Ty(Γ.𝐴) there are a type Π(𝐴,𝐵)∈Ty(Γ), an operation 𝜆:Tm(Γ.𝐴,𝐵)→Tm(Γ,Π(𝐴,𝐵)), and an operation assigning to 𝑓∈Tm(Γ,Π(𝐴,𝐵)) and 𝑎∈Tm(Γ,𝐴) a term 𝖺𝗉𝗉(𝑓,𝑎)∈Tm(Γ,𝐵[⟨𝗂𝖽,𝑎⟩]), subject to, for all 𝛾:Δ→Γ and appropriately typed arguments, 𝖺𝗉𝗉(𝜆(𝑏),𝑎)=𝑏[⟨𝗂𝖽,𝑎⟩],𝑓=𝜆(𝖺𝗉𝗉(𝑓[𝐩𝐴],𝐪𝐴)),Π(𝐴,𝐵)[𝛾]=Π(𝐴[𝛾],𝐵[𝛾+]),𝜆(𝑏)[𝛾]=𝜆(𝑏[𝛾+]),𝖺𝗉𝗉(𝑓,𝑎)[𝛾]=𝖺𝗉𝗉(𝑓[𝛾],𝑎[𝛾]). The 𝜂-equation typechecks because the comprehension equations give (𝐩𝐴)+∘⟨𝗂𝖽,𝐪𝐴⟩=𝗂𝖽: the weakening component is 𝐩𝐴, the variable component is 𝐪𝐴, and comprehension uniqueness identifies the resulting extension with 𝗂𝖽. Here 𝜆 is a typed CwF operation: its source already records 𝐴. Only the raw substitution-calculus constructor needs the explicit notation 𝜆(𝐴,𝑏).
A CwF supports Σ-types if for all Γ, 𝐴∈Ty(Γ), 𝐵∈Ty(Γ.𝐴) there are a type Σ(𝐴,𝐵)∈Ty(Γ) and operations (𝑎,𝑏)∈Tm(Γ,Σ(𝐴,𝐵)),𝗉𝗋1(𝑐)∈Tm(Γ,𝐴),𝗉𝗋2(𝑐)∈Tm(Γ,𝐵[⟨𝗂𝖽,𝗉𝗋1(𝑐)⟩]). Here 𝑎∈Tm(Γ,𝐴), 𝑏∈Tm(Γ,𝐵[⟨𝗂𝖽,𝑎⟩]), 𝑐∈Tm(Γ,Σ(𝐴,𝐵)), subject to 𝗉𝗋1(𝑎,𝑏)=𝑎, 𝗉𝗋2(𝑎,𝑏)=𝑏, (𝗉𝗋1(𝑐),𝗉𝗋2(𝑐))=𝑐, and strict stability: Σ(𝐴,𝐵)[𝛾]=Σ(𝐴[𝛾],𝐵[𝛾+]), (𝑎,𝑏)[𝛾]=(𝑎[𝛾],𝑏[𝛾]), 𝗉𝗋𝑖(𝑐)[𝛾]=𝗉𝗋𝑖(𝑐[𝛾]).
for all Γ, 𝐴∈Ty(Γ) and 𝑎,𝑏∈Tm(Γ,𝐴) there is a type 𝖨𝖽𝐴(𝑎,𝑏)∈Ty(Γ) with 𝖨𝖽𝐴(𝑎,𝑏)[𝛾]=𝖨𝖽𝐴[𝛾](𝑎[𝛾],𝑏[𝛾]);
for each 𝑎 there is 𝗋𝖾𝖿𝗅𝑎∈Tm(Γ,𝖨𝖽𝐴(𝑎,𝑎)) with 𝗋𝖾𝖿𝗅𝑎[𝛾]=𝗋𝖾𝖿𝗅𝑎[𝛾];
writing Γ𝐴:=Γ.𝐴.𝐴[𝐩] for the context of pairs, 𝐼𝐴:=𝖨𝖽𝐴[𝐩∘𝐩](𝐪[𝐩],𝐪)∈Ty(Γ𝐴) for the generic identity type, 𝛿𝐴:=⟨𝗂𝖽,𝐪⟩:Γ.𝐴→Γ𝐴 for the diagonal, and 𝑟𝐴:=⟨𝛿𝐴,𝗋𝖾𝖿𝗅𝐪⟩:Γ.𝐴⟶Γ𝐴.𝐼𝐴. This is well typed because 𝐼𝐴[𝛿𝐴]=𝖨𝖽𝐴[𝐩](𝐪,𝐪). For every 𝐶∈Ty(Γ𝐴.𝐼𝐴) and 𝑑∈Tm(Γ.𝐴,𝐶[𝑟𝐴]) there is a term 𝖩(𝐶,𝑑)∈Tm(Γ𝐴.𝐼𝐴,𝐶),𝖩(𝐶,𝑑)[𝑟𝐴]=𝑑, stable under substitution. For 𝛾:Δ→Γ, let 𝛾[2]𝐴:Δ𝐴[𝛾]→Γ𝐴 be the two successive lifts through the two copies of 𝐴, and let 𝛾[3]𝐴:Δ𝐴[𝛾].𝐼𝐴[𝛾]→Γ𝐴.𝐼𝐴 be its lift through the identity type. Then 𝖩(𝐶,𝑑)[𝛾[3]𝐴]=𝖩(𝐶[𝛾[3]𝐴],𝑑[𝛾+]).
The pointwise eliminator of definition 30.1 is recovered by substituting the concrete triple (𝑎,𝑏,𝑝) into 𝖩(𝐶,𝑑) with ⟨⟨⟨𝗂𝖽,𝑎⟩,𝑏⟩,𝑝⟩. In particular, 𝖩(𝐶,𝑑)[⟨⟨⟨𝗂𝖽,𝑎⟩,𝑏⟩,𝑝⟩]∈Tm(Γ,𝐶[⟨⟨⟨𝗂𝖽,𝑎⟩,𝑏⟩,𝑝⟩]). Reindexing the displayed stability equation gives its substitution law, and 𝖩(𝐶,𝑑)[𝑟𝐴]=𝑑 gives the reflexive computation rule.
A CwF supports the selected predicative hierarchy when, for every 𝑖 and context Γ, it has a stable type U𝑖∈Ty(Γ) and a stable decoding operation 𝖤𝗅()𝑖(𝑐)∈Ty(Γ)(𝑐∈Tm(Γ,U𝑖)),U𝑖[𝛾]=U𝑖,𝖤𝗅()𝑖(𝑐)[𝛾]=𝖤𝗅()𝑖(𝑐[𝛾]). The exact code operations required by SΠΣ𝖨𝖽𝖴 are ⌜Π⌝𝑖(𝑐,𝑑),⌜Σ⌝𝑖(𝑐,𝑑):U𝑖𝑐:U𝑖,𝑑:U𝑖overΓ.𝖤𝗅()𝑖(𝑐),⌜𝖨𝖽⌝𝑖(𝑐,𝑎,𝑏):U𝑖𝑐:U𝑖,𝑎,𝑏:𝖤𝗅()𝑖(𝑐),⌜U𝑖⌝:U𝑖+1. Their decoding equations are respectively 𝖤𝗅()𝑖(⌜Π⌝𝑖(𝑐,𝑑))=Π(𝖤𝗅()𝑖(𝑐),𝖤𝗅()𝑖(𝑑)),𝖤𝗅()𝑖(⌜Σ⌝𝑖(𝑐,𝑑))=Σ(𝖤𝗅()𝑖(𝑐),𝖤𝗅()𝑖(𝑑)),𝖤𝗅()𝑖(⌜𝖨𝖽⌝𝑖(𝑐,𝑎,𝑏))=𝖨𝖽𝖤𝗅()𝑖(𝑐)(𝑎,𝑏),𝖤𝗅()𝑖+1(⌜U𝑖⌝)=U𝑖. Every code is strictly stable under substitution: for Π and Σ, substitute 𝑐 by 𝛾 and 𝑑 by 𝛾+; for identity, substitute 𝑐,𝑎,𝑏 by 𝛾; ⌜U𝑖⌝ is constant. These are Tarski-style semantic data. The official Russell hierarchy of definition 29.1 is interpreted by the displayed decoding equations and its stated cumulative lifts; no further code former is implicit here.
An SΠΣ𝖨𝖽𝖴-model is a CwF with exactly the Π-, Σ-, intensional-identity-, and predicative universe structures of definition 54.21, definition 54.22, definition 54.23, definition 54.24, including every displayed strict substitution and computation equation. A morphism of such models must preserve all those operations and equations; the exact strict notion is displayed in definition 54.26 immediately before it is used. Adding another type former changes the signature and hence changes the category of models; no initiality or soundness result below silently ranges over such additions.
Π, Σ and 𝖨𝖽 above are specified by operations and equations, in bijection with the rules of definition 27.2, definition 27.9, definition 30.1: the point of the CwF language is that nothing else is needed. The structures can be repackaged as universal properties — e.g. Π-structure is a family of bijections Tm(Γ.𝐴,𝐵)≅Tm(Γ,Π(𝐴,𝐵)) natural in Γ, and 𝖨𝖽-structure with judgmental 𝖩-computation is weak orthogonality of 𝑟𝐴. The initiality theorem uses only the operation-and-equation presentation; universal-property formulations are developed in [AG26, CCD21].
★★☆ In definition 54.21, verify the 𝜂-equation’s well-typedness: show 𝑓[𝐩𝐴]∈Tm(Γ.𝐴,Π(𝐴[𝐩𝐴],𝐵[(𝐩𝐴)+])), that 𝖺𝗉𝗉(𝑓[𝐩𝐴],𝐪𝐴) has type 𝐵[(𝐩𝐴)+∘⟨𝗂𝖽,𝐪𝐴⟩], and that this substitution equals 𝗂𝖽.
★★★ Derive from definition 54.23 the pointwise rule: for 𝑎,𝑏∈Tm(Γ,𝐴), 𝑝∈Tm(Γ,𝖨𝖽𝐴(𝑎,𝑏)), and 𝐶, 𝑑 as in definition 30.1, a term 𝖩𝑎,𝑏,𝑝(𝐶,𝑑)∈Tm(Γ,𝐶[⟨⟨⟨𝗂𝖽,𝑎⟩,𝑏⟩,𝑝⟩]) satisfying the computation rule at 𝑏:=𝑎, 𝑝:=𝗋𝖾𝖿𝗅𝑎. Conversely, show that pointwise 𝖩with its stability equations yields the generic 𝖩 of definition 54.23.
Initiality means that for every model of the fixed signature there is exactly one strict morphism from the syntactic model to that model. The dictionary of section 54.3 has such a fixed point: syntax itself.
A tempting definition recurses directly on a named typing derivation: interpret its final rule from the interpretations of its premises. It is not yet a function on judgments. The same judgment may end with an inserted conversion, or with conversion pushed into a premise, and the two recursion trees need not be syntactically identical. One would first have to prove the coherence equation [[𝐷1]]raw=[[𝐷2]]rawwhenever𝐷1,𝐷2derivethesamejudgment. For the algebraic syntax, the repair is an indexed rule induction. It first interprets every derivable context, substitution, type, and term with all ambient indices present; simultaneously it proves that a different derivation of the same judgment gives the same result. Only then does the interpretation descend to judgmental-equality classes. Streicher’s alternative for named syntax is a partial interpretation followed by a definedness and coherence proof [Hof97, Str93].
Let C, D be CwFs. A strict morphism𝐹:C→D is a functor of underlying categories together with functions 𝐹:TyC(Γ)→TyD(𝐹Γ) and 𝐹:TmC(Γ,𝐴)→TmD(𝐹Γ,𝐹𝐴) such that 𝐹𝟏=𝟏, 𝐹(𝐴[𝛾])=𝐹𝐴[𝐹𝛾], 𝐹(𝑎[𝛾])=𝐹𝑎[𝐹𝛾], 𝐹(Γ.𝐴)=𝐹Γ.𝐹𝐴, 𝐹𝐩𝐴=𝐩𝐹𝐴, 𝐹𝐪𝐴=𝐪𝐹𝐴 (hence 𝐹⟨𝛾,𝑎⟩=⟨𝐹𝛾,𝐹𝑎⟩). When both CwFs carry type-former structure, 𝐹 is required to preserve it on the nose: 𝐹(Π(𝐴,𝐵))=Π(𝐹𝐴,𝐹𝐵), 𝐹(𝜆(𝑏))=𝜆(𝐹𝑏), and so on for each former.
Fix an SΠΣ𝖨𝖽𝖴-model C. Restore in every compressed rule of definition 54.2 the derivations of all presuppositions required by convention 26.14. There are simultaneous assignments 𝐷Γ:Γ𝖼𝗍𝗑hasvalue[[Γ]]𝐷Γ∈C,(𝐷Δ,𝐷𝛾,𝐷Γ):Δ⊢𝛾:Γhasvalue[[𝛾]]𝐷Δ,𝐷𝛾,𝐷Γ:[[Δ]]𝐷Δ⟶[[Γ]]𝐷Γ,(𝐷Γ,𝐷𝐴):Γ⊢𝐴𝗍𝗒𝗉𝖾hasvalue[[𝐴]]𝐷Γ,𝐷𝐴∈Ty([[Γ]]𝐷Γ),(𝐷Γ,𝐷𝐴,𝐷𝑎):Γ⊢𝑎:𝐴hasvalue[[𝑎]]𝐷Γ,𝐷𝐴,𝐷𝑎∈Tm([[Γ]]𝐷Γ,[[𝐴]]𝐷Γ,𝐷𝐴). They have the following two properties.
Every derivation of a substitution, type, or term equality is sent to literal equality of the corresponding arrows, types, or terms. Pairwise context equality from remark 54.4 is sent to literal equality of context objects.
If 𝐷 and 𝐷′ derive the same one of the four formation judgments, then their displayed interpretations are equal. More generally, this remains true when the two conclusions differ only by admissible context exchange or type conversion. In the substitution, type, and term cases, the equality is read after rewriting the domain, codomain, and ambient type by the equalities for those converted indices.
Thus the assignments depend on the derivable judgment, not on its derivation.
Proof of Lemma 116.32 — Indexed interpretation and derivation independence
Proof. Use simultaneous well-founded induction on derivation height; for the comparison claim use the sum of the two heights. The three claims are: formation derivations produce the four displayed, correctly sorted values; equality derivations produce literal semantic equalities; and two formation derivations of the same raw object at judgmentally equal indices produce equal values after those indices are rewritten. A conversion or context-exchange conclusion is administrative: its formation premise and its equality premise have smaller height. Interpret both by the induction hypotheses, rewrite by the equality obtained from the second premise, and keep the value obtained from the first. This deals in particular with a term whose final type has been changed by conversion.
After administrative conclusions have been removed, the outer constructor of the raw conclusion determines the final formation rule. Two derivations of the same raw object therefore have corresponding premises whose indices are judgmentally equal; the strengthened comparison induction identifies their interpretations after rewriting those indices. The representative dependent cases are as follows.
Context extension. From 𝐷Γ:Γ𝖼𝗍𝗑 and 𝐷𝐴:Γ⊢𝐴𝗍𝗒𝗉𝖾, put [[Γ.𝐴]]𝐶𝑡𝑥−𝐸𝑥𝑡(𝐷Γ,𝐷𝐴):=[[Γ]]𝐷Γ.[[𝐴]]𝐷Γ,𝐷𝐴. Both indices on the right are supplied by the displayed premises. If the two premise derivations change, their induction equalities make the two comprehensions literally equal. Pairwise context equality is handled by the same clause: equal interpretations of the shorter contexts and semantic soundness of the final type equality give equal context comprehensions.
Substitution extension. For premises 𝐷𝛾:Δ⊢𝛾:Γ, 𝐷𝐴:Γ⊢𝐴𝗍𝗒𝗉𝖾, and 𝐷𝑎:Δ⊢𝑎:𝐴[𝛾], define [[⟨𝛾,𝑎⟩]]:=⟨[[𝛾]],[[𝑎]]⟩:[[Δ]]⟶[[Γ]].[[𝐴]]. The semantic type of [[𝑎]] is [[𝐴]][[[𝛾]]] by the induction hypothesis for 𝐷𝑎; hence the semantic pairing operation has exactly this domain and codomain.
Reindexing. The conclusions of Sb-Ty and Sb-Tm are interpreted by [[𝐴[𝛾]]]:=[[𝐴]][[[𝛾]]],[[𝑎[𝛾]]]:=[[𝑎]][[[𝛾]]]. Their source context is the codomain of [[𝛾]], and their resulting ambient context is its domain. This records the indices that an unindexed recursion on raw trees would have omitted.
Dependent-product constructors. For 𝐷𝐴:Γ⊢𝐴𝗍𝗒𝗉𝖾 and 𝐷𝐵:Γ.𝐴⊢𝐵𝗍𝗒𝗉𝖾, define [[Π(𝐴,𝐵)]]:=Π([[𝐴]],[[𝐵]]). The context-extension case makes [[𝐵]] a type over [[Γ]].[[𝐴]], as the semantic operation requires. For 𝐷𝑏:Γ.𝐴⊢𝑏:𝐵, 𝐷𝑓:Γ⊢𝑓:Π(𝐴,𝐵), and 𝐷𝑎:Γ⊢𝑎:𝐴, the term constructors are [[𝜆(𝐴,𝑏)]]:=𝜆([[𝑏]]),[[𝖺𝗉𝗉(𝑓,𝑎)]]:=𝖺𝗉𝗉([[𝑓]],[[𝑎]]). The application has semantic type [[𝐵]][⟨𝗂𝖽,[[𝑎]]⟩], the interpretation of its syntactic result type. The Σ, identity, and universe constructors use the operations with those exact indices in definition 54.22–definition 54.24. Each premise is a shorter formation derivation, so the comparison cases decrease the same induction measure.
Equations. For Tm-Comp, the equality induction goal is exactly [[𝑎]][[[𝛾]]][[[𝛿]]]=[[𝑎]][[[𝛾]]∘[[𝛿]]], the term-reindexing equation of a CwF. The identity, category, and comprehension generators are proved by the corresponding equations in definition 54.16; the Π, Σ, identity, and universe generators are proved by the equations in definition 54.21, definition 54.22, definition 54.23, definition 54.24. Reflexivity, symmetry, and transitivity use the same properties of literal equality, and a congruence rule applies the relevant semantic operation to equal arguments.
These cases cover every possible final rule family: context formation; category and comprehension formation; reindexing; the four fixed type-former structures; equality closure; and conversion or context exchange. In each constructor case every premise derivation is shorter, while in each administrative case both the formation and equality premises are shorter. The simultaneous induction therefore proves correct sorting, equality soundness, and derivation independence together. ◻
contexts [Γ]: derivable contexts Γ𝖼𝗍𝗑, modulo the pairwise judgmental equality of their types (remark 54.4);
substitutions [Δ]⟶[Γ]: derivable judgments Δ′⊢𝛾:Γ′ with [Δ′]=[Δ] and [Γ′]=[Γ], modulo substitution equality after exchanging those endpoint representatives;
Ty([Γ]): derivable Γ′⊢𝐴𝗍𝗒𝗉𝖾 with [Γ′]=[Γ], modulo type equality after context exchange;
Tm([Γ],[𝐴]): derivable Γ′⊢𝑎:𝐴′ with [Γ′]=[Γ] and [𝐴′]=[𝐴], modulo term equality after context exchange and type conversion;
all operations induced by the syntactic constructors.
Then: (1) 𝕋 is a CwF supporting Π, Σ, intensional identity types, and the displayed universe hierarchy; (2) 𝕋 is initial: for every SΠΣ𝖨𝖽𝖴-model C (definition 116.28) there is exactly one strict structure-preserving morphism [[−]]:𝕋→C.
Proof of Theorem 54.27 — The term model and initiality
Proof. (1) Context exchange and conversion make the three indexed carriers independent of the endpoint, context, and type representatives chosen in the statement. Congruence then makes every constructor well-defined on their judgmental-equality classes. If [Γ] is a context and [𝐴]∈Ty([Γ]), define [Γ].[𝐴]:=[Γ.𝐴],𝑝[𝐴]:=[𝐩],𝑞[𝐴]:=[𝐪]. For [𝛾]:[Δ]→[Γ] and [𝑎]∈Tm([Δ],[𝐴[𝛾]]), define their pairing by ⟨[𝛾],[𝑎]⟩:=[⟨𝛾,𝑎⟩]. The rules Ext-Wk, Ext-Vz, and Ext-Uniq give the three comprehension equations. The category and reindexing equations are the corresponding identity, composition, and functoriality rules of definition 54.2. Finally, the operations of definition 54.9, definition 54.22, definition 54.23, definition 54.24 descend by congruence and satisfy their displayed substitution equations. Thus 𝕋 has the asserted CwF and type-former structure.
(2) Existence. Apply lemma 116.32. Its four assignments are independent of the chosen formation derivations, and its equality clause identifies judgmentally equal representatives. They therefore descend to functions on the four quotient carriers defining 𝕋. The clauses for identity, composition, comprehension, reindexing, and every fixed type former are the corresponding operations of C, so the resulting map is a strict SΠΣ𝖨𝖽𝖴-morphism.
Uniqueness. Let 𝐹:𝕋→C be another strict structure-preserving morphism. Simultaneous induction on well-sorted formation derivations gives 𝐹[Γ]=[[Γ]], 𝐹[𝛾]=[[𝛾]], 𝐹[𝐴]=[[𝐴]], and 𝐹[𝑎]=[[𝑎]]. In the context-extension case, strict preservation of comprehension and the induction hypotheses give 𝐹[Γ.𝐴]=𝐹[Γ].𝐹[𝐴]=[[Γ]].[[𝐴]]=[[Γ.𝐴]]. Strict preservation of pairing proves the substitution-extension case, and strict preservation of reindexing proves the explicit-action case. For Π, for instance, 𝐹[Π(𝐴,𝐵)]=Π(𝐹[𝐴],𝐹[𝐵])=Π([[𝐴]],[[𝐵]])=[[Π(𝐴,𝐵)]]; the other formers follow from their preservation equations. Hence 𝐹=[[−]]. ◻
Theorem 54.27 is strict algebraic initiality for syntax in which substitutions and all stability equations are constructors of the signature. It is not the stronger claim that an arbitrary named presentation, with substitution only a metalevel operation, is initial without a coherence proof. For comparison, de Boer’s formalization proves initiality for a fully annotated de Bruijn syntax with Π, Σ, identity, natural numbers, binary sums, empty and unit types, and an infinite universe hierarchy, using contextual categories and a partial interpretation followed by separate totality, substitution, and weakening theorems [dB20]. That source supports its own stated signature; we do not transfer it silently to ours. The named-to-algebraic soundness below uses only the forward translation in theorem 54.13; the unproved larger converse recorded there is not a hidden premise.
Let C be a CwF supporting Π, Σ, intensional identity types, and the displayed universe hierarchy. There is an interpretation [[−]] of every derivable judgment of TΠΣ𝖨𝖽𝖴 in the named syntax of definition 26.1 such that:
if Γ𝖼𝗍𝗑 then [[Γ]]∈C is defined;
if Γ⊢𝐴𝗍𝗒𝗉𝖾 then [[Γ;𝐴]]∈Ty([[Γ]]) is defined;
if Γ⊢𝑎:𝐴 then [[Γ;𝑎]]∈Tm([[Γ]],[[Γ;𝐴]]) is defined;
Proof of Theorem 54.28 — Soundness of the interpretation
Proof. Translate a named judgment by (−)∗ from construction 54.10. By theorem 54.13 its translation is a derivable algebraic judgment and named judgmental equality is preserved. Let 𝐹:𝕋→C be the unique strict morphism of theorem 54.27, and define [[Γ]]:=𝐹[Γ∗],[[Γ;𝐴]]:=𝐹[𝐴∗],[[Γ;𝑎]]:=𝐹[𝑎∗]. The sort assertions in clauses (1)–(3) are exactly the context, type, and term components of the strict morphism. If 𝐴≡𝐵 or 𝑎≡𝑏 in the named calculus, theorem 54.13(1) makes their translations equal in 𝕋; applying the function 𝐹 proves (4) or (5). This also proves independence of the chosen named derivation, since 𝕋 was quotiented by judgmental equality before 𝐹 was applied.
To identify this construction with the usual direct clauses, observe that strictness gives [[Γ,𝑥:𝐴;𝑥]]=𝐪 and [[Γ,𝑦:𝐵;𝑥]]=[[Γ;𝑥]][𝐩]; preservation of abstraction gives [[Γ;𝜆𝑥.𝑏]]=𝜆([[Γ,𝑥:𝐴;𝑏]]). Likewise, preservation of the identity structure sends 𝖩 to the operation of definition 54.23; its computation equation is therefore the strict CwF equation. Hence middle-of-context weakening, substitution, and 𝖩 are interpreted by the same strict morphism as the remaining clauses. ◻
The two named presentations of definition 26.22 — structural rules primitive, versus substitution and weakening admissible — derive exactly the same judgments.
Proof of Corollary 54.30 — Equivalence of structural presentations
Proof. By theorem 26.43, simultaneous admissibility transforms a derivation using primitive weakening, substitution, equal-term substitution, or context conversion into a derivation in the presentation where those rules are admissible. Conversely, every admissible use expands to the corresponding primitive rule instance. Thus a judgment is derivable in the first named presentation if and only if the same judgment is derivable in the second. ◻
★☆☆ Verify directly that 𝕋 satisfies item 4 of definition 54.16: the universal property of comprehension holds with ⟨𝛾,𝑎⟩ the syntactic extension, uniqueness being Ext-Uniq.
★★☆ For the Π-only fragment, write out the uniqueness argument of theorem 54.27(2). Let two strict morphisms be given: 𝐹,𝐺:𝕋→C Show by induction on a chosen representative that they agree on every equivalence class.
Initiality pays off only if there are models other than syntax. The set model validates everything of chapter 26–chapter 30 including definition 35.1; the groupoid model separates 𝖩 from uniqueness of identity proofs and closes the earlier external-model boundary.
Choose a hierarchy of strongly inaccessible cardinals 𝜅𝑖 and one outer Grothendieck universe V𝜔 containing every V𝑖=𝑉𝜅𝑖. These assumptions keep the set and groupoid universe models small; they were not used in the syntactic initiality argument.
In the metatheory of convention 116.17, convention 116.37, let V𝑖=𝑉𝜅𝑖 and use the outer Grothendieck universe V𝜔. There is a CwF 𝐒𝐞𝐭: contexts are the sets in V𝜔, substitutions are functions, Ty(Γ) is the set of functions 𝐴:Γ→V𝜔, Tm(Γ,𝐴)=∏𝛾∈Γ𝐴(𝛾), reindexing is precomposition, 𝟏 is a singleton, and Γ.𝐴:={(𝛾,𝑥)∣𝛾∈Γ,𝑥∈𝐴(𝛾)} with 𝐩(𝛾,𝑥)=𝛾 and 𝐪(𝛾,𝑥)=𝑥. It supports all the structure of section 54.4, with Π(𝐴,𝐵)(𝛾)=∏𝑥∈𝐴(𝛾)𝐵(𝛾,𝑥), Σ(𝐴,𝐵)(𝛾)=∑𝑥∈𝐴(𝛾)𝐵(𝛾,𝑥), 𝖨𝖽𝐴(𝑎,𝑏)(𝛾)={⋆∣𝑎(𝛾)=𝑏(𝛾)}, and U𝑖(𝛾)=V𝑖. The CwF itself is regarded as an object of a larger ambient collection; every context and comprehension it constructs remains in V𝜔.
Proof of Proposition 54.31 — The set model as a CwF
Proof. The comprehension property is direct: given 𝛾:Δ→Γ and 𝑎∈Tm(Δ,𝐴[𝛾]), the unique mediating function is 𝛿↦(𝛾(𝛿),𝑎(𝛿)). The former-wise equations were verified in definition 48.30; they hold on the nose. Note that this 𝖨𝖽 interprets even the extensional𝖤𝗊-rules of definition 35.1. Consequently the corresponding object theory is consistent relative to the ZFC plus inaccessible-cardinal assumptions of convention 116.37; this does not remove those metatheoretic hypotheses from corollary 90.7. ◻
A groupoid is a category all of whose morphisms are invertible. Here “small” means that its object set, arrow set, and structure maps belong to V𝜔 of convention 116.37; 𝐆𝐩𝐝𝜔 denotes the resulting set-sized-in-the-next-universe category of groupoids and functors. For a groupoid Γ, a family of groupoids𝐴 over Γ is a functor 𝐴:Γ→𝐆𝐩𝐝𝜔; for a functor 𝐹:Δ→Γ, reindexing is composition, 𝐴[𝐹]:=𝐴∘𝐹. A section𝑎 of 𝐴 assigns to each object 𝛾∈Γ an object 𝑎(𝛾)∈𝐴(𝛾) and to each morphism 𝑝:𝛾→𝛾′ a morphism 𝑎(𝑝):𝐴(𝑝)(𝑎(𝛾))→𝑎(𝛾′) in 𝐴(𝛾′), functorially: 𝑎(𝗂𝖽𝛾)=𝗂𝖽 and 𝑎(𝑞∘𝑝)=𝑎(𝑞)∘𝐴(𝑞)(𝑎(𝑝)).
Let 𝐴:Γ→𝐆𝐩𝐝𝜔 be a family and let 𝑎,𝑏 be sections of 𝐴. A vertical natural transformation𝛼:𝑎⇒𝑏 consists of arrows 𝛼𝛾:𝑎(𝛾)⟶𝑏(𝛾)in𝐴(𝛾) such that, for every 𝑝:𝛾→𝛾′ in Γ, 𝑏(𝑝)∘𝐴(𝑝)(𝛼𝛾)=𝛼𝛾′∘𝑎(𝑝).(𝑉𝑁𝑎𝑡) The identity has component 𝗂𝖽𝑎(𝛾), and vertical composition is componentwise: (𝛽⋅𝛼)𝛾:=𝛽𝛾∘𝛼𝛾. Functoriality of 𝐴 proves naturality of the identity, and composing the two instances of (VNat) proves naturality of 𝛽⋅𝛼. Every component is invertible because 𝐴(𝛾) is a groupoid. The inverse family (𝛼−1)𝛾:=(𝛼𝛾)−1 is natural because 𝑎(𝑝)∘𝐴(𝑝)(𝛼−1𝛾)VNat=𝛼−1𝛾′∘𝑏(𝑝)∘𝐴(𝑝)(𝛼𝛾)∘𝐴(𝑝)(𝛼−1𝛾)inverse=𝛼−1𝛾′∘𝑏(𝑝). Thus sections of 𝐴 and vertical natural transformations form a groupoid, denoted Sect(𝐴).
The CwF G has: contexts the groupoids, substitutions the functors, Ty(Γ) the families of definition 54.32, Tm(Γ,𝐴) the sections, both reindexed by composition; 𝟏 the one-object one-morphism groupoid; and comprehension the Grothendieck construction: Γ.𝐴 has objects the pairs (𝛾,𝑥) with 𝑥∈𝐴(𝛾) and morphisms (𝛾,𝑥)→(𝛾′,𝑥′) the pairs (𝑝,𝜑) with 𝑝:𝛾→𝛾′ and 𝜑:𝐴(𝑝)(𝑥)→𝑥′; 𝐩 is the projection functor 𝐩(𝛾,𝑥):=𝛾,𝐩(𝑝,𝜑):=𝑝, and 𝐪 is the section (𝛾,𝑥)↦𝑥, (𝑝,𝜑)↦𝜑.
Let T𝖦 be the intensional fragment with the structural rules, Π, Σ, intensional identity types, 𝟎, 𝟏, 𝟐, ℕ, and a predicative universe hierarchy, but without coproduct or W-types. Then G is a CwF supporting every former of T𝖦 and validates every rule of that fragment. The key clauses are:
Identity types are hom-sets:𝖨𝖽𝐴(𝑎,𝑏)(𝛾) is the discrete groupoid on the set hom𝐴(𝛾)(𝑎(𝛾),𝑏(𝛾)), with reindexing along 𝑝:𝛾→𝛾′ given by ℎ↦𝑏(𝑝)∘𝐴(𝑝)(ℎ)∘𝑎(𝑝)−1; 𝗋𝖾𝖿𝗅𝑎(𝛾)=𝗂𝖽𝑎(𝛾); and 𝖩(𝐶,𝑑) transports 𝑑 along the morphism (𝗂𝖽,𝗂𝖽,ℎ):(𝛾,𝑥,𝑥,𝗂𝖽)→(𝛾,𝑥,𝑥′,ℎ) of Γ𝐴.𝐼𝐴, so that 𝖩(𝐶,𝑑)[𝑟𝐴]=𝑑 holds on the nose.
Base types are discrete:𝟎, 𝟏, 𝟐, ℕ are the discrete groupoids on ∅, {⋆}, {0,1}, ℕ.
Universes: for each chosen inaccessible 𝜅𝑖, U𝑖 is the discrete groupoid on the set of groupoid structures whose data belong to 𝑉𝜅𝑖, with 𝖤𝗅(𝑐)(𝛾):=𝑐(𝛾).
Write 𝐵𝛾:𝐴(𝛾)→𝐆𝐩𝐝𝜔 for the restriction of 𝐵 along 𝑥↦(𝛾,𝑥) and ℎ↦(𝗂𝖽𝛾,ℎ). Then Π(𝐴,𝐵)(𝛾):=Sect(𝐵𝛾), with arrows exactly the vertical natural transformations of definition 116.40; Σ(𝐴,𝐵)(𝛾) is the Grothendieck construction of 𝐵𝛾 over 𝐴(𝛾).
Proof. We construct the operations and check their equations. The resulting derivation invariant says that a context is sent to a groupoid, a type over it to a groupoid-valued functor, a term to a section, and a judgmental equality to literal equality of the corresponding functors or sections. Induction on the last rule preserves this invariant by the construction named in the matching paragraph below; the displayed strict reindexing and computation equations handle conversion and computation rules.
The CwF. The terminal context is the terminal groupoid. Reindexing a family 𝐴 or a section 𝑎 along 𝐹:Δ→Γ is composition with 𝐹, so identity and composition are strict. Given 𝐹:Δ→Γ and a section 𝑎 of 𝐴[𝐹], define ⟨𝐹,𝑎⟩(𝛿):=(𝐹𝛿,𝑎𝛿),⟨𝐹,𝑎⟩(𝑟):=(𝐹𝑟,𝑎(𝑟)). The section laws make this a functor Δ→Γ.𝐴. Projection composed with it is 𝐹, and the generic term reindexed along it is 𝑎. Conversely, these two components determine its value on every object and arrow, so the mediating functor is unique. This proves the comprehension universal property.
Sums and products. At 𝛾, let Σ(𝐴,𝐵)(𝛾) be the Grothendieck construction of the restriction of 𝐵 to the fiber 𝐴(𝛾). Thus an object is (𝑥,𝑦) and an arrow is (ℎ,𝑘) with ℎ:𝑥→𝑥′,𝑘:𝐵(𝗂𝖽𝛾,ℎ)(𝑦)→𝑦′. For 𝑝:𝛾→𝛾′, apply 𝐴(𝑝) to the first component and apply 𝐵(𝑝,𝗂𝖽) to the second; functoriality of 𝐴 and 𝐵 proves the family laws. Pairing and the two projections act componentwise. Their two 𝛽-equations and the Σ-𝜂 equation are therefore literal equalities of objects and arrows, and all three operations commute with reindexing.
For products, use the section groupoid Sect(𝐵𝛾) of definition 116.40. Let 𝑝:𝛾→𝛾′ and 𝑥′∈𝐴(𝛾′), and write 𝑢𝑝,𝑥′:=(𝑝,𝗂𝖽𝑥′):(𝛾,𝐴(𝑝−1)(𝑥′))⟶(𝛾′,𝑥′) in Γ.𝐴. Transport a section 𝑠 of 𝐵𝛾 by (𝑝∗𝑠)(𝑥′):=𝐵(𝑢𝑝,𝑥′)(𝑠(𝐴(𝑝−1)(𝑥′))). For ℎ′:𝑥′→𝑦′, its section arrow is (𝑝∗𝑠)(ℎ′):=𝐵(𝑢𝑝,𝑦′)(𝑠(𝐴(𝑝−1)(ℎ′))). Its domain has first been rewritten by the commuting equation (𝗂𝖽𝛾′,ℎ′)∘𝑢𝑝,𝑥′=𝑢𝑝,𝑦′∘(𝗂𝖽𝛾,𝐴(𝑝−1)(ℎ′)) and functoriality of 𝐵. For a vertical transformation 𝛼:𝑠⇒𝑡, put (𝑝∗𝛼)𝑥′:=𝐵(𝑢𝑝,𝑥′)(𝛼𝐴(𝑝−1)(𝑥′)). Equation (VNat) for 𝑝∗𝛼 is the image under 𝐵 of the same commuting square, followed by the naturality equation for 𝛼. Hence 𝑝∗ is a functor between section groupoids. The equations (𝑞𝑝)∗=𝑞∗𝑝∗ and (𝗂𝖽)∗=𝗂𝖽 follow by expanding the definition and using (𝑞𝑝)−1=𝑝−1𝑞−1.
If 𝑡 is a section of 𝐵 over Γ.𝐴, define 𝜆(𝑡)(𝛾) by 𝜆(𝑡)(𝛾)(𝑥):=𝑡(𝛾,𝑥),𝜆(𝑡)(𝛾)(ℎ):=𝑡(𝗂𝖽𝛾,ℎ); its action on 𝑝:𝛾→𝛾′ is the vertical transformation whose 𝑥′-component is 𝑡(𝑢𝑝,𝑥′). Its naturality equation is the section law for 𝑡 applied to the commuting square used above.
At a fixed 𝛾, evaluation sends (𝑠,𝑥) to 𝑠(𝑥). An arrow (𝛼,ℎ):(𝑠,𝑥)→(𝑡,𝑦), where 𝛼:𝑠⇒𝑡 and ℎ:𝑥→𝑦, is sent to 𝑡(ℎ)∘𝐵𝛾(ℎ)(𝛼𝑥)=𝛼𝑦∘𝑠(ℎ); the equality is precisely (VNat). This fiberwise evaluation commutes with the transports 𝑝∗ by their displayed definitions. Consequently it is the application operation of the CwF. Hence 𝖺𝗉𝗉(𝜆(𝑡),𝑥)=𝑡(𝛾,𝑥) and 𝜆(𝑥.𝖺𝗉𝗉(𝑠,𝑥))=𝑠, on objects and arrows. These are the Π-𝛽 and Π-𝜂 equations. The definitions also show strict stability under reindexing.
Identity. Over an object (𝛾,𝑥,𝑦) of the context Γ,𝑥:𝐴,𝑦:𝐴, put 𝐼𝐴(𝛾,𝑥,𝑦):=disc(hom𝐴(𝛾)(𝑥,𝑦)). On a context arrow (𝑝,𝑞,𝑟):(𝛾,𝑥,𝑦)→(𝛾′,𝑥′,𝑦′) set 𝐼𝐴(𝑝,𝑞,𝑟)(ℎ):=𝑟∘𝐴(𝑝)(ℎ)∘𝑞−1. Identity and composition follow from cancellation and functoriality of 𝐴. The reflexivity section chooses 𝗂𝖽𝑥; the displayed conjugation sends it to 𝗂𝖽𝑥′, so reflexivity is natural.
It remains to verify 𝖩, including its morphism component. Let 𝐷 be the context of quadruples 𝑧=(𝛾,𝑥,𝑦,ℎ) and let 𝑟𝐴:Γ.𝐴→𝐷 be the reflexivity functor. Given a family 𝐶 over 𝐷 and a section 𝑑 of 𝐶[𝑟𝐴], define ℓ𝑧:=(𝗂𝖽𝛾,𝗂𝖽𝑥,ℎ,∗):𝑟𝐴(𝛾,𝑥)⟶𝑧,𝖩(𝐶,𝑑)(𝑧):=𝐶(ℓ𝑧)(𝑑(𝛾,𝑥)). For an arrow 𝑚=(𝑝,𝑞,𝑟,∗):𝑧→𝑧′ in 𝐷, discreteness of 𝐼𝐴 says exactly ℎ′=𝑟∘𝐴(𝑝)(ℎ)∘𝑞−1. Consequently the following two arrows in 𝐷 are equal: 𝑚∘ℓ𝑧=ℓ𝑧′∘𝑟𝐴(𝑝,𝑞). Apply 𝐶 to this equality and then to the naturality arrow 𝑑(𝑝,𝑞); this defines the arrow component of 𝖩(𝐶,𝑑) from 𝐶(𝑚)(𝖩(𝐶,𝑑)(𝑧)) to 𝖩(𝐶,𝑑)(𝑧′). Its identity and composition laws are those of 𝐶 and 𝑑. On the reflexivity locus ℓ𝑟𝐴(𝛾,𝑥) is an identity, on objects and arrows, so 𝖩(𝐶,𝑑)[𝑟𝐴]=𝑑 strictly. This proves every identity-type rule and not merely the object part of the eliminator.
Base types and universes. Interpret 𝟎,𝟏,𝟐,ℕ by the constant discrete groupoids on ∅,{⋆},{0,1},ℕ. Empty elimination is the unique section from an empty comprehension. Unit elimination, Boolean case analysis, and natural-number induction are defined fiberwise; their naturality follows respectively by uniqueness, by the two cases, and by meta-level induction on 𝑛. Their constructor equations are literal equalities. The singleton interpretation also validates the judgmental Unit-𝜂 rule.
Finally choose inaccessible cardinals 𝜅0<𝜅1<⋯. Let U𝑖 be the constant discrete groupoid of 𝜅𝑖-small groupoids and let the family 𝖤𝗅 over it have fiber 𝖤𝗅(𝑋)=𝑋. Discreteness makes its action on a universe arrow the identity functor. The constructions above preserve 𝜅𝑖-smallness, and 𝜅𝑗-small groupoids form an object of U𝑖 when 𝑗<𝑖; hence all stated universe formation and closure rules are validated. Therefore every derivable judgment of T𝖦 has an interpretation in G, and every judgmental equality is sent to literal equality of the interpreted data.
The construction is due to Hofmann and Streicher [Hof95]. Its scope restriction is essential: Hofmann explicitly says in §5.2.2.5 that arbitrary parameterized inductive definitions were not checked. The argument above therefore covers the stated fragment but not W-types. ◻
In G, let 𝔹 denote the groupoid with one object ∗ and hom(∗,∗)=ℤ/2ℤ={𝗂𝖽,𝑔}. Interpret the context Γ0:=(𝑋:U,𝑥:𝖤𝗅(𝑋),𝑝:𝖨𝖽𝖤𝗅(𝑋)(𝑥,𝑥)). Then the interpretation of the type Γ0⊢𝖨𝖽𝖨𝖽𝖤𝗅(𝑋)(𝑥,𝑥)(𝑝,𝗋𝖾𝖿𝗅𝑥)𝗍𝗒𝗉𝖾 has empty fiber over the object (⌜𝔹⌝,∗,𝑔)∈[[Γ0]]; consequently the type has no section, and the corresponding 𝖪-type (definition 30.28) is uninhabited in G. Likewise the 𝖴𝖨𝖯-type over (𝑋:U,𝑥,𝑦:𝖤𝗅(𝑋),𝑝,𝑞:𝖨𝖽𝖤𝗅(𝑋)(𝑥,𝑦)) is uninhabited.
Proof. Unfolding theorem 54.34: over the object (⌜𝔹⌝,∗,𝑔), the type 𝖨𝖽𝖤𝗅(𝑋)(𝑥,𝑥) is interpreted as the discrete groupoid on hom𝔹(∗,∗)={𝗂𝖽,𝑔}, and the displayed identity type as the discrete groupoid on the morphisms from 𝑔 to 𝗂𝖽 therein — the empty set, since in a discrete groupoid distinct objects have no morphisms between them and 𝑔≠𝗂𝖽. A section would pick an element of every fiber. For 𝖴𝖨𝖯, evaluate at (⌜𝔹⌝,∗,∗,𝗂𝖽,𝑔). ◻
In the fragment T𝖦 of theorem 54.34 there is no term of type ∏𝑋:U∏𝑥:𝖤𝗅(𝑋)∏𝑝:𝖨𝖽𝖤𝗅(𝑋)(𝑥,𝑥)𝖨𝖽𝖨𝖽𝖤𝗅(𝑋)(𝑥,𝑥)(𝑝,𝗋𝖾𝖿𝗅𝑥), nor of the 𝖴𝖨𝖯 type. Thus, relative to the ambient ZFC plus inaccessible hierarchy used to construct G, the eliminator 𝖪 is not derivable from 𝖩 in that fragment.
Proof of Corollary 54.36 — K and UIP are underivable
Proof. The derivation induction in the proof of theorem 54.34 would turn such a term into a section of its interpreted type. Evaluating the Π-clauses at the objects listed in proposition 54.35 would then produce an element of an empty set. ◻
The groupoid model validates function extensionality: two sections of a Π-family that are pointwise equal are equal, and the 𝖨𝖽-fibers of Π(𝐴,𝐵) compute accordingly. Hence G cannot establish remark 111.89; that boundary is recorded there as an open exact-signature transfer obligation rather than as a consequence of this model.
The groupoid model is the germ of homotopy type theory: it interprets types as 1-truncated homotopy types and suggests — as Hofmann and Streicher already noted — both that types could be interpreted as higher groupoids and that propositional equality of the universe could be isomorphism, a rule they proved sound in G. The stronger univalence axiom asks that the canonical map from equality of universe elements to equivalence of decoded types be an equivalence for every pair of universe elements; that axiom is not part of the fragment interpreted here [Hof95, Uni13].
★★☆ Verify in 𝐒𝐞𝐭 (proposition 54.31) the four equations of comprehension — the two triangle equations, naturality ⟨𝛾,𝑎⟩∘𝛿=⟨𝛾∘𝛿,𝑎[𝛿]⟩, and ⟨𝐩,𝐪⟩=𝗂𝖽 — and the Σ-structure equations of definition 54.22.
★★★ Show that every type of the fragment generated by 𝟎, 𝟏, 𝟐, ℕ, Π, Σ, 𝖨𝖽 (no universes) is interpreted in G, over any discrete context, by a discrete groupoid. Conclude that 𝖴𝖨𝖯holds for these types in G, so universes are essential to proposition 54.35.
The substitution calculus is Martin-Löf’s, from his unpublished 1992 Göteborg lectures “Substitution calculus” [ML92], with roots in the theory of expressions of [ML84] and in the context-morphism presentations of [NPS90, NPS00]. Categories with families were distilled from it by Dybjer [Dyb96], explicitly as an “internal type theory”: a generalized algebraic theory whose models are the semantic counterpart of the general rules. The survey [CCD21] develops the unityped–simply-typed–dependently-typed progression, the free (bi-)initial CwFs, and the biequivalences with Lawvere theories, cartesian closed categories and locally cartesian closed categories; its Theorems 6, 7 and 10 motivate the strict algebraic viewpoint but are not cited as an exact-signature proof of theorem 54.27. De Boer’s thesis and companion Agda development give the separate exact initiality result described in remark 116.34[dB20]. Hofmann’s chapter [Hof97] remains the most careful elementary account of the interpretation of named syntax (theorem 54.28), including the weakening and substitution lemmas and the partial-interpretation device, which is due to Streicher’s monograph on contextual categories; Streicher’s habilitation [Str93] initiated the study of intensionality criteria and the eliminator 𝖪. Alternative packagings of the same semantic data — categories with attributes, comprehension categories, display-map categories — are surveyed in [Jac99]; Angiuli–Gratzer [AG26] develop the natural-model formulation (representability of Tm∙→Ty) and the coherence problem for locally cartesian closed categories. The groupoid model (theorem 54.34) is Hofmann–Streicher’s; our elementary description follows [Hof95], ch. 5, where proposition 54.35 appears as the non-definability of uniqueness of identity and the isomorphism-as-equality rule for the universe is proved sound — the observation that, a decade later, grew into univalence [Uni13]. For the use of CwFs as the backbone of modern metatheory — gluing, canonicity, normalization — see the proved Π/𝟐 closed-canonicity case in theorem 49.2 and the separately scoped normalization imports recorded in chapter 49; for fuller developments, see the theses [Ang19, Ste21, Gra23].
Suggested first pass.
None of these problems is a prerequisite for a later chapter. Begin with exercise 116.20, then complete exercise 116.21.
★★★ For the CwF of set-valued families, write the interpretation morphism from the term CwF on contexts, substitutions, types, and terms. Verify the comprehension square and prove uniqueness by induction over the four sorts.
★★★Practical project.explicit-substitution-normalizer Implement in Agda or Kappa the rewrite system of definition 54.2. Maintain well-scoped de Bruijn indices and a strictly decreasing rule measure. Normalize identity, associativity, and lift-after-extension examples to the forms predicted by lemma 54.12; reject an ill-scoped lift. Mutation test: reversing one composition rule must be detected as a cycle.
Diagram commutes and is a pullback in