Suppose 𝑝 identifies 𝑎 with 𝑏 and 𝑢:𝐵[𝑎/𝑥]. In the intensional theory the passage from 𝑢 to the fiber 𝐵[𝑏/𝑥] is recorded by the term 𝗍𝗋𝑝(𝑢). Extensional type theory makes a different choice: from 𝑝 it admits the judgment 𝑎≡𝑏, after which conversion regards the unchanged term 𝑢 as an element of 𝐵[𝑏/𝑥].
The extensional equality type𝖤𝗊𝐴(𝑎,𝑏) has reflexivity as its proof and reflects an inhabitant into judgmental equality. Equality reflection turns 𝑝:𝖤𝗊𝐴(𝑎,𝑏) into 𝑎≡𝑏, so conversion moves terms between the two fibers without an explicit transport.
The extensional delta
The equality type internalizes the judgment Γ⊢𝑎≡𝑏:𝐴 itself, not a proof-relevant approximation of it.
Extend the binding signature by the type former 𝖤𝗊𝐴(𝑎,𝑏) of arity (0,0,0) and an annotated constructor 𝖾𝗊𝗋𝖾𝖿𝗅𝑎 of arity (0). The constructor 𝖾𝗊𝗋𝖾𝖿𝗅𝑎 is printed 𝗋𝖾𝖿𝗅 when its endpoint is determined by the expected type. The extensional equality former 𝖤𝗊𝐴(𝑎,𝑏) is distinct from the intensional identity type 𝖨𝖽𝐴(𝑎,𝑏) of definition 30.1, which the base theory retains.
The theory ETT extends the base by the type former 𝖤𝗊𝐴(𝑎,𝑏), governed by the following rules (premises compressed per convention 26.14).
Γ⊢𝑎:𝐴Γ⊢𝑏:𝐴
Γ⊢𝖤𝗊𝐴(𝑎,𝑏)𝗍𝗒𝗉𝖾
Eq-F
Γ⊢𝑎:𝐴
Γ⊢𝗋𝖾𝖿𝗅:𝖤𝗊𝐴(𝑎,𝑎)
Eq-I
Γ⊢𝑝:𝖤𝗊𝐴(𝑎,𝑏)
Γ⊢𝑎≡𝑏:𝐴
Eq-Reflect
Γ⊢𝑝:𝖤𝗊𝐴(𝑎,𝑏)
Γ⊢𝑝≡𝗋𝖾𝖿𝗅:𝖤𝗊𝐴(𝑎,𝑏)
Eq-Uniq
When the base contains the Russell universes of definition 29.1, equality propositions are small whenever their ambient type is small:
The classified congruence instances for the new raw operators are
Γ⊢𝐴≡𝐴′𝗍𝗒𝗉𝖾Γ⊢𝑎≡𝑎′:𝐴Γ⊢𝑏≡𝑏′:𝐴
Γ⊢𝖤𝗊𝐴(𝑎,𝑏)≡𝖤𝗊𝐴′(𝑎′,𝑏′)𝗍𝗒𝗉𝖾
Eq-F-eq
Γ⊢𝑎≡𝑎′:𝐴
Γ⊢𝖾𝗊𝗋𝖾𝖿𝗅𝑎≡𝖾𝗊𝗋𝖾𝖿𝗅𝑎′:𝖤𝗊𝐴(𝑎,𝑎)
Eq-I-eq
In the second conclusion the right-hand term and its natural classifier are first converted along Eq-F-eq. The conclusions of Eq-Reflect and Eq-Uniq are likewise stable under conversion of their premises. These are the congruence facts used below.
The conclusion of Eq-Uniq equates 𝑝 with 𝗋𝖾𝖿𝗅 at the type 𝖤𝗊𝐴(𝑎,𝑏), although Eq-I gives 𝗋𝖾𝖿𝗅 the type 𝖤𝗊𝐴(𝑎,𝑎). The rule is nevertheless well posed: from the premise, Eq-Reflect yields 𝑎≡𝑏, hence Γ⊢𝖤𝗊𝐴(𝑎,𝑎)≡𝖤𝗊𝐴(𝑎,𝑏)𝗍𝗒𝗉𝖾 by congruence, and 𝗋𝖾𝖿𝗅 inhabits 𝖤𝗊𝐴(𝑎,𝑏) by conversion. Thus Eq-Uniq presupposes Eq-Reflect; the two rules cannot be adopted separately in this formulation.
Under convention 48.28, let V0∈V1∈⋯ be the resulting sequence as in lemma 74.14. The set interpretation of the Russell hierarchy, extended to intensional identity types as in proposition 77.32, extends further to the extensional equality rules. Consequently, relative to those set-theoretic assumptions, ETT with Russell universes has no closed term of 𝟎, and 𝗍𝗍≢𝖿𝖿 remains valid after adding reflection.
Proof of Proposition 35.4 — A separating set interpretation
Proof. First use the extension of proposition 77.32: interpret an identity type by the singleton when its endpoints have equal denotations and by the empty set otherwise. Reflexivity denotes the unique element; 𝖩 is well defined because an inhabitant forces the two endpoints to have the same denotation, and its reflexivity clause is literal.
At level 𝑖, continue that interpretation by putting [[𝖤𝗊𝐴(𝑎,𝑏)]]𝜌:={∗∣[[𝑎]]𝜌=[[𝑏]]𝜌}. Thus an equality type is either empty or a singleton. Reflexivity denotes ∗. An inhabitant forces the endpoint denotations to be equal, validating Eq-Reflect; any two inhabitants denote the unique element, validating Eq-Uniq. Both fibers lie in V𝑖: they are subsets of the singleton {∗}∈V𝑖, and a Grothendieck universe is closed under subsets. Thus Eq-Form-U is sound at every level. Ordinary substitution of set families validates substitution and congruence.
The interpretations of 𝟎, 𝗍𝗍, and 𝖿𝖿 have not changed: they are ∅, 1, and 0. Soundness therefore gives the two separation conclusions. ◻
The set model is the composite of the interpretations in definition 28.12, lemma 74.14, proposition 77.32, proposition 35.4. The name includes exactly those four stages; it does not silently add a quotient, a simplicial interpretation, or a univalent universe.
Eq-Reflect concludes an equality judgment from the mere existence of a term. Three observations measure its strength. (i) Judgmentally equal terms may be exchanged silently at any position of any judgment, by conversion and the classified congruence scheme of definition 26.36, convention 27.1. (ii) The proof 𝑝 is not recorded in such exchanges: the conclusion 𝑎≡𝑏 retains no trace of it. (iii) The premise does not require 𝑝 to be closed or canonical; 𝑝 may be a variable, so any hypothesis of equality type acts on the judgmental equality of the entire context. This observation concerns the rule itself; the undecidability proof below is a separate reduction.
Let Γ,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾, Γ⊢𝑝:𝖤𝗊𝐴(𝑎,𝑏) and Γ⊢𝑢:𝐵[𝑎/𝑥]. Then 𝑢 itself inhabits 𝐵[𝑏/𝑥] — transport is the identity. In the base, the same passage requires the transport construction 𝗍𝗋 of construction 30.9 and leaves a mark on the term. Rule names for the structural rules as in definition 26.22:
Proof of Theorem 35.7 — Eq internalizes judgmental equality
Proof. (1) If Γ⊢𝑝:𝖤𝗊𝐴(𝑎,𝑏), then Γ⊢𝑎≡𝑏:𝐴 by Eq-Reflect. Conversely, if Γ⊢𝑎≡𝑏:𝐴, then Γ⊢𝖤𝗊𝐴(𝑎,𝑎)≡𝖤𝗊𝐴(𝑎,𝑏)𝗍𝗒𝗉𝖾 by congruence for Eq-F, and Γ⊢𝗋𝖾𝖿𝗅:𝖤𝗊𝐴(𝑎,𝑎) by Eq-I, so Γ⊢𝗋𝖾𝖿𝗅:𝖤𝗊𝐴(𝑎,𝑏) by Conv. (2) If 𝑝,𝑞 both inhabit 𝖤𝗊𝐴(𝑎,𝑏), then 𝑝≡𝗋𝖾𝖿𝗅 and 𝑞≡𝗋𝖾𝖿𝗅 by Eq-Uniq. The inverse of the second judgment is 𝗋𝖾𝖿𝗅≡𝑞; composing it with the first gives 𝑝≡𝑞. ◻
𝖤𝗊 is the one former of this book with no type-valued elimination rule: it has formation and introduction rules, but no ordinary elimination or computation rules. Eq-Reflect occupies the place of elimination — it eliminates into the judgmental level rather than into types — and Eq-Uniq is an 𝜂-law. An eliminator in the style of 𝖩 is derivable, with a judgmental computation rule (theorem 35.9(iii)), so nothing is lost. Conversely, suppose the other three rules are joined by a 𝖩-eliminator. In context 𝑥,𝑦:𝐴,𝑞:𝖤𝗊𝐴(𝑥,𝑦), reflection makes 𝐶(𝑥,𝑦,𝑞):=𝖤𝗊𝖤𝗊𝐴(𝑥,𝑦)(𝑞,𝗋𝖾𝖿𝗅) well formed. The reflexivity branch is 𝗋𝖾𝖿𝗅:𝐶(𝑥,𝑥,𝗋𝖾𝖿𝗅), so 𝖩 gives 𝐶(𝑎,𝑏,𝑝) for every 𝑝:𝖤𝗊𝐴(𝑎,𝑏). Reflecting that inhabitant gives 𝑝≡𝗋𝖾𝖿𝗅; this is Eq-Uniq. Thus the derivation belongs to the main line; exercise 35.2 reconstructs its rule tree.
★★☆ Exhibit the following rule as the instance of the classified congruence scheme of definition 26.36 for the parameter telescope (𝐴𝗍𝗒𝗉𝖾;𝑎:𝐴;𝑏:𝐴): if Γ⊢𝐴≡𝐴′𝗍𝗒𝗉𝖾, Γ⊢𝑎≡𝑎′:𝐴 and Γ⊢𝑏≡𝑏′:𝐴, then Γ⊢𝖤𝗊𝐴(𝑎,𝑏)≡𝖤𝗊𝐴′(𝑎′,𝑏′)𝗍𝗒𝗉𝖾. Conclude that Γ⊢𝗋𝖾𝖿𝗅:𝖤𝗊𝐴(𝑎,𝑏) whenever Γ⊢𝑎≡𝑏:𝐴.
★★☆ Consider the base extended by Eq-F, Eq-I, Eq-Reflect and a 𝖩-style eliminator for 𝖤𝗊 (formulate its rules following definition 30.1), but withoutEq-Uniq. Show that Eq-Uniq is derivable. Hint: the family 𝐶(𝑥,𝑦,𝑞):=𝖤𝗊𝖤𝗊𝐴(𝑥,𝑦)(𝑞,𝗋𝖾𝖿𝗅) is well formed thanks to Eq-Reflect applied to the variable 𝑞; eliminate, then reflect.
★★☆ Using Eq-Reflect but not 𝖩, construct terms 𝗌𝗒𝗆:𝖤𝗊𝐴(𝑎,𝑏)→𝖤𝗊𝐴(𝑏,𝑎),𝗍𝗋𝖺𝗇𝗌:𝖤𝗊𝐴(𝑎,𝑏)→𝖤𝗊𝐴(𝑏,𝑐)→𝖤𝗊𝐴(𝑎,𝑐), and show that every application of either is judgmentally equal to 𝗋𝖾𝖿𝗅.
The base signature contains neither 𝖪 nor function extensionality; definition 30.35 therefore treated the latter as an additional principle. ETT proves both. No underivability claim is a premise here; a later groupoid countermodel separates 𝖪 from 𝖩 for its exact universe/Π/Σ/base-type fragment.
(UIP) If Γ⊢𝑝:𝖤𝗊𝐴(𝑎,𝑏) and Γ⊢𝑞:𝖤𝗊𝐴(𝑎,𝑏), then Γ⊢𝑝≡𝑞:𝖤𝗊𝐴(𝑎,𝑏); moreover the internal statement 𝖤𝗊𝖤𝗊𝐴(𝑎,𝑏)(𝑝,𝑞) is inhabited (by 𝗋𝖾𝖿𝗅).
(Function extensionality) If Γ⊢𝑓:∏𝑥:𝐴𝐵, Γ⊢𝑔:∏𝑥:𝐴𝐵 and Γ⊢ℎ:∏𝑥:𝐴𝖤𝗊𝐵(𝑓𝑥,𝑔𝑥), then Γ⊢𝑓≡𝑔:∏𝑥:𝐴𝐵; moreover 𝖤𝗊∏𝑥:𝐴𝐵(𝑓,𝑔) is inhabited (by 𝗋𝖾𝖿𝗅).
(𝖩 and 𝖪 definable) Let Γ,𝑥:𝐴,𝑦:𝐴,𝑞:𝖤𝗊𝐴(𝑥,𝑦)⊢𝐶𝗍𝗒𝗉𝖾 and Γ,𝑥:𝐴⊢𝑐:𝐶[𝑥,𝑥,𝗋𝖾𝖿𝗅/𝑥,𝑦,𝑞]. Then for all Γ⊢𝑎:𝐴, Γ⊢𝑏:𝐴, Γ⊢𝑝:𝖤𝗊𝐴(𝑎,𝑏), the term 𝖩(𝑥.𝑐;𝑎,𝑏,𝑝):=𝑐[𝑎/𝑥] satisfies Γ⊢𝑐[𝑎/𝑥]:𝐶[𝑎,𝑏,𝑝/𝑥,𝑦,𝑞] and computes judgmentally: 𝖩(𝑥.𝑐;𝑎,𝑎,𝗋𝖾𝖿𝗅)≡𝑐[𝑎/𝑥]. For the 𝖪 construction, suppose Γ,𝑥:𝐴,𝑞:𝖤𝗊𝐴(𝑥,𝑥)⊢𝐷𝗍𝗒𝗉𝖾, Γ,𝑥:𝐴⊢𝑑:𝐷[𝗋𝖾𝖿𝗅/𝑞], Γ⊢𝑎:𝐴, and Γ⊢𝑝:𝖤𝗊𝐴(𝑎,𝑎), define 𝖪(𝑥.𝑞.𝐷;𝑥.𝑑;𝑎,𝑝):=𝑑[𝑎/𝑥]:𝐷[𝑎/𝑥,𝑝/𝑞]. Then 𝖪(𝑥.𝑞.𝐷;𝑥.𝑑;𝑎,𝗋𝖾𝖿𝗅)≡𝑑[𝑎/𝑥].
Proof of Theorem 35.9 — Consequences of reflection
Proof. (1) By Eq-Uniq, 𝑝≡𝗋𝖾𝖿𝗅≡𝑞. Internalization gives the term 𝗋𝖾𝖿𝗅:𝖤𝗊𝖤𝗊𝐴(𝑎,𝑏)(𝑝,𝑞).
(2) In the context Γ,𝑥:𝐴 we have Γ,𝑥:𝐴⊢ℎ𝑥:𝖤𝗊𝐵(𝑓𝑥,𝑔𝑥), so Γ,𝑥:𝐴⊢𝑓𝑥≡𝑔𝑥:𝐵 by Eq-Reflect. By the rule 𝜆-eq (remark 27.4), Γ⊢𝜆𝑥.𝑓𝑥≡𝜆𝑥.𝑔𝑥:∏𝑥:𝐴𝐵, and by the 𝜂-rule for Π (definition 27.2) 𝑓≡𝜆𝑥.𝑓𝑥 and 𝑔≡𝜆𝑥.𝑔𝑥; hence 𝑓≡𝑔 by transitivity. Apply theorem 35.7(1) for the internal statement.
(3) We have Γ⊢𝑐[𝑎/𝑥]:𝐶[𝑎,𝑎,𝗋𝖾𝖿𝗅/𝑥,𝑦,𝑞] by the substitution rule. From 𝑝, Eq-Reflect gives 𝑎≡𝑏 and Eq-Uniq gives 𝑝≡𝗋𝖾𝖿𝗅, so Γ⊢𝐶[𝑎,𝑎,𝗋𝖾𝖿𝗅/𝑥,𝑦,𝑞]≡𝐶[𝑎,𝑏,𝑝/𝑥,𝑦,𝑞]𝗍𝗒𝗉𝖾 by congruence, and Conv concludes the typing. The computation rule 𝖩(𝑥.𝑐;𝑎,𝑎,𝗋𝖾𝖿𝗅)≡𝑐[𝑎/𝑥] holds because the left-hand side is defined to be the right-hand side.
For 𝖪, substitution gives 𝑑[𝑎/𝑥]:𝐷[𝑎/𝑥,𝗋𝖾𝖿𝗅/𝑞]. Rule Eq-Uniq gives 𝑝≡𝗋𝖾𝖿𝗅, so dependent congruence and conversion change this classifier to 𝐷[𝑎/𝑥,𝑝/𝑞]. The reflexivity equation is judgmental because the displayed 𝖪 was defined to be 𝑑[𝑎/𝑥]. ◻
In ETT, the intensional identity type of definition 30.1 satisfies reflection and uniqueness as derived rules: if Γ⊢𝑝:𝖨𝖽𝐴(𝑎,𝑏), then Γ⊢𝑎≡𝑏:𝐴 and Γ⊢𝑝≡𝗋𝖾𝖿𝗅:𝖨𝖽𝐴(𝑎,𝑏). Consequently 𝖨𝖽𝐴(𝑎,𝑏) and 𝖤𝗊𝐴(𝑎,𝑏) are inhabited in exactly the same contexts, and each inhabitant of either is judgmentally equal to 𝗋𝖾𝖿𝗅.
Proof of Proposition 35.10 — Collapse of the identity type
Proof. Define 𝑒:=𝜆𝑝.𝖩(𝑥.𝑦.𝑞.𝖤𝗊𝐴(𝑥,𝑦);𝑧.𝗋𝖾𝖿𝗅;𝑝):𝖨𝖽𝐴(𝑎,𝑏)→𝖤𝗊𝐴(𝑎,𝑏), using the primitive 𝖩 with motive 𝖤𝗊𝐴(𝑥,𝑦) and reflexivity clause 𝑧.𝗋𝖾𝖿𝗅; here 𝖩 is the primitive eliminator of definition 30.1. Given Γ⊢𝑝:𝖨𝖽𝐴(𝑎,𝑏), we obtain Γ⊢𝑒𝑝:𝖤𝗊𝐴(𝑎,𝑏) and hence 𝑎≡𝑏 by Eq-Reflect.
Conversely, if 𝑟:𝖤𝗊𝐴(𝑎,𝑏), reflection gives 𝑎≡𝑏; hence 𝗋𝖾𝖿𝗅𝑎:𝖨𝖽𝐴(𝑎,𝑎) converts to an inhabitant of 𝖨𝖽𝐴(𝑎,𝑏). This proves the asserted equivalence of inhabitation.
For uniqueness, consider the family Γ,𝑥:𝐴,𝑦:𝐴,𝑞:𝖨𝖽𝐴(𝑥,𝑦)⊢𝖨𝖽𝖨𝖽𝐴(𝑥,𝑦)(𝑞,𝗋𝖾𝖿𝗅)𝗍𝗒𝗉𝖾. It is well formed: applying 𝑒 to the variable𝑞 and reflecting gives 𝑥≡𝑦 in its context. Hence 𝖨𝖽𝐴(𝑥,𝑥)≡𝖨𝖽𝐴(𝑥,𝑦) as types, and 𝗋𝖾𝖿𝗅𝑥:𝖨𝖽𝐴(𝑥,𝑦) by conversion. The base case 𝗋𝖾𝖿𝗅:𝖨𝖽𝖨𝖽𝐴(𝑥,𝑥)(𝗋𝖾𝖿𝗅,𝗋𝖾𝖿𝗅) is available, so 𝖩 yields Γ⊢𝑤:𝖨𝖽𝖨𝖽𝐴(𝑎,𝑏)(𝑝,𝗋𝖾𝖿𝗅). Applying 𝑒 at the type 𝖨𝖽𝐴(𝑎,𝑏) and reflecting once more gives 𝑝≡𝗋𝖾𝖿𝗅. ◻
In ETT, every operation of the groupoid structure of theorem 30.20 — symmetry, transitivity, 𝖺𝗉, transport — is judgmentally equal to a constant function returning 𝗋𝖾𝖿𝗅 (respectively, for transport, to the identity function): for instance 𝗍𝗋𝐵𝑝(𝑢)≡𝑢 for every 𝑝 and 𝑢.
Proof of Corollary 35.11 — The groupoid structure trivializes
Proof. Each operation is defined by 𝖩 from a base case (theorem 30.20). By proposition 35.10, every path argument is judgmentally 𝗋𝖾𝖿𝗅. Hence 𝑝−1𝑝𝑟𝑜𝑝𝑜𝑠𝑖𝑡𝑖𝑜𝑛35.10≡𝗋𝖾𝖿𝗅−1𝐼𝑑−𝑐𝑜𝑚𝑝≡𝗋𝖾𝖿𝗅,𝑝⋅𝑞𝑝𝑟𝑜𝑝𝑜𝑠𝑖𝑡𝑖𝑜𝑛35.10≡𝗋𝖾𝖿𝗅⋅𝗋𝖾𝖿𝗅𝐼𝑑−𝑐𝑜𝑚𝑝≡𝗋𝖾𝖿𝗅,𝖺𝗉𝑓(𝑝)𝑝𝑟𝑜𝑝𝑜𝑠𝑖𝑡𝑖𝑜𝑛35.10≡𝖺𝗉𝑓(𝗋𝖾𝖿𝗅)𝐼𝑑−𝑐𝑜𝑚𝑝≡𝗋𝖾𝖿𝗅. Likewise 𝗍𝗋𝐵𝑝(𝑢)𝑝𝑟𝑜𝑝𝑜𝑠𝑖𝑡𝑖𝑜𝑛35.10≡𝗍𝗋𝐵𝗋𝖾𝖿𝗅(𝑢)𝐼𝑑−𝑐𝑜𝑚𝑝≡𝑢. For example, the right-unit law reduces to 𝑝⋅𝗋𝖾𝖿𝗅𝑏𝑝𝑟𝑜𝑝𝑜𝑠𝑖𝑡𝑖𝑜𝑛35.10≡𝗋𝖾𝖿𝗅𝑎⋅𝗋𝖾𝖿𝗅𝑎𝐼𝑑−𝑐𝑜𝑚𝑝≡𝗋𝖾𝖿𝗅𝑎𝑝𝑟𝑜𝑝𝑜𝑠𝑖𝑡𝑖𝑜𝑛35.10≡𝑝. The inverse, left-unit, associativity, and action laws reduce by the same three displayed computations. ◻
Equality reflection derives 𝖪. The derivation is clause (3) of theorem 35.9. The groupoid countermodel refutes 𝖪 in the corresponding intensional fragment. Equality reflection therefore strictly strengthens that fragment. The exact core signature in which reflection has the same inhabitation strength as UIP plus function extensionality is stated in section 35.4.
★★☆ Use the derived 𝖪 from theorem 35.9(3), with motive 𝐷(𝑥,𝑝):=𝖤𝗊𝖤𝗊𝐴(𝑥,𝑥)(𝑝,𝗋𝖾𝖿𝗅). Compare the resulting inhabitant with the direct inhabitant given by Eq-Uniq. Internalize their equality using theorem 35.7.
★★☆ Write out the conversions in 𝗍𝗋𝐵𝑝⋅𝑞(𝑢)≡𝗍𝗋𝐵𝑞(𝗍𝗋𝐵𝑝(𝑢)) explicitly: first replace 𝑝,𝑞 by reflexivity using proposition 35.10, then cite the two relevant 𝖩 computation rules. Repeat for (𝑝⋅𝑞)−1≡𝑞−1⋅𝑝−1.
★★☆ Define 𝗁𝖺𝗉𝗉𝗅𝗒:𝖤𝗊∏𝑥:𝐴𝐵(𝑓,𝑔)→∏𝑥:𝐴𝖤𝗊𝐵(𝑓𝑥,𝑔𝑥) without 𝖩, and show that 𝗁𝖺𝗉𝗉𝗅𝗒 and the function 𝖿𝗎𝗇𝖾𝗑𝗍:=𝜆ℎ.𝗋𝖾𝖿𝗅 of theorem 35.9(2) are mutually inverse, both composites being judgmentally equal to identity functions.
Under propositions-as-types, 𝟏, 𝟎, Π, × and → model ⊤, ⊥, ∀, ∧ and ⊃; but Σ and + overshoot ∃ and ∨, because their inhabitants carry more information than the bare truth of the proposition. This section delimits the types that behave as propositions and adds the connective that discards the surplus.
Being a proposition is a judgment about the generic pair of elements of 𝐴, and is therefore stable under substitution and weakening, as every judgment is. It is not the condition “𝐴 has at most one closed inhabitant”. With the universes of definition 29.1, take the type 𝑋 in context 𝑋:U0. It has no inhabitants: one would specialize under 𝑋:=𝟎 to an inhabitant of 𝟎. Yet it is not a proposition: propositionhood is preserved by the substitution 𝑋:=𝟐, and 𝟐 is not a proposition (lemma 35.15(v)).
Proof. (1) By Eq-Uniq, both generic inhabitants are judgmentally equal to 𝗋𝖾𝖿𝗅.
(2) For 𝟏: 𝑥≡⋆≡𝑦 by the 𝜂-rule in definition 27.14. For 𝟎: in the context Γ,𝑥:𝟎,𝑦:𝟎 the term 𝗋𝖾𝖼𝟎(𝑥) inhabits 𝖤𝗊𝟎(𝑥,𝑦), and Eq-Reflect concludes 𝑥≡𝑦. (Note the use of reflection: in the base, 𝟎 is a proposition only propositionally.)
(3) Let 𝑓,𝑔 be the generic elements of ∏𝑥:𝐴𝐵. In the extended context …,𝑥:𝐴, the terms 𝑓𝑥 and 𝑔𝑥 are two elements of the proposition 𝐵, so 𝑓𝑥≡𝑔𝑥; rule 𝜆-eq of remark 27.4 and the 𝜂-rule of definition 27.2 then give 𝑓≡𝑔, exactly as in the proof of theorem 35.9(2).
(4) Let 𝑢,𝑣 be the generic elements of ∑𝑥:𝐴𝐵. Since 𝐴 is a proposition, 𝗉𝗋1(𝑢)≡𝗉𝗋1(𝑣):𝐴. Convert 𝗉𝗋2(𝑣) along this equality to the fiber 𝐵[𝗉𝗋1(𝑢)/𝑥]. That fiber is a proposition, so 𝗉𝗋2(𝑢)≡𝗉𝗋2(𝑣). Pair congruence followed by the two Σ eta equations gives 𝑢Σ−𝜂≡(𝗉𝗋1(𝑢),𝗉𝗋2(𝑢))𝑝𝑎𝑖𝑟−𝑒𝑞≡(𝗉𝗋1(𝑣),𝗉𝗋2(𝑣))Σ−𝜂≡𝑣.
(5) If 𝟐 were a proposition, substituting its generic elements by 𝗍𝗍,𝖿𝖿 would give 𝗍𝗍≡𝖿𝖿. This contradicts the sound set interpretation of proposition 35.4, in which they denote 1 and 0. The propositions 𝟏,𝟏 have a coproduct with distinct elements 𝗂𝗇𝗅(⋆) and 𝗂𝗇𝗋(⋆); their set interpretations carry different tags. Hence 𝟏+𝟏 is not a proposition. ◻
Proof. If 𝐴 is a proposition, then in Γ,𝑥:𝐴,𝑦:𝐴 we have 𝑥≡𝑦, so 𝗋𝖾𝖿𝗅 inhabits 𝖤𝗊𝐴(𝑥,𝑦) by conversion, and 𝜆𝑥.𝜆𝑦.𝗋𝖾𝖿𝗅:𝗂𝗌𝖯𝗋𝗈𝗉(𝐴). Conversely, if Γ⊢𝑤:𝗂𝗌𝖯𝗋𝗈𝗉(𝐴), then Γ,𝑥:𝐴,𝑦:𝐴⊢𝑤𝑥𝑦:𝖤𝗊𝐴(𝑥,𝑦), and Eq-Reflect gives 𝑥≡𝑦. Finally 𝗂𝗌𝖯𝗋𝗈𝗉(𝐴) is a Π-type into an 𝖤𝗊-type, hence a proposition by lemma 35.15(1),(3). ◻
Let Γ⊢𝐴𝗍𝗒𝗉𝖾, Γ⊢𝐵𝗍𝗒𝗉𝖾 and Γ,𝑥:𝐴,𝑦:𝐵⊢𝑃𝗍𝗒𝗉𝖾. The naive translation of the axiom of choice with Σ as ∃, 𝖭𝖺𝗂𝗏𝖾𝖢𝗁𝗈𝗂𝖼𝖾:=(∏𝑥:𝐴∑𝑦:𝐵𝑃)→∑𝑓:𝐴→𝐵∏𝑥:𝐴𝑃[𝑓𝑥/𝑦], is inhabited already in the base, by 𝜆𝐹.(𝜆𝑥.𝗉𝗋1(𝐹𝑥),𝜆𝑥.𝗉𝗋2(𝐹𝑥)) (the second component typechecks up to 𝛽). This term does not choose anything: it merely re-associates a pair-valued function into a pair of functions. The force of the axiom of choice — extracting a function from a bare existence statement — is absent, because an inhabitant of ∑𝑦:𝐵𝑃 is not a bare existence statement: its witness is available by projection. The proper formulation requires an existential that is a proposition.
The propositional truncation‖𝐴‖ discards the identity of an inhabitant of 𝐴 while retaining whether one exists. Extend the binding signature by ‖𝐴‖ and |𝑎|, both of arity (0), and by the annotated recursor 𝗋𝖾𝖼‖𝐴‖(𝑥.𝑐,𝑡) of arity (1,0), binding 𝑥 in 𝑐. Substitution through the recursor is therefore the corresponding binding clause of definition 26.10.
The optional truncation delta adds a former ‖𝐴‖.
Γ⊢𝐴𝗍𝗒𝗉𝖾
Γ⊢‖𝐴‖𝗍𝗒𝗉𝖾
Tr-F
Γ⊢𝑎:𝐴
Γ⊢|𝑎|:‖𝐴‖
Tr-I
Γ⊢𝑝:‖𝐴‖Γ⊢𝑞:‖𝐴‖
Γ⊢𝑝≡𝑞:‖𝐴‖
Tr-Uniq
Γ⊢𝐶𝗍𝗒𝗉𝖾Γ,𝑦:𝐶,𝑧:𝐶⊢𝑦≡𝑧:𝐶Γ,𝑥:𝐴⊢𝑐:𝐶Γ⊢𝑡:‖𝐴‖
Γ⊢𝗋𝖾𝖼‖𝐴‖(𝑥.𝑐,𝑡):𝐶
Tr-E
Its classified congruence instances include
Γ⊢𝐴≡𝐴′𝗍𝗒𝗉𝖾
Γ⊢‖𝐴‖≡‖𝐴′‖𝗍𝗒𝗉𝖾
Tr-F-eq
Γ⊢𝑎≡𝑎′:𝐴
Γ⊢|𝑎|≡|𝑎′|:‖𝐴‖
Tr-I-eq
and, after converting the primed data to the displayed common types,
Γ⊢𝐶≡𝐶′𝗍𝗒𝗉𝖾Γ,𝑦:𝐶,𝑧:𝐶⊢𝑦≡𝑧:𝐶Γ,𝑥:𝐴⊢𝑐≡𝑐′:𝐶Γ⊢𝑡≡𝑡′:‖𝐴‖
Γ⊢𝗋𝖾𝖼‖𝐴‖(𝑥.𝑐,𝑡)≡𝗋𝖾𝖼‖𝐴‖(𝑥.𝑐′,𝑡′):𝐶
Tr-E-eq
Rule Tr-Uniq makes ‖𝐴‖ a proposition. Rule Tr-E permits elimination into propositions only: its premise on 𝐶 is the judgment of definition 35.13.
Proof of Corollary 35.19 — Set interpretation of truncation
Proof. Interpret ‖𝐴‖ as the quotient of [[𝐴]]𝜌 by the indiscrete equivalence relation. It is empty when 𝐴 is empty and otherwise a singleton; |𝑎| denotes the class of 𝑎. Given a branch 𝑎↦𝑐(𝑎) into a proposition 𝐶, set 𝗋𝖾𝖼‖𝐴‖(𝑥.𝑐,[𝑎]):=𝑐(𝑎). This is independent of the representative because every two elements of 𝐶 are equal. It validates Tr-Uniq, Tr-E, their congruence rules, and semantic substitution. ◻
No computation rule accompanies Tr-E: since 𝐶 is a proposition, 𝗋𝖾𝖼‖𝐴‖(𝑥.𝑐,|𝑎|) and 𝑐[𝑎/𝑥] are two elements of 𝐶 and hence the following equality is derivable: Γ⊢𝗋𝖾𝖼‖𝐴‖(𝑥.𝑐,|𝑎|)≡𝑐[𝑎/𝑥]:𝐶. For the same reason a dependent eliminator is derivable rather than postulated (proposition 35.21). Rule Tr-Uniq makes ‖𝐴‖ judgmentally propositional.
Suppose every fiber 𝐶 is a proposition and Γ,𝑧:‖𝐴‖⊢𝐶𝗍𝗒𝗉𝖾. Assume Γ,𝑥:𝐴⊢𝑐:𝐶[|𝑥|/𝑧]andΓ⊢𝑡:‖𝐴‖. One can derive a term of 𝐶[𝑡/𝑧] using only Tr-E and the earlier type formers.
Proof of Proposition 35.21 — Dependent truncation elimination
Proof. Put 𝐷:=∑𝑧:‖𝐴‖𝐶. This is a proposition. Indeed, for generic 𝑑,𝑒:𝐷, rule Tr-Uniq gives 𝗉𝗋1(𝑑)≡𝗉𝗋1(𝑒). After converting the second components to the same fiber, propositionhood of 𝐶 gives 𝗉𝗋2(𝑑)≡𝗉𝗋2(𝑒); pair congruence and Σ-𝜂 then give 𝑑≡𝑒.
The branch 𝑥.(|𝑥|,𝑐) has type 𝐷, so Tr-E gives 𝑑:=𝗋𝖾𝖼‖𝐴‖(𝑥.(|𝑥|,𝑐),𝑡):𝐷. Both 𝗉𝗋1(𝑑) and 𝑡 inhabit ‖𝐴‖, hence Tr-Uniq gives 𝗉𝗋1(𝑑)≡𝑡. Consequently 𝗉𝗋2(𝑑):𝐶[𝗉𝗋1(𝑑)/𝑧] converts to an element of 𝐶[𝑡/𝑧], as required. When 𝑡=|𝑎|, the induced computation equality from the preceding remark, followed by the two Σ beta rules, identifies this term with 𝑐[𝑎/𝑥]. ◻
With the truncation delta, the propositions of definition 35.13 model intuitionistic predicate logic, with connectives:
logic
type
a proposition when
⊤
𝟏
always
⊥
𝟎
always
𝜑∧𝜓
𝜑×𝜓
𝜑,𝜓 propositions
𝜑⊃𝜓
𝜑→𝜓
𝜓 a proposition
¬𝜑
𝜑→𝟎
always
𝑎=𝐴𝑏
𝖤𝗊𝐴(𝑎,𝑏)
always
∀𝑥:𝐴.𝜑
∏𝑥:𝐴𝜑
𝜑 a proposition
∃𝑥:𝐴.𝜑
‖∑𝑥:𝐴𝜑‖
always
𝜑∨𝜓
‖𝜑+𝜓‖
always
Each connective is a proposition under the stated hypotheses, and its introduction and elimination rules (restricted, for ∃ and ∨, to propositional conclusions) are derivable.
Proof. Proposition-hood follows from lemma 35.15 and Tr-Uniq. The ordinary rules of the corresponding formers give the rules for ⊤,⊥,∧,⊃,¬, and ∀. Equality uses theorem 35.7. Existential introduction is |(𝑎,𝑏)|; elimination into a proposition combines Tr-E with Σ-elimination.
For disjunction, the two introductions are 𝜆𝑎.|𝗂𝗇𝗅(𝑎)|:𝐴→𝐴∨𝐵,𝜆𝑏.|𝗂𝗇𝗋(𝑏)|:𝐵→𝐴∨𝐵. Given a proposition 𝐶, 𝑓:𝐴→𝐶, and 𝑔:𝐵→𝐶, coproduct elimination gives 𝑧:𝐴+𝐵⊢𝗂𝗇𝖽+(𝑓,𝑔,𝑧):𝐶. Applying Tr-E yields 𝜆𝑡.𝗋𝖾𝖼‖𝐴+𝐵‖(𝑧.𝗂𝗇𝖽+(𝑓,𝑔,𝑧),𝑡):(𝐴∨𝐵)→𝐶. On either injection the expected computation equality follows first from the induced truncation computation of remark 35.20 and then from the corresponding coproduct beta rule. ◻
Assume the universe rules of definition 29.1. The type of small propositions is 𝖯𝗋𝗈𝗉0:=∑𝑋:U0𝗂𝗌𝖯𝗋𝗈𝗉(𝑋). For 𝜑:𝖯𝗋𝗈𝗉0, write 𝜑∘:=𝗉𝗋1(𝜑) for its underlying type. Thus the universe-quantified form of excluded middle is the precise type ∏𝜑:𝖯𝗋𝗈𝗉0𝜑∘∨¬𝜑∘. No closure property of 𝖯𝗋𝗈𝗉0 is hidden in this notation; the required codes and proofs of propositionhood must be constructed. Quantifying over 𝖯𝗋𝗈𝗉0 is what upgrades the preceding predicate-logic interpretation to higher-order logic.
Formulated with ∃ of definition 35.22, the axiom of choice 𝖠𝖢:=(∏𝑥:𝐴‖∑𝑦:𝐵𝑃‖)→‖∑𝑓:𝐴→𝐵∏𝑥:𝐴𝑃[𝑓𝑥/𝑦]‖ is no longer automatically inhabited: the witness inside a truncation is inaccessible to the type 𝐴→𝐵. Neither 𝖠𝖢 nor the law of excluded middle 𝖫𝖤𝖬:=∏𝜑:𝖯𝗋𝗈𝗉0𝜑∘∨¬𝜑∘ of definition 35.24 is assumed in this chapter. Projecting from ‖∑𝑦:𝐵𝑃‖ cannot define a witness in 𝐵; therefore the calculation of example 35.17 proves neither 𝖠𝖢 nor 𝖫𝖤𝖬.
★★☆ Assume Γ⊢𝐴𝗍𝗒𝗉𝖾 and Γ,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾, let every fiber 𝐵 be a proposition, and suppose it has a section 𝑠:∏𝑥:𝐴𝐵. Show that ∑𝑥:𝐴𝐵 is a proposition if and only if 𝐴 is. For the implication from the sum to 𝐴, apply 𝗉𝗋1 to the equality between (𝑥,𝑠(𝑥)) and (𝑦,𝑠(𝑦)).
★☆☆ Use proposition 35.4 to show that ℕ is not a proposition. More generally, let 𝐴 be a closed type with a closed inhabitant 𝑎:𝐴. Show in the empty context that 𝐴+𝐴 is not a proposition by comparing 𝗂𝗇𝗅(𝑎) and 𝗂𝗇𝗋(𝑎) in the set interpretation.
★★☆ Show that 𝐴 is a proposition if and only if the map 𝜆𝑎.|𝑎|:𝐴→‖𝐴‖ admits a retraction, and that in this case the retraction is a judgmental isomorphism (both composites judgmentally equal to identities). Conclude that ‖‖𝐴‖‖ and ‖𝐴‖ are always judgmentally isomorphic.
★★☆ For 𝑓:𝐴→𝐵, use Tr-E to construct ‖𝑓‖:‖𝐴‖→‖𝐵‖. Show from propositionhood alone that ‖𝜆𝑥.𝑥‖ is judgmentally the identity and that ‖𝑔∘𝑓‖ is judgmentally ‖𝑔‖∘‖𝑓‖.
★★☆ Construct maps 𝐴∨𝐵→𝐵∨𝐴 and (𝐴∨𝐵)∨𝐶→𝐴∨(𝐵∨𝐶). Construct their reverse maps and use propositionhood to show that both pairs of composites are judgmentally equal to the relevant identity functions.
★★★ Work with 𝖯𝗋𝗈𝗉0 from definition 35.24. Construct elements representing ⊤, ⊥, 𝜑∘∧𝜓∘, and 𝜑∘⊃𝜓∘ for 𝜑,𝜓:𝖯𝗋𝗈𝗉0. More generally, if Γ,𝑥:𝐴⊢𝐵:U0 and Γ⊢𝐴:U0 and Γ⊢𝑞:∏𝑥:𝐴𝗂𝗌𝖯𝗋𝗈𝗉(𝐵), construct the element of 𝖯𝗋𝗈𝗉0 whose underlying type is ∏𝑥:𝐴𝐵.
For Γ⊢𝐴:U0 and Γ⊢𝑎,𝑏:𝐴, explicitly apply Eq-Form-U and Eq-Uniq to construct the element whose underlying type is 𝖤𝗊𝐴(𝑎,𝑏). Finally, assuming a universe code for truncation and its decoding equation, construct elements whose underlying types are ‖∑𝑥:𝐴𝐵‖and‖𝜑∘+𝜓∘‖. These are the universe-coded existential and disjunction operations.
By theorem 35.9, reflection proves UIP and function extensionality. This section states the precise converse: over the core base, the two axioms recover the full strength of reflection, as far as inhabitation is concerned. The result is due to Hofmann.
Fix the Hofmann core𝑇H: the structural rules (definition 26.22) with the formers Π, Σ, and 𝟏 (with their 𝜂-rules), ℕ, and 𝖨𝖽 with 𝖩 (definition 30.1); no universes or other inductive types. Define:
𝑇𝐸 (extensional core): 𝑇H extended by the rules
Γ⊢𝑝:𝖨𝖽𝐴(𝑎,𝑏)
Γ⊢𝑎≡𝑏:𝐴
Id-Reflect
Γ⊢𝑝:𝖨𝖽𝐴(𝑎,𝑏)
Γ⊢𝑝≡𝗋𝖾𝖿𝗅:𝖨𝖽𝐴(𝑎,𝑏)
Id-Uniq
i.e. the delta of definition 35.1 imposed on 𝖨𝖽 directly; by proposition 35.10 this is our ETT restricted to the core after replacing 𝖤𝗊 by the propositionally equivalent 𝖨𝖽 former. The two raw type formers are not being declared judgmentally equal.
𝑇𝐼 (intensional core with extensionality axioms): 𝑇H extended by two constants without computation rules. Their raw arities are 𝗎𝗂𝗉(𝑝):(0) and 𝖾𝗑𝗍(𝑓,𝑔,𝑥.ℎ):(0,0,1), the last entry binding 𝑥 in ℎ:
Γ⊢𝑝:𝖨𝖽𝐴(𝑎,𝑎)
Γ⊢𝗎𝗂𝗉(𝑝):𝖨𝖽𝖨𝖽𝐴(𝑎,𝑎)(𝑝,𝗋𝖾𝖿𝗅)
UIP-Ax
Γ⊢𝑓:∏𝑥:𝐴𝐵Γ⊢𝑔:∏𝑥:𝐴𝐵Γ,𝑥:𝐴⊢ℎ:𝖨𝖽𝐵(𝑓𝑥,𝑔𝑥)
Γ⊢𝖾𝗑𝗍(𝑓,𝑔,𝑥.ℎ):𝖨𝖽∏𝑥:𝐴𝐵(𝑓,𝑔)
Ext-Ax
The one-endpoint form of UIP-Ax is the primitive constant used below.
The named stripping map sends expressions of 𝑇𝐼 to expressions of 𝑇𝐸. For source expressions 𝑒:=𝗎𝗂𝗉(𝑝),𝑒′:=𝖾𝗑𝗍(𝑓,𝑔,𝑥.ℎ), put strip(𝑒):=𝗋𝖾𝖿𝗅strip(𝑝),strip(𝑒′):=𝗋𝖾𝖿𝗅strip(𝑓). The map is homomorphic through every other term, type, and context former. For contexts, strip(⋅)=⋅,strip((Γ,𝑥:𝐴))=strip(Γ),𝑥:strip(𝐴). The corresponding type and term clauses induce stripping on judgments. Propositional truncation is not among the formers of 𝑇𝐼 or 𝑇𝐸. In particular, stripping preserves the raw domain annotation of 𝜆(𝑥:𝐴).𝑏, sending it to the annotated expression 𝜆(𝑥:strip(𝐴)).strip(𝑏). The annotation is merely suppressed in ordinary print.
Stripping is well defined on alpha-classes and commutes with capture-avoiding substitution: strip(𝑒[𝑎/𝑥])=strip(𝑒)[strip(𝑎)/𝑥]. For a telescope, the induced equation is strip((Δ[𝑎/𝑥]))=strip(Δ)[strip(𝑎)/𝑥] declaration by declaration.
Proof. Induct on the binding tree of 𝑒. Every old constructor is homomorphic. For 𝗎𝗂𝗉(𝑝) the induction hypothesis gives the first equation below. For 𝖾𝗑𝗍(𝑓,𝑔,𝑦.ℎ) choose 𝑦 fresh for 𝑎; the induction hypothesis applies to 𝑓,𝑔,ℎ and gives the second: strip(𝑝[𝑎/𝑥])𝐼𝐻=strip(𝑝)[strip(𝑎)/𝑥],strip(𝑓[𝑎/𝑥])𝐼𝐻=strip(𝑓)[strip(𝑎)/𝑥]. Changing the fresh representative changes neither result, so the calculation also respects the alpha-generator at the bound branch. The displayed context and telescope equations then induce the result for judgments. ◻
Proof of Proposition 35.29 — Soundness of stripping
Proof. Use induction on derivations. Substitution cases use lemma 35.28. Every other rule of 𝑇H translates to itself. For UIP-Ax, put 𝐼:=𝖨𝖽strip(𝐴)(strip(𝑎),strip(𝑎)). Inductively, strip(Γ)⊢strip(𝑝):𝐼. Hence strip(𝑝)𝐼𝑑−𝑈𝑛𝑖𝑞≡𝗋𝖾𝖿𝗅,𝖨𝖽𝐼(strip(𝑝),𝗋𝖾𝖿𝗅)𝑐𝑜𝑛𝑔𝑟𝑢𝑒𝑛𝑐𝑒≡𝖨𝖽𝐼(𝗋𝖾𝖿𝗅,𝗋𝖾𝖿𝗅). The term 𝗋𝖾𝖿𝗅strip(𝑝) inhabits the latter type; conversion concludes. For Ext-Ax, the induction hypothesis gives strip(Γ),𝑥:strip(𝐴)⊢strip(ℎ):𝖨𝖽strip(𝐵)(strip(𝑓)𝑥,strip(𝑔)𝑥). Thus strip(𝑓)𝑥≡strip(𝑔)𝑥 by Id-Reflect, hence strip(𝑓)≡strip(𝑔) by the 𝜆-eq (remark 27.4) and 𝜂 as in theorem 35.9(2). By conversion, 𝗋𝖾𝖿𝗅strip(𝑓) inhabits 𝖨𝖽∏𝑥:strip(𝐴)strip(𝐵)(strip(𝑓),strip(𝑔)). (Without the 𝜂-rule for Π this case fails for terms that are not abstractions; 𝜂 is essential here.)
The two new term-congruence schemes also require cases because stripping is not homomorphic at these constructors. The induction hypothesis is strip(𝑝)≡strip(𝑝′); conversion makes the two identity classifiers the same type; congruence for annotated reflexivity then gives 𝗋𝖾𝖿𝗅strip(𝑝)𝐼𝐻≡𝗋𝖾𝖿𝗅strip(𝑝′). This is the congruence case for 𝗎𝗂𝗉. For 𝖾𝗑𝗍, the induction hypothesis strip(𝑓)≡strip(𝑓′) gives 𝗋𝖾𝖿𝗅strip(𝑓)≡𝗋𝖾𝖿𝗅strip(𝑓′) by reflexivity congruence. The hypotheses for 𝑔 and the bound branch validate the remaining premises of the source congruence instance, although stripping its conclusion depends only on 𝑓. Thus every stripped 𝗎𝗂𝗉 congruence is reflexivity congruence in 𝑇𝐸; the same holds for 𝖾𝗑𝗍 congruence. ◻
Stripping is now a sound one-way translation, but it is not an inverse on terms: the two axiom constants have disappeared. The first quotient attempt identifies 𝑎 and 𝑏 whenever 𝖨𝖽𝐴(𝑎,𝑏) is inhabited. It fails under substitution: if the substitution representatives are only propositionally equal, then 𝐴[𝑓] and 𝐴[𝑔] are different fibers, so the two substituted terms do not even have a common identity type until one is transported. Choosing an arbitrary transport does not repair composition, because the two choices at an intermediate representative need not be the same raw map.
Here is the failed backward case in symbols. We write 𝑋⟶𝑌 for the underlying comparison map from 𝑋 to 𝑌. Equality reflection in 𝑇𝐸 turns 𝑝:𝖨𝖽𝐴(𝑎,𝑏) into 𝑎≡𝑏. A backward translation must instead compare 𝐵[𝑎/𝑥]and𝐵[𝑏/𝑥]by𝗍𝗋𝑥.𝐵𝑝:𝐵[𝑎/𝑥]⟶𝐵[𝑏/𝑥]. For two witnesses 𝑝,𝑞:𝖨𝖽𝐴(𝑎,𝑏) it obtains two raw maps 𝗍𝗋𝑥.𝐵𝑝 and 𝗍𝗋𝑥.𝐵𝑞. Even if both have the right endpoints, composition through a third representative requires a path 𝗍𝗋𝑥.𝐵𝑝⋅𝑟=𝖨𝖽𝗍𝗋𝑥.𝐵𝑟∘𝗍𝗋𝑥.𝐵𝑝, and changing 𝑝 to 𝑞 requires another such coherence. A quotient by inhabitation alone records neither witness, so it cannot type, let alone prove, these two comparison obligations. General UIP equates parallel witnesses; canonical comparisons retain the transport maps and their composition paths.
To lift an extensional inhabitant back, we therefore construct a quotient 𝑄 of 𝑇𝐼 syntax in which propositionally equal substitutions and terms have coherent representatives. The construction comes in four steps. General UIP makes any two identity witnesses interchangeable, so no choice among them matters. Equal-substitution transport compares fibers over propositionally equal substitutions. Canonical comparisons then organize changes of representative, and the quotient lemmas carry the structural rules and the five core formers across them. A final triangle calculation produces the lifted term.
Proof. Use the primitive two-endpoint 𝖩 on 𝑞 with motive 𝑥,𝑦:𝐴,𝑞:𝖨𝖽𝐴(𝑥,𝑦)⊢∏𝑝:𝖨𝖽𝐴(𝑥,𝑦)𝖨𝖽𝖨𝖽𝐴(𝑥,𝑦)(𝑝,𝑞)𝗍𝗒𝗉𝖾. Its reflexivity clause is 𝑧.𝜆𝑝.𝗎𝗂𝗉(𝑝). The required inhabitant is the resulting function applied to 𝑝. Only its existence and the resulting uniqueness of all identity witnesses are needed below. ◻
Let Δ=(𝑦1:𝐵1,…,𝑦𝑛:𝐵𝑛) and let 𝑓,𝑔:Γ→Δ. A component path𝑝:𝑓=Δ𝑔 is a left-to-right list of identifications. Its first component is 𝑝1:𝖨𝖽𝐵1(𝑓1,𝑔1). Having chosen the first 𝑖−1 components, transport 𝑓𝑖 through them to the fiber containing 𝑔𝑖 and choose an identification there. This is the same telescope discipline used for a context morphism in proposition 26.46.
If Δ⊢𝐴𝗍𝗒𝗉𝖾, write 𝑝𝐴∗:𝐴[𝑓]⟶𝐴[𝑔] for iterated transport through this list. Its reverse is (𝑝−1)𝐴∗. Concatenation of component paths is defined in the same left-to-right order, transporting every later component before composing it.
The first dependent case is worth displaying. For Δ=(𝑦:𝐵,𝑧:𝐶(𝑦)), write 𝑓=(𝑏,𝑐) and 𝑔=(𝑏′,𝑐′). A component path from 𝑓 to 𝑔 is not merely a pair of parallel paths: it consists of 𝑝:𝖨𝖽𝐵(𝑏,𝑏′),𝑞:𝖨𝖽𝐶(𝑏′)(𝑝𝐶∗(𝑐),𝑐′). Thus, for 𝑦:𝐵,𝑧:𝐶(𝑦)⊢𝐷𝗍𝗒𝗉𝖾, its action has the typed form (𝑝,𝑞)𝐷∗:𝐷[𝑏/𝑦,𝑐/𝑧]⟶𝐷[𝑏′/𝑦,𝑐′/𝑧]. One first eliminates 𝑝; only then do 𝑐 and 𝑐′ lie in a common fiber and the elimination of 𝑞 become well formed. At 𝑝≡𝗋𝖾𝖿𝗅 and 𝑞≡𝗋𝖾𝖿𝗅 the displayed map is the identity. This two-coordinate calculation is the induction step repeated down a longer telescope.
Proof of Lemma 35.32 — Equal-substitution transport
Proof. Induct on the length of Δ. For the empty telescope there is one substitution, 𝑝𝐴∗≡𝜆𝑥.𝑥, and every clause is reflexivity. For Δ′=(Δ,𝑦:𝐵), write 𝑓=(¯𝑓,𝑟), 𝑔=(¯𝑔,𝑠), and 𝑝=(¯𝑝,𝑞), where ¯𝑝:¯𝑓=Δ¯𝑔,𝑞:𝖨𝖽𝐵[¯𝑔](¯𝑝𝐵∗(𝑟),𝑠). First apply the induction hypothesis to ¯𝑝. Elimination on 𝑞 then reduces the last coordinate to reflexivity, so the action on a family over Δ,𝑦:𝐵 is the iterated action (¯𝑝,𝑞)𝐴∗:=𝑞𝑦.𝐴[¯𝑔]∗∘¯𝑝𝑦.𝐴∗; the displayed notation abbreviates the two successive, well-typed identity eliminations. At ¯𝑝≡𝗋𝖾𝖿𝗅 and 𝑞≡𝗋𝖾𝖿𝗅 this is literally the identity. The inverse law and the term-action law therefore follow by the same two eliminations. For concatenation and reindexing, the induction hypothesis identifies the prefix maps, after which elimination on the two last-coordinate paths leaves the reflexivity equation. This proves (1)–(3) and records the induction step rather than appealing to simultaneous elimination without its dependent typing.
For (4), stripping reflects the prefix components and then 𝑞 to judgmental equalities, so the two successive eliminations compute to the identity. Choice-independence uses the same telescope induction. UIP first identifies the two prefix paths; transport along that identification puts the two last-coordinate paths in one identity type, where UIP identifies them. The two induced maps are pointwise equal by the preceding calculation, and Ext-Ax identifies the maps themselves. ◻
A context comparison𝑐:Γ≅Δ consists of substitutions 𝑐+:Γ→Δ and 𝑐−:Δ→Γ and component paths 𝜖:𝑐−𝑐+=Γ1Γ,𝜂:𝑐+𝑐−=Δ1Δ.
For Γ⊢𝐴𝗍𝗒𝗉𝖾 and Δ⊢𝐵𝗍𝗒𝗉𝖾, a type comparison𝑢:𝐴≅𝑐𝐵 consists of 𝑢+:𝐴⟶𝐵[𝑐+],𝑢−:𝐵⟶𝐴[𝑐−], together with inverse identifications. In the first composite, 𝑢−[𝑐+]𝑢+ lands in 𝐴[𝑐−𝑐+] and is transported by 𝜖𝐴∗ before it is compared with the identity; the other composite uses 𝜂𝐵∗. Thus the inverse equations are literally well typed.
Both comparisons are written ≅, and the subscript names the context comparison the types are compared over. When 𝐴 and 𝐵 live over the same context, that comparison is the identity and the subscript is omitted, so a bare 𝐴≅𝐵 is still a type comparison, never a context comparison: the operands say which is meant.
The canonical comparisons are the inductively generated class containing identity comparisons and the comparisons 𝑝𝐴∗ of lemma 35.32, and closed under inverse, composite, substitution, judgmental conversion, and the following constructors. At a context extension the forward substitution is (𝑐+,𝑢+(𝑥)):Γ,𝑥:𝐴⟶Δ,𝑥′:𝐵; the reverse is obtained by exchanging 𝑐+ with 𝑐− and 𝑢+ with 𝑢−. The two component paths are the prefix paths followed by the inverse laws for 𝑢. For 𝟏 and ℕ take identity comparisons. From 𝑐:Γ≅Δ, 𝑢:𝐴≅𝑐𝐴′, and a comparison 𝑣:𝐵≅(𝑐,𝑢)𝐵′ over the extended contexts, close the class under the induced Π- and Σ-comparisons. For identity types, from 𝑐,𝑢 and arbitrary endpoint identifications 𝛼:𝑢+(𝑎)=𝖨𝖽𝑎′[𝑐+],𝛽:𝑢+(𝑏)=𝖨𝖽𝑏′[𝑐+], close it under the induced comparison between 𝖨𝖽𝐴(𝑎,𝑏) and 𝖨𝖽𝐴′(𝑎′,𝑏′). These clauses are closed under reindexing. Every generator preserves the number of context declarations; in particular, the canonical-comparison class of ⋅ contains only ⋅. Arguments about canonical comparisons may therefore proceed by induction on the final generating clause; no additional, unnamed comparisons belong to the class.
For the identity context comparison on Γ and any Γ⊢𝐴𝗍𝗒𝗉𝖾, the generated type comparison is 𝐴≅1Γ𝐴,𝑢+:=𝜆𝑥.𝑥,𝑢−:=𝜆𝑥.𝑥. Both inverse witnesses reduce to reflexivity. Reindexing this comparison along 𝑓:Δ→Γ computes to the same identity comparison on 𝐴[𝑓]; thus the first generator already exhibits the typing, inverse, and reindexing components required below.
The class of definition 35.33 is closed under Π,Σ,𝟏,ℕ, and 𝖨𝖽, and under reindexing. Its inverse and composite comparisons obey the expected unit, associativity, and substitution laws up to identity. Parallel canonical maps are propositionally equal. After stripping, every canonical map is judgmentally the identity.
Proof of Lemma 35.34 — Canonical comparisons for the formers
Proof. The proof is a simultaneous induction on comparison-generation trees. The Σ case maps pairs coordinate by coordinate. The Π case conjugates functions by the domain and codomain comparisons. The 𝖨𝖽 case maps a path by the endpoint comparisons and the action of the carrier map. For each constructor, the proof writes the forward and reverse maps before checking inverse paths, reindexing, uniqueness, and stripping.
The comparisons for 𝟏 and ℕ are identities. Suppose 𝑐:Γ≅Δ, 𝑢:𝐴≅𝑐𝐴′, and 𝑣:𝐵≅(𝑐,𝑢)𝐵′ over the extended contexts. For Σ, the forward map is 𝑧↦(𝑢+(𝗉𝗋1𝑧),𝑣+,𝗉𝗋1𝑧(𝗉𝗋2𝑧)).(Σ) The reverse map is symmetric. Pair congruence, the inverse laws of 𝑢,𝑣, and Σ-eta give the two inverse identifications.
The product comparison must include the prefix transport. Reindex 𝑢− along 𝑐+ and, for 𝑥′:𝐴′[𝑐+], put ¯𝑥:=𝜖𝐴∗(𝑢−[𝑐+](𝑥′)):𝐴. The component path actually used here is the extended path ̃𝜖𝑥′:(𝑐−𝑐+,𝑢−[𝑐+](𝑥′))=Γ,𝑥:𝐴(1Γ,¯𝑥).(̃𝜖) Its prefix is 𝜖 and its last component is reflexivity, because ¯𝑥 was defined by the required transport. Apply clause 2 of lemma 35.32 to the section 𝑥.𝑢+(𝑥) and this extended path. It aligns 𝑢+[𝑐−𝑐+](𝑢−[𝑐+](𝑥′)) with 𝑢+(¯𝑥). The 𝜂-side inverse law for 𝑢, reindexed along 𝑐+, identifies the former term with 𝑥′; general UIP (lemma 35.30) identifies the intervening transport witnesses. Concatenating these paths in the required orientation gives 𝛿𝑥′:𝖨𝖽𝐴′[𝑐+](𝑢+(¯𝑥),𝑥′). Now define (Π(𝑢,𝑣))+(𝑓)(𝑥′):=(𝛿𝑥′)𝐵′[𝑐+]∗(𝑣+,¯𝑥(𝑓(¯𝑥))).(Π) Here the last transport moves the value from the fiber at 𝑢+(¯𝑥) to the fiber at 𝑥′.
For the reverse map, take 𝑥:𝐴[𝑐−] and put ¯𝑥′:=𝜂𝐴′∗(𝑢+[𝑐−](𝑥)):𝐴′. The extended path (𝑐+𝑐−,𝑢+[𝑐−](𝑥))=Δ,𝑥′:𝐴′(1Δ,¯𝑥′) and the 𝜖-side inverse law for 𝑢, reindexed along 𝑐−, give in exactly the preceding way 𝛿′𝑥:𝖨𝖽𝐴[𝑐−](𝑢−(¯𝑥′),𝑥). Define (Π(𝑢,𝑣))−(𝑔)(𝑥):=(𝛿′𝑥)𝐵[𝑐−]∗(𝑣−,¯𝑥′(𝑔(¯𝑥′))).(Π−1) After expanding the two formulas, the inverse laws for 𝑢 identify the twice-converted arguments and those for 𝑣 identify the values; UIP aligns the composite transports. Write 𝑃+:=Π(𝑢,𝑣)+ and 𝑃−:=Π(𝑢,𝑣)−. Thus, pointwise, 𝑃−(𝑃+(𝑓))(𝑥)=𝖨𝖽𝑓(𝑥),𝑃+(𝑃−(𝑔))(𝑥′)=𝖨𝖽𝑔(𝑥′). Rule Ext-Ax, followed by Π-eta, gives the two inverse identifications of functions.
For identity types, let 𝛼:𝑢+(𝑎)=𝖨𝖽𝑎′[𝑐+] and 𝛽:𝑢+(𝑏)=𝖨𝖽𝑏′[𝑐+] be the endpoint comparisons. Put 𝑝↦(𝛼−1⋅𝖺𝗉𝑢+(𝑝))⋅𝛽.(𝖨𝖽) For the reverse map, reindex 𝛼 and 𝛽 along 𝑐− and transport them through 𝜂. Clause 2 of equal-substitution transport for the endpoint sections gives ̂𝛼:𝖨𝖽𝐴′(𝜂𝐴′∗(𝑢+[𝑐−](𝑎[𝑐−])),𝑎′),̂𝛽:𝖨𝖽𝐴′(𝜂𝐴′∗(𝑢+[𝑐−](𝑏[𝑐−])),𝑏′). Let 𝜄𝑎 and 𝜄𝑏 be the 𝜖-side inverse laws for 𝑢 at 𝑎[𝑐−] and 𝑏[𝑐−], with the displayed 𝜂 transports inserted, and set ¯𝛼:=𝖺𝗉𝑢−(̂𝛼)−1⋅𝜄𝑎:𝖨𝖽𝐴[𝑐−](𝑢−(𝑎′),𝑎[𝑐−]),¯𝛽:=𝖺𝗉𝑢−(̂𝛽)−1⋅𝜄𝑏:𝖨𝖽𝐴[𝑐−](𝑢−(𝑏′),𝑏[𝑐−]). The reverse map is therefore the well-typed formula 𝑝′↦(¯𝛼−1⋅𝖺𝗉𝑢−(𝑝′))⋅¯𝛽.(𝖨𝖽−1) Let 𝐹 and 𝐺 denote the forward and reverse maps just defined. General UIP gives the endpoint-indexed inverse paths 𝜂𝑝′:𝖨𝖽𝖨𝖽𝐴′(𝑎′,𝑏′)(𝐹(𝐺(𝑝′)),𝑝′),𝜖𝑝:𝖨𝖽𝖨𝖽𝐴(𝑎,𝑏)(𝐺(𝐹(𝑝)),𝑝). The same UIP terms make the maps independent of the chosen witnesses used to define ̂𝛼,̂𝛽.
These formulas define the former clauses. For substitution, reindex every displayed map; whenever two reindexed substitutions are only connected by a component path, insert the map of lemma 35.32. Its concatenation and reindexing laws give the unit, associativity, and substitution equations.
The identity comparison is reflexivity. For an equal-substitution generator, typing is the first clause of lemma 35.32; its inverse law is the second clause; uniqueness of the chosen comparison is the third; and stripping is the fourth. For an inverse or composite, concatenate the paths obtained for the smaller generation trees. The only mixed calculation is reindexing a composite: (𝑣+𝑢+)[ℎ]≡𝑣+[ℎ]𝑢+[ℎ]. If the two occurrences of ℎ have equal substitution components, the comparison between them is the transport of lemma 35.32; its concatenation law proves that the two inserted comparisons agree.
For a context extension, the induction splits into the prefix components and the final fiber component. For Σ, pointwise equality of the two coordinates and pair congruence compare parallel maps. For Π, compare the values at an arbitrary 𝑥′ by the induction hypotheses for 𝑢 and 𝑣, use UIP to identify the intervening transport paths, and apply Ext-Ax; this is exactly the point at which function extensionality is needed. For 𝖨𝖽, the two endpoint calculations reduce the claim to equality of parallel path data by lemma 35.30. The 𝟏 and ℕ cases are identities. Hence the induction proves closure, the three coherence laws, and uniqueness of parallel comparisons.
Finally, after stripping, Id-Reflect makes every component path judgmental. Formula (Σ) then reduces by pair eta, (Π) by 𝜆-eq and Π-eta, and (𝖨𝖽) by the groupoid computations at reflexivity. Thus every canonical comparison strips to the identity. ◻
Canonical comparisons are stable under composition and reindexing, so quotient equality can use them without choosing an arbitrary transport.
Define 𝑄 without identifying raw representatives silently.
A context is a canonical-comparison class [Γ].
A substitution [Γ]→[Δ] is represented by a triple (Γ0,Δ0,𝑓) with Γ0∈[Γ], Δ0∈[Δ], and 𝑓:Γ0→Δ0. Two triples (Γ0,Δ0,𝑓) and (Γ1,Δ1,𝑓′) are equal when, for canonical 𝑐:Γ0≅Γ1 and 𝑑:Δ0≅Δ1, there is a component path 𝑑+𝑓=Δ1𝑓′𝑐+.(𝑄−𝑆𝑢𝑏)
A type over [Γ] is represented by (Γ0,𝐴) with Γ0⊢𝐴𝗍𝗒𝗉𝖾. Two representatives are equal when connected by a canonical type comparison over a canonical comparison of their contexts.
A term is represented by (Γ0,𝐴,𝑎) with Γ0⊢𝑎:𝐴. Representatives (Γ0,𝐴,𝑎) and (Γ1,𝐵,𝑏) are equal when, for canonical 𝑐:Γ0≅Γ1 and 𝑢:𝐴≅𝑐𝐵, one has 𝑢+(𝑎)=𝖨𝖽𝑏[𝑐+].(𝑄−𝑇𝑚)
By lemma 35.34, the truth of (Q-Sub) and (Q-Tm) is independent of the chosen canonical comparisons.
Proof of Lemma 35.36 — Quotient substitution and comprehension
Proof. First, context, substitution, type, and term equality are equivalence relations: identities, inverses, and composites are canonical, and lemma 35.32 aligns the middle fibers in a transitivity calculation.
For example, the transitivity calculation for (Q-Sub) is visible already at substitutions. Suppose 𝑓𝑖:Γ𝑖→Δ𝑖 for 𝑖=0,1,2 represent consecutive equal substitutions, with canonical source comparisons 𝑐01,𝑐12, target comparisons 𝑑01,𝑑12, and component paths 𝑝:𝑑01,+𝑓0=Δ1𝑓1𝑐01,+,𝑞:𝑑12,+𝑓1=Δ2𝑓2𝑐12,+. Whisker 𝑝 on the left by 𝑑12,+ and 𝑞 on the right by 𝑐01,+, then concatenate: 𝑑12,+𝑑01,+𝑓0=Δ2𝑑12,+𝑓1𝑐01,+=Δ2𝑓2𝑐12,+𝑐01,+. This is (Q-Sub) for the composite canonical comparisons; their associativity paths align the displayed bracketings. The type and term transitivity proofs repeat this calculation one fiber at a time, using the transport lemma before concatenating the next component.
For (Q-Comp), replacing 𝑑 by another bridge gives a componentwise equal composite because parallel canonical maps are equal. Replacing 𝑓 or 𝑔 uses (Q-Sub), whiskered on the appropriate side; the concatenation law of lemma 35.32 identifies this concatenated whiskered path with the composite path displayed above. For (3), if 𝑑,𝑑′:Δ0≅Δ1 are two bridges, canonical coherence gives 𝑑+=Δ1𝑑′+. Substitution stability then gives the canonical comparison 𝐵[𝑑+𝑓]≅𝐵[𝑑′+𝑓]; the term comparison is its instance of lemma 35.32. For example, if 𝑓=Δ𝑓′, the required comparison 𝐵[𝑓]≅𝐵[𝑓′] is exactly (𝑓=𝑓′)𝐵∗ from that lemma. This is the comparison that ordinary substitution stability alone would not provide.
Associativity compares the two expressions obtained from (Q-Comp). After inserting the three bridges, their raw composites have the same order; associativity of syntactic substitution and the concatenation law identify them. Unit laws are the reflexivity case. At context extension, use the extended canonical comparison (𝑐,𝑢) of definition 35.33; its last component is precisely the comparison required for the variable. Projection and pairing equations are then the corresponding syntactic equations, represented by reflexivity. This proves every displayed structural equation. ◻
Thus the quotient already supports substitution and context extension; it remains only to show that the type formers and their eliminators respect these structural identifications.
The operations for Π,Σ,𝟏,ℕ, and 𝖨𝖽, including their introductions, eliminators, congruence, and computation equations, are well defined on the quotient data.
Proof of Lemma 35.37 — The formers and eliminators descend
Proof. Formation is independent of representatives by the five clauses of lemma 35.34. For Σ, formula (Σ) commutes with pairing and both projections; its two component calculations are the inverse laws for 𝑢,𝑣. Hence pair, 𝗉𝗋1, and 𝗉𝗋2 send equal representatives to equal representatives. The two beta equations and eta are represented by the judgmental equations of 𝑇𝐼.
For Π, formula (Π) was chosen so that evaluation commutes with the domain comparison: evaluating at 𝑥′ gives the displayed transported value in the fiber at 𝑥′. Its inverse calculation shows the same for abstraction. Thus application and abstraction preserve (Q-Tm); beta and eta again descend from their judgmental equations in 𝑇𝐼.
The 𝟏 comparison is the identity, so introduction and eta are immediate. The ℕ comparison is also the identity, but compatibility of its eliminator requires a calculation. Let 𝐶,𝐶′ be compared motives, write 𝑤𝑛:𝐶(𝑛)→𝐶′(𝑛) for the forward fiber map, and suppose the zero branches 𝑧,𝑧′ and successor branches 𝑠,𝑠′ satisfy (Q-Tm). For the common scrutinee 𝑛, prove by ℕ-induction that 𝑤𝑛(𝗂𝗇𝖽ℕ(𝐶;𝑧,𝑠;𝑛))=𝖨𝖽𝗂𝗇𝖽ℕ(𝐶′;𝑧′,𝑠′;𝑛).(𝑁𝑎𝑡−𝑐𝑜𝑚𝑝𝑎𝑡) At zero, both recursors compute and the required path is the comparison of 𝑧 with 𝑧′. At 𝗌𝗎𝖼(𝑛), both compute to their successor branches; apply the branch comparison to the induction hypothesis and then use the substitution transport of lemma 35.32 to align the two successor fibers. This proves (Nat-compat). If the scrutinees themselves are related by 𝑝:𝖨𝖽ℕ(𝑚,𝑛), identity induction on 𝑝 first reduces to the common-scrutinee calculation just proved. Thus ℕ elimination preserves quotient equality, including changes of motive and branches.
For 𝖨𝖽, formula (𝖨𝖽) preserves reflexivity by the unit laws. For 𝖩, let 𝑤𝑎,𝑏,𝑝 be the canonical fiber map between the motives, and let 𝑐,𝑐′ be their compared reflexivity branches. Let 𝑞:=(𝛼−1⋅𝖺𝗉𝑢+(𝑝))⋅𝛽 and let 𝑟:𝖨𝖽𝖨𝖽𝐴′(𝑎′,𝑏′)(𝑞,𝑝′) be the (Q-Tm) comparison of the two eliminands. Transport the motive comparison to the target fiber by putting ¯𝑤𝑎,𝑏,𝑝,𝑝′,𝑟(𝑑):=𝗍𝗋𝑞.𝐶′(𝑎′,𝑏′,𝑞)𝑟(𝑤𝑎,𝑏,𝑝(𝑑)). The required equation in this common fiber is ¯𝑤𝑎,𝑏,𝑝,𝑝′,𝑟(𝖩𝐶(𝑐;𝑎,𝑏,𝑝))=𝖨𝖽𝖩𝐶′(𝑐′;𝑎′,𝑏′,𝑝′).(𝐽−𝑐𝑜𝑚𝑝𝑎𝑡) Generalize the target endpoints, the endpoint paths 𝛼,𝛽, the target eliminand 𝑝′, and its comparison 𝑟. First identity-induct on the source eliminand 𝑝; then identity-induct on 𝛼 and 𝛽. The source and target endpoints now coincide and 𝑞≡𝗋𝖾𝖿𝗅. At this stage do not replace 𝑝′ by UIP: the transport in ¯𝑤 would remain stuck. Instead identity-induct directly on 𝑟:𝖨𝖽𝖨𝖽𝐴′(𝑎′,𝑎′)(𝗋𝖾𝖿𝗅,𝑝′). Its reflexivity case makes 𝑝′≡𝗋𝖾𝖿𝗅 and 𝑟≡𝗋𝖾𝖿𝗅 simultaneously. Therefore the transport in ¯𝑤 computes to the identity and both 𝖩 terms compute to their reflexivity branches. The remaining equation is exactly the assumed comparison of 𝑐 with 𝑐′. These four identity inductions prove (J-compat), hence 𝖩 preserves (Q-Tm). General UIP is used only afterward to make the result independent of alternative endpoint and transport witnesses. ◻
These compatibility results make 𝑄 a model of the core type theory. The stripping and quotient maps therefore form the triangle used for conservativity.
The quotient data validates every rule of 𝑇𝐸. If 𝖲𝗒𝗇(𝑇) denotes derivable contexts, types, substitutions, and terms modulo judgmental equality, there are maps 𝐾:𝖲𝗒𝗇(𝑇𝐼)→𝑄,𝑅:𝖲𝗒𝗇(𝑇𝐸)→𝑄,𝑆:𝑄→𝖲𝗒𝗇(𝑇𝐸) such that 𝐾=𝑅∘strip(−),𝑆𝑅=1𝖲𝗒𝗇(𝑇𝐸). Here 𝐾 takes a derivable object to its quotient class, 𝑅 interprets 𝑇𝐸 in 𝑄, and 𝑆 strips a representative.
Proof of Lemma 35.38 — The quotient model and its triangle
Proof. The structural rules hold by lemma 35.36, and the former rules by lemma 35.37. Identity is extensional in 𝑄: a representative 𝑝:𝖨𝖽𝐴(𝑎,𝑏) is exactly the witness required by (Q-Tm) to conclude [𝑎]=[𝑏]. To validate Id-Uniq, first align the classifiers: the identity comparison on 𝐴, together with the endpoint paths 𝗋𝖾𝖿𝗅𝑎:𝑎=𝑎 and 𝑝−1:𝑏=𝑎, gives a canonical comparison 𝖨𝖽𝐴(𝑎,𝑏)≅𝖨𝖽𝐴(𝑎,𝑎). It carries 𝑝 to a loop at 𝑎; general UIP (lemma 35.30) compares that transported loop with 𝗋𝖾𝖿𝗅𝑎. Thus [𝑝]=[𝗋𝖾𝖿𝗅𝑎] in the term quotient with its classifiers explicitly aligned. Hence 𝑄 validates every rule of 𝑇𝐸, and rule induction defines 𝑅. This interpretation is independent of the chosen derivation. Indeed, simultaneously for contexts, types, substitutions, and terms, induct on a pair of derivations of the same judgment. Structural and former cases use the equations proved in lemma 35.36, lemma 35.37; conversion and congruence use the defining quotient relations; and the two extensional cases use exactly the endpoint and proof identifications just displayed. Thus two derivations give the same quotient class, so 𝑅 descends to 𝖲𝗒𝗇(𝑇𝐸) rather than depending on proof trees.
Define 𝐾 by quotienting representatives, and define 𝑆[Γ]=strip(Γ),𝑆[(Γ,𝐴)]=strip(𝐴),𝑆[(Γ,𝐴,𝑎)]=strip(𝑎), and, for a substitution representative 𝛾:Δ⟶Γ, set 𝑆[𝛾]=strip(𝛾). This is well defined: canonical maps strip to identities by lemma 35.34, while Id-Reflect erases component paths and (Q-Tm) witnesses.
For the first equation in (35.1), induct on the 𝑇𝐼 derivation. Structural and former rules are lemma 35.36, lemma 35.37; conversion and congruence follow from the quotient relations, so both routes choose equal classes. The two extra 𝑇𝐼 constructors are 𝗎𝗂𝗉 and 𝖾𝗑𝗍. In the first case, 𝗎𝗂𝗉(𝑝):𝖨𝖽𝐼(𝑝,𝗋𝖾𝖿𝗅), where 𝐼:=𝖨𝖽𝐴(𝑎,𝑎), has endpoints 𝑝 and 𝗋𝖾𝖿𝗅; this path aligns the natural classifier 𝖨𝖽𝐼(𝑝,𝑝) of 𝗋𝖾𝖿𝗅𝑝 with 𝖨𝖽𝐼(𝑝,𝗋𝖾𝖿𝗅). After that alignment, general UIP compares 𝗋𝖾𝖿𝗅𝑝 with 𝗎𝗂𝗉(𝑝). In the second case put 𝑒:=𝖾𝗑𝗍(𝑓,𝑔,𝑥.ℎ):𝖨𝖽𝑃(𝑓,𝑔), where 𝑃:=∏𝑥:𝐴𝐵. The path 𝑒 aligns the natural classifier 𝖨𝖽𝑃(𝑓,𝑓) of 𝗋𝖾𝖿𝗅𝑓 with 𝖨𝖽𝑃(𝑓,𝑔), and general UIP then compares the transported reflexivity witness with 𝑒. These are exactly the two equalities between the 𝐾-classes and the classes of the stripped, endpoint-annotated reflexivity terms.
For 𝑆𝑅=1, induct on the 𝑇𝐸 derivation. Every structural or former rule is preserved by stripping the representative selected by its quotient operation. In an Id-Reflect case, 𝑅 identifies the endpoint classes using the source path and 𝑆 strips that path to the very judgmental equality produced by reflection. In an Id-Uniq case, 𝑅 uses the canonical classifier alignment followed by general UIP; 𝑆 strips both maps to identities and leaves the reflected proof-uniqueness equation. Conversion and congruence are preserved because 𝑆 is well defined on the quotient relations. These are all rules of 𝑇𝐸, so the second induction proves 𝑆𝑅=1. This proves the triangle. ◻
Let Γ𝖼𝗍𝗑 and Γ⊢𝐴𝗍𝗒𝗉𝖾 in 𝑇𝐼. If strip(Γ)⊢𝑡:strip(𝐴) in 𝑇𝐸 for some term 𝑡, then there exists a term 𝑡′ with Γ⊢𝑡′:𝐴 in 𝑇𝐼 and strip(Γ)⊢strip(𝑡′)≡𝑡:strip(𝐴) in 𝑇𝐸. In particular, a 𝑇𝐼-type is inhabited in 𝑇𝐼 if and only if its stripping is inhabited in 𝑇𝐸.
Proof. First let Γ be empty. Then 𝑅(𝑡) is a term of 𝑅(strip(𝐴))=𝐾(𝐴)=[(⋅,𝐴)] in 𝑄, by (35.1). Choose a representative ⋅⊢𝑏:𝐵 of this quotient term. Its classifier equality with [(⋅,𝐴)] has a canonical map 𝑢+:𝐵→𝐴; put 𝑡′:=𝑢+(𝑏). The equality of the two quotient terms says 𝐾(𝑡′)=𝑅(𝑡). Applying 𝑆 and using 𝑆𝑅=1 gives strip(𝑡′)≡𝑡:strip(𝐴) in 𝑇𝐸.
For a telescope Γ=(𝑥1:𝐴1,…,𝑥𝑛:𝐴𝑛), abstract the assumed term: 𝜆𝑥1.⋯𝜆𝑥𝑛.𝑡:∏𝑥1:strip(𝐴1)⋯∏𝑥𝑛:strip(𝐴𝑛)strip(𝐴). This displayed type is the stripping of the corresponding 𝑇𝐼 iterated product, so the empty-context case produces a 𝑇𝐼 inhabitant of that product. Apply it successively to 𝑥1,…,𝑥𝑛; repeated Π-beta gives 𝑡′:𝐴 in Γ and, after stripping, the required equality with 𝑡. The converse implication is proposition 35.29. ◻
This is Hofmann’s quotient construction [Hof95]. His primitive substitution and our 𝖩 define one another through transport (construction 30.9); his 𝖨𝖽𝖴𝗇𝗂 and 𝖤𝗑𝗍 are the two axioms of 𝑇𝐼. Choosing a quotient representative is metatheoretic, so the proof gives existence, not a normalization algorithm.
Theorem 35.39 concerns inhabitation, not the conservation of judgmental equations. Reflection can turn a constructed identification into an equation. For example, writing 𝗌𝗎𝖼𝑥(𝟢) for the 𝑥-fold iterate of 𝗌𝗎𝖼 on 𝟢 defined by primitive recursion, induction constructs an inhabitant of 𝖨𝖽ℕ(𝑥,𝗌𝗎𝖼𝑥(𝟢)). Hence 𝑇𝐸 derives 𝑥:ℕ⊢𝑥≡𝗌𝗎𝖼𝑥(𝟢):ℕ by Id-Reflect. This calculation illustrates what reflection does; comparison with judgmental equality in 𝑇𝐼 is outside this example.
The signature of theorem 35.39 is exactly the Hofmann core 𝑇H of definition 35.26. Adding a former requires both a canonical action on comparisons and the eliminator-compatibility calculation of lemma 35.37; the book’s universe hierarchy, W-types, and other large eliminations are outside that signature.
Kapulkin and Li’s exact intensional models are contextual categories with 𝖨𝖽-, Π𝖤𝗑𝗍-, and Σ-structure; the Π𝖤𝗑𝗍 structure already includes function extensionality. Their category 𝖢𝗑𝗅𝖢𝖺𝗍𝖨𝖳𝖳+𝖴𝖨𝖯 adds chosen UIP structure. The extensional category 𝖢𝗑𝗅𝖢𝖺𝗍𝖤𝖳𝖳 instead has equality reflection. Both carry the left semi-model structures fixed in their paper. For these categories, Morita equivalent means that a free–forgetful adjunction is a Quillen adjunction and that its unit is a weak equivalence at every cofibrant intensional model. This is an equivalence of model categories up to the specified weak equivalences, not equality of raw syntax and not a theorem about every theory named ITT or ETT.
At the signature of definition 90.47, the free–forgetful adjunction 𝖢𝗑𝗅𝖢𝖺𝗍𝖨𝖳𝖳+𝖴𝖨𝖯⟨−⟩∘𝖤𝖳𝖳⇄|−|𝖢𝗑𝗅𝖢𝖺𝗍𝖤𝖳𝖳 is a Morita equivalence. In particular, the result applies to cofibrant extensions by new types, terms, and propositional equations at that same logical signature.
Proof of Theorem 90.48 — Imported: Kapulkin–Li Morita equivalence
Proof. This is Theorem 7.3 of [KL25]. The forgetful functor preserves fibrations and acyclic fibrations. Their quotient construction supplies its left adjoint; Lemmas 5.8 and 7.2 show that the unit is a weak equivalence on cellular models, and cellular replacement plus the two-out-of-three property extends the conclusion to every cofibrant model. The theorem does not assert syntactic conservativity for arbitrary extensions. ◻
Neither 𝑇𝖿𝖺𝗆 nor 𝑇𝖼𝗈 is in definition 90.47, and neither is in the Hofmann core of definition 35.26. Adding the indexed-family schema or coinductive records therefore requires a new action on comparison maps and a new eliminator-compatibility proof. No theorem in this section supplies it.
Reflection does simplify a single indexed branch once evidence is present. If 𝑝:𝖤𝗊ℕ(𝑘,𝗌𝗎𝖼𝑛),𝑢:𝑃(𝑘), then Eq-Reflect gives 𝑘≡𝗌𝗎𝖼𝑛, congruence gives 𝑃(𝑘)≡𝑃(𝗌𝗎𝖼𝑛), and Conv reclassifies the unchanged term as 𝑢:𝑃(𝗌𝗎𝖼𝑛). An intensional branch would retain an explicit transport. The calculation does not decide whether 𝑝 exists; making this equality part of conversion is exactly what invalidates conversion-driven pattern compilation as an algorithm.
★★☆ Write the full primitive-𝖩 term used in lemma 35.30. With 𝐼:=𝖨𝖽𝐴(𝑥,𝑦), its two-endpoint motive is 𝑥,𝑦:𝐴,𝑞:𝐼⊢∏𝑝:𝐼𝖨𝖽𝐼(𝑝,𝑞). Show that its diagonal clause is 𝑧.𝜆𝑝.𝗎𝗂𝗉(𝑝), and verify the resulting classifier for arbitrary 𝑝,𝑞:𝖨𝖽𝐴(𝑎,𝑏).
★★☆ Construct, by ℕ-induction in the base, a term 𝑥:ℕ⊢𝑃:𝖨𝖽ℕ(𝑥,𝗌𝗎𝖼𝑥(𝟢)), using reflexivity at zero and congruence of 𝗌𝗎𝖼 in the inductive step. Then apply Id-Reflect in 𝑇𝐸 and state the resulting judgmental equality.
Fix an effective Gödel coding of finite raw terms, contexts, and finite derivation trees by natural numbers, and fix an ordinary deterministic Turing machine model. A relation on these codes is decidable when some total machine computes its characteristic function. “Computable encoding” means a total machine computing the output code. These are statements in the ambient metatheory, not typing judgments internal to ETT.
Castellan, Clairambault, and Dybjer separate two undecidability endpoints [CCD17]. With one base type, dependent products, and extensional identity, type inhabitation and judgmental equality are undecidable; the judgmental-equality result remains true after adding unit and dependent sums. With no base type but one universe containing a chosen type, dependent products, and extensional identity, judgmental equality is again undecidable. The local construction below spells out this second, one-universe reduction. The free-lccc bifreeness theorem from the same paper is not a premise of that calculation.
The set Λ of combinators is generated by 𝑡::=𝖲∣𝖪∣𝑡𝑡, with application associated to the left. Conversion ∼ is the least equivalence relation closed under
𝖪𝑡𝑢∼𝑡
SK-K
𝖲𝑡𝑢𝑣∼(𝑡𝑣)(𝑢𝑣)
SK-S
𝑡∼𝑡′𝑢∼𝑢′
𝑡𝑢∼𝑡′𝑢′
SK-App
Equivalently, orient the K and S equations from left to right, close one step under application contexts, and write 𝑡⟶∗𝑢 for its reflexive–transitive closure; ∼ is the least equivalence relation containing that closure.
Proof of Lemma 35.44 — The SK word problem is undecidable
Proof. This is the classical word-problem theorem for combinatory logic with the 𝖪 and 𝖲 equations and congruence. We import the theorem at exactly that signature; Statman proves the word-problem result [Sta00], and the same result is the explicit input to the type-theoretic encoding of Castellan, Clairambault, and Dybjer [CCD17]. The grammar has no variables, so every term in Λ is already closed. No claim about a particular reduction strategy or about normalization is needed here. ◻
In ETT with U0, let Γ𝖲𝖪:=(𝑋:U0,𝑎𝑝𝑝:∏𝑥:𝑋∏𝑦:𝑋𝑋,𝑠:𝑋,𝑘:𝑋,𝑒𝐾:∏𝑎:𝑋∏𝑏:𝑋𝖤𝗊𝑋(𝑘⋅𝑎⋅𝑏,𝑎),𝑒𝑆:∏𝑎:𝑋∏𝑏:𝑋∏𝑐:𝑋𝖤𝗊𝑋(𝑠⋅𝑎⋅𝑏⋅𝑐,(𝑎⋅𝑐)⋅(𝑏⋅𝑐))), where 𝑢⋅𝑣:=𝑎𝑝𝑝𝑢𝑣. Recursively define ⌜𝖲⌝:=𝑠,⌜𝖪⌝:=𝑘,⌜𝑡𝑢⌝:=⌜𝑡⌝⋅⌜𝑢⌝. Thus Γ𝖲𝖪⊢⌜𝑡⌝:𝑋 for every 𝑡∈Λ.
Proof. Induct on the derivation of 𝑡∼𝑢. In the 𝖪 case, 𝑒𝐾⌜𝑡⌝⌜𝑢⌝ inhabits 𝖤𝗊𝑋(⌜𝖪𝑡𝑢⌝,⌜𝑡⌝), and Eq-Reflect gives the required equation. In the 𝖲 case, 𝑒𝑆⌜𝑡⌝⌜𝑢⌝⌜𝑣⌝ inhabits 𝖤𝗊𝑋(⌜𝖲𝑡𝑢𝑣⌝,⌜(𝑡𝑣)(𝑢𝑣)⌝), so Eq-Reflect gives the encoded 𝑆𝐾−𝑆 equation. The application case is application congruence (remark 27.4); reflexivity, symmetry, and transitivity use the corresponding rules for judgmental equality. ◻
Proof of Lemma 35.47 — Completeness of the encoding
Proof. Write [𝑡] for the ∼-class of 𝑡. Interpret the context Γ𝖲𝖪 in the set model of proposition 35.4 by 𝑋:=Λ/∼,𝑎𝑝𝑝([𝑡],[𝑢]):=[𝑡𝑢],𝑠:=[𝖲],𝑘:=[𝖪]. The operation on classes is well defined by SK-App. The two remaining components 𝑒𝐾,𝑒𝑆 are the unique elements of their singleton equality fibers; those fibers are inhabited by SK-K and SK-S. This is a legitimate U0-environment. Under the fixed finite-tree coding of convention 90.50, identify Λ with a subset of ℕ. Since ℕ∈V0 and a Grothendieck universe is closed under subsets, Λ∈V0. Then P(Λ)∈V0, and Λ/∼⊆P(Λ) puts the quotient itself in V0. This uses the closure properties, not countability alone.
Induction on 𝑡 gives [[⌜𝑡⌝]]=[𝑡]. Soundness of the set interpretation therefore sends the assumed judgmental equality to [𝑡]=[𝑢], which means 𝑡∼𝑢. ◻
Proof of Lemma 35.48 — Generation for equality formation
Proof. The naive invariant “inspect only the outer constructor of the conclusion” is not stable under the rules. Substitution can expose an equality former, for example when 𝐷(𝑥):=𝑥 and the substituted term itself is 𝖤𝗊𝐴(𝑎,𝑏); a Russell-universe elimination can likewise place an 𝖤𝗊-headed code in a classifier. Hence the induction must inspect subjects, equality endpoints, classifiers, and every declaration type, as stated below.
Use simultaneous rule induction over the five judgment forms (remark 26.23). The strengthened invariant examines every constituent expression of the conclusion: subjects, both sides of an equality, classifiers, and the declaration types inside its context. If any such constituent has displayed outer constructor 𝖤𝗊, its two endpoints have the displayed ambient type. Thus the invariant also covers an 𝖤𝗊-headed classifier, an 𝖤𝗊-headed declaration, and a term of a Russell universe. The lemma is the type-formation instance of this stronger assertion.
A final Eq-F has premises Γ⊢𝑎:𝐴 and Γ⊢𝑏:𝐴, exactly the required endpoint derivations; Eq-Form-U has the same endpoint premises, and Eq-F-eq has them for both equality types. If U-El concludes that an 𝖤𝗊-headed universe element 𝐸 is a type, the induction hypothesis for its premise Γ⊢𝐸:U𝑖 gives the endpoint derivations.
The only rule that can expose a new outer constructor is substitution. Raw substitution has the dichotomy 𝐸[𝑎/𝑥]is𝖤𝗊-headed⟹𝐸=𝖤𝗊𝐴0(𝑢,𝑣)or(𝐸=𝑥and𝑎=𝖤𝗊𝐴0(𝑢,𝑣)). In the first case the judgment-premise induction hypothesis gives 𝑢:𝐴0 and 𝑣:𝐴0; Subst derives 𝑢[𝑎/𝑥]:𝐴0[𝑎/𝑥] and 𝑣[𝑎/𝑥]:𝐴0[𝑎/𝑥]. In the second case the typing-premise induction hypothesis gives 𝑢:𝐴0 and 𝑣:𝐴0 for the substituend, and weakening through Δ[𝑎/𝑥] places both judgments in the conclusion context. Equal substitution uses the same dichotomy and its equality rules align the two resulting ambient types.
Every other rule obeys one preservation principle. A newly constructed conclusion has a fixed non-𝖤𝗊 head; an 𝖤𝗊-headed constituent retained from a premise is handled by that premise’s induction hypothesis; and an instantiated branch is handled by the substitution dichotomy. Context extension and variables use the induction hypotheses for their declaration types. Equality, conversion, presupposition, universe, lifting, and the core former rules all have one of these three shapes. Therefore the strengthened invariant, and hence the stated formation case, holds. ◻
An input contains derivation trees of Γ⊢𝑎:𝐴 and Γ⊢𝑏:𝐴; decide whether Γ⊢𝑎≡𝑏:𝐴 is derivable. The supplied trees make this a decision problem on well-typed endpoints, not a hidden typechecking problem.
Typechecking.
On a raw finite triple (Γ,𝑎,𝐴), decide whether Γ⊢𝑎:𝐴 is derivable.
Typehood.
On a raw finite pair (Γ,𝐴), decide whether Γ⊢𝐴𝗍𝗒𝗉𝖾 is derivable.
A decider must be total on every code of the indicated form. Malformed raw inputs are negative instances of the last two problems.
In ETT with the Russell universes of definition 29.1, none of the three problems in definition 90.58 is decidable. The effective reductions from judgmental equality to typechecking and from typechecking to typehood use only plain ETT.
Proof.Lemma 35.46 gives the forward implication and lemma 35.47 the backward one in 𝑡∼𝑢⟺Γ𝖲𝖪⊢⌜𝑡⌝≡⌜𝑢⌝:𝑋. The context, the two endpoint-typing derivations, and the encoded terms are computed by structural recursion on the finite SK trees. Hence this is a total reduction to the first problem of definition 90.58, and lemma 35.44 gives its undecidability.
Now suppose Γ⊢𝑎:𝐴 and Γ⊢𝑏:𝐴. Then Γ⊢𝑎≡𝑏:𝐴 holds if and only if Γ⊢𝗋𝖾𝖿𝗅:𝖤𝗊𝐴(𝑎,𝑏): reflection proves the reverse implication, and theorem 35.7(1) proves the forward one. Thus a typechecking algorithm would decide equality.
Finally, Γ⊢𝑎:𝐴⟺Γ⊢𝖤𝗊𝐴(𝑎,𝑎)𝗍𝗒𝗉𝖾. Rule Eq-F proves the forward implication, while lemma 35.48 proves the reverse. Hence a typehood algorithm would decide typechecking. Both transformations are primitive recursions on raw syntax and hence total under the fixed coding. All three problems are therefore undecidable. ◻
Add the universes of definition 29.1 to ETT and work in the context Γ:=𝑋:U0,𝑝:𝖤𝗊U0(𝑋,𝑋→𝑋). The context is well formed because 𝑋→𝑋:U0. Reflection gives Γ⊢𝑋≡𝑋→𝑋:U0; rule U-El-Eq of definition 29.1 turns this into Γ⊢𝑋≡𝑋→𝑋𝗍𝗒𝗉𝖾. For 𝑥:𝑋, conversion therefore gives 𝑥:𝑋→𝑋, so 𝑥𝑥:𝑋 and 𝜔:=𝜆𝑥.𝑥𝑥:𝑋→𝑋. Converting once more gives 𝜔:𝑋; hence Ω:=𝜔𝜔:𝑋 and Ω⟶𝛽Ω. Thus open ETT terms need not normalize. This is independent of theorem 35.49. The context need not be inhabitable; a type checker must respond to every context.
The local set models prove soundness of the extensional delta and optional truncation (proposition 35.4, corollary 35.19). What fails is a complete terminating decision procedure for the raw judgments of theorem 35.49. A checker that demands explicit equality evidence can verify the evidence it is given; it still cannot decide conversion between two bare terms.
★★☆ Write out the induction cases in lemma 35.46 for the closure rules of ∼. For given 𝑡,𝑢,𝑣, derive the encoded reflexivity ⌜𝑡⌝≡⌜𝑡⌝, the symmetry and transitivity steps, and the SK-App congruence step, all in Γ𝖲𝖪 at type 𝑋. Explain why the context’s two equation families 𝑒𝐾,𝑒𝑆 are the only nonstructural hypotheses used.
★★☆ Reconstruct the encoding of one SK reduction step as an equality-reflection derivation. Separate the use of extensional equality evidence from the use of Eq-Reflect, and show why erasing the evidence cannot give a decision procedure for bare conversion.
★★★Practical project.ett-evidence-checker Before implementing the checker, write the complete accepted derivation for 𝑒𝐾𝑠𝑘 and a rejected derivation attempt whose two endpoints have different classifiers; mark the premise at which it fails. Implement in Agda or Kappa a checker that verifies explicitly supplied ETT identity evidence and then reflects it. The checker must preserve typing of both equality endpoints. Accept the encoded 𝐾𝑥𝑦→𝑥 step, reject a proof whose endpoints encode different result types, and print the reflected equation; do not search for evidence.
Sources. Martin-Löf introduced extensional type theory [ML82, ML84]. Our propositions and truncation follow [AG26]; for squash and bracket types see [CAB^+86, AB04]. Hofmann proves theorem 35.39 and extensional undecidability in Chapter 3 of [Hof95]: the extension criterion is §3.2.6, and the quotient and universe results are Theorems 3.2.18 and 3.2.20. The conservativity theorem above is restricted to the Hofmann core named in remark 35.42; the Russell hierarchy used for the separate SK model is not silently included in that quotient construction. For SK see [CCD17] and lemma 35.44; the modern model-level endpoint is [KL25]. For choice see [Hyl82, Dia75].