Observational Equality and Computational Extensionality
Observational equality is equality defined by the type being observed. In particular, 𝑓≈∏𝑥:𝐴𝐵𝑔≡∏𝑥:𝐴𝑓(𝑥)≈𝐵(𝑥)𝑔(𝑥). Equality proofs are irrelevant, while a separate 𝖼𝖺𝗌𝗍 transports proof-relevant data between equal types. We call the cumulative Π/ℕ/strict-proposition core with these operations TTobs22.
Strict propositions
Add strict proposition sorts𝖲𝖯𝗋𝗈𝗉𝑖 whose inhabitants are judgmentally proof-irrelevant: if 𝑝,𝑞:𝑃:𝖲𝖯𝗋𝗈𝗉𝑖, then 𝑝≡𝑞.
The theory extends the base by a second hierarchy of universes 𝖲𝖯𝗋𝗈𝗉0,𝖲𝖯𝗋𝗈𝗉1,…, the sorts of strict propositions, whose inhabitants are judgmentally proof-irrelevant (also written 𝖲𝖯𝗋𝗈𝗉 in implementations [GCST19]), governed by the following rules. We write 𝑠𝑖 for a sort, ranging over {U𝑖,𝖲𝖯𝗋𝗈𝗉𝑖}.
Γ𝖼𝗍𝗑𝑖<𝑗
Γ⊢𝖲𝖯𝗋𝗈𝗉𝑖:U𝑗
Sort-F
Γ⊢𝐴:𝑠𝑖𝑖≤𝑗
Γ⊢𝐴:𝑠𝑗
Cum
Γ⊢𝐴:𝖲𝖯𝗋𝗈𝗉𝑖Γ⊢𝑝:𝐴Γ⊢𝑞:𝐴
Γ⊢𝑝≡𝑞:𝐴
Irr
Rule Irr is the defining feature: any two inhabitants of a strict proposition are judgmentally equal. Rule Cum makes both hierarchies cumulative (U𝑖 as well as 𝖲𝖯𝗋𝗈𝗉𝑖); this is not a convenience but a load-bearing requirement (remark 79.13).
An implicit universe annotation is a level omitted from the written term and recovered from its premises. Every such level is the least common upper level required by the premises. The symbols 𝗉𝗋1,𝗉𝗋2 eliminate both strict pairs and Σ-pairs; the type of their argument determines which rule applies.
The sorts 𝖲𝖯𝗋𝗈𝗉𝑖 are inhabited by the following formers.
Γ𝖼𝗍𝗑
Γ⊢⊥:𝖲𝖯𝗋𝗈𝗉𝑖
Bot-F
Γ⊢𝐴:𝑠𝑖Γ⊢𝑝:⊥
Γ⊢𝗋𝖾𝖼⊥(𝐴,𝑝):𝐴
Bot-E
Γ𝖼𝗍𝗑
Γ⊢⊤:𝖲𝖯𝗋𝗈𝗉𝑖
Top-F
Γ𝖼𝗍𝗑
Γ⊢⋆:⊤
Top-I
Γ⊢𝑃:𝖲𝖯𝗋𝗈𝗉𝑖Γ,𝑥:𝑃⊢𝑄:𝖲𝖯𝗋𝗈𝗉𝑖
Γ⊢∃(𝑥:𝑃).𝑄:𝖲𝖯𝗋𝗈𝗉𝑖
Ex-F
Γ⊢𝑝:𝑃Γ⊢𝑞:𝑄[𝑝/𝑥]
Γ⊢(𝑝,𝑞):∃(𝑥:𝑃).𝑄
Ex-I
Γ⊢𝑟:∃(𝑥:𝑃).𝑄
Γ⊢𝗉𝗋1𝑟:𝑃
Ex-E1
Γ⊢𝑟:∃(𝑥:𝑃).𝑄
Γ⊢𝗉𝗋2𝑟:𝑄[𝗉𝗋1𝑟/𝑥]
Ex-E2
Γ⊢𝐴:𝑠𝑖Γ,𝑥:𝐴⊢𝑃:𝖲𝖯𝗋𝗈𝗉𝑗𝑖,𝑗≤𝑘
Γ⊢∏𝑥:𝐴𝑃:𝖲𝖯𝗋𝗈𝗉𝑘
Pi-Prop-F
We abbreviate 𝑃∧𝑄:=∃(𝑥:𝑃).𝑄 when 𝑄 does not depend on 𝑥, and 𝑃→𝑄:=∏𝑥:𝑃𝑄 likewise. By Pi-Prop-F the sorts 𝖲𝖯𝗋𝗈𝗉 are closed under universal quantification over arbitrary types: a Π-type lands in 𝖲𝖯𝗋𝗈𝗉 as soon as its codomain does.
Proof of Lemma 79.4 — Irrelevance absorbs the missing rules
Proof. (1) Both sides inhabit the strict proposition ∃(𝑥:𝑃).𝑄; apply Irr. (2) By Irr, 𝑢≡⋆ at ⊤, so 𝐶[𝑢/𝑥]≡𝐶[⋆/𝑥] by congruence (definition 26.22), and 𝑐 transfers by conversion. ◻
The empty type 𝟎:U0 of chapter 28 is not a strict proposition: its rules make any two inhabitants propositionally equal (via 𝗂𝗇𝖽𝟎), but not judgmentally so — 𝟎 has no 𝜂-rule. The proposition ⊥ plays the corresponding role in 𝖲𝖯𝗋𝗈𝗉, and Bot-E eliminates into both sorts. In the base extended by definition 79.1, definition 79.3 alone, Bot-E is the only passage from proof-irrelevant hypotheses to proof-relevant conclusions (the 𝖼𝖺𝗌𝗍 of § 79.3 is the second). The terms 𝜆𝑧.𝗋𝖾𝖼⊥(𝟎,𝑧):⊥→𝟎 and 𝜆𝑧.𝗂𝗇𝖽𝟎(𝑧):𝟎→⊥ make the two logically equivalent.
By Sort-F, 𝖲𝖯𝗋𝗈𝗉𝑖 inhabits U𝑗, not 𝖲𝖯𝗋𝗈𝗉𝑗: two propositions (say ⊤ and ⊥) must not be judgmentally identified merely for being propositions. Proof irrelevance identifies inhabitants of one strict proposition; it does not identify two proposition codes.
chapter 66 called 𝐴 a proposition when 𝗂𝗌𝖯𝗋𝗈𝗉(𝐴) is inhabited (definition 66.2): any two elements are propositionally equal. Irr is strictly stronger. If 𝐴:U𝑖 is equivalent to a strict proposition 𝑃:𝖲𝖯𝗋𝗈𝗉𝑖, the equivalence does not derive 𝐴:𝖲𝖯𝗋𝗈𝗉𝑖: strictness is assigned by a sorting judgment, not transported across equivalences. The two notions coexist in implementations: Agda and Rocq provide 𝖲𝖯𝗋𝗈𝗉 exactly as in definition 79.1 (see the bibliographic notes), alongside h-propositions.
★☆☆ Show that ⊤ and ⊥→⊥ are interprovable, and that any two terms of ⊥→⊥ are judgmentally equal. Conclude that in definition 79.3 the former ⊤ is definable and its rules derivable.
★★☆ Explain why an eliminator from ⊥’s relevant cousin — a rule concluding Γ⊢𝑡:𝐴 for 𝐴:U𝑖 from a closed derivation in the empty context of ⊥ — would be harmless, while adding Irr for 𝟎 (i.e., declaring 𝟎:𝖲𝖯𝗋𝗈𝗉0 with its chapter 28 large eliminator) is a design decision requiring justification. Which metatheoretic property of chapter 48’s demand list is at stake when a proof-irrelevant type eliminates into all sorts?
The equality former has reflexivity and a proposition-valued eliminator. Equality between types additionally supports 𝖼𝖺𝗌𝗍, with 𝖼𝖺𝗌𝗍𝗋𝖾𝖿𝗅 witnessing that every self-cast is observationally equal to its input.
Transp is the eliminator 𝖩 of definition 30.1 restricted to proof-irrelevant motives; Cast transports along a proof of equality of types; Cast-Refl asserts, propositionally, that casting a type to itself does nothing. Note that 𝑡≈𝐴𝑢 is formed only for 𝐴 a relevant type: strict propositions need no equality, by Irr.
Proof of Lemma 79.9 — Transp needs no computation rule
Proof. The type 𝐵𝑡𝗋𝖾𝖿𝗅(𝑡) inhabits 𝖲𝖯𝗋𝗈𝗉𝑗; apply Irr. For each groupoid law of theorem 30.20, its two sides are inhabitants of the same strict proposition 𝑢≈𝐴𝑣; a direct instance of Irr therefore identifies them judgmentally. The intensional base instead proves those laws propositionally by path induction. ◻
Let Γ⊢𝐴:U𝑖 and Γ⊢𝑒:𝑡≈𝐴𝑢. Reading a family Γ,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾 as a map 𝐵:𝐴→U𝑗 (chapter 29), define:
𝑒−1:=𝗍𝗋𝖺𝗇𝗌𝗉(𝑡,𝜆𝑦.𝜆_.𝑦≈𝐴𝑡,𝗋𝖾𝖿𝗅(𝑡),𝑢,𝑒):𝑢≈𝐴𝑡;
for Γ⊢𝑒′:𝑢≈𝐴𝑣: 𝑒⋅𝑒′:=𝗍𝗋𝖺𝗇𝗌𝗉(𝑢,𝜆𝑦.𝜆_.𝑡≈𝐴𝑦,𝑒,𝑣,𝑒′):𝑡≈𝐴𝑣;
for Γ⊢𝑓:𝐴→𝐶 with 𝐶:U𝑗: 𝖺𝗉𝑓(𝑒):=𝗍𝗋𝖺𝗇𝗌𝗉(𝑡,𝜆𝑦.𝜆_.𝑓𝑡≈𝐶𝑓𝑦,𝗋𝖾𝖿𝗅(𝑓𝑡),𝑢,𝑒):𝑓𝑡≈𝐶𝑓𝑢; in particular 𝖺𝗉𝐵(𝑒):𝐵𝑡≈U𝑗𝐵𝑢 for a type family 𝐵, since 𝐵𝑡≈U𝑗𝐵𝑦 is itself a strict proposition and hence a legitimate motive for Transp.
Each motive is 𝖲𝖯𝗋𝗈𝗉-valued, so Transp applies; the required base cases are given by 𝗋𝖾𝖿𝗅. By lemma 79.9, all equations among these operations hold judgmentally.
If 𝐴 is neutral, then 𝑡≈𝐴𝑢 is neutral. Otherwise the rules reduce 𝐴 to weak-head normal form; at an inductive type they also reduce 𝑡,𝑢 enough to expose their constructors. Thus equality computation is driven by its type index.
The Π-, ℕ-, universe-, and strict-proposition clauses belong to TTobs22. For the dependent-pair and Boolean calculations in this section, write the Σ/𝟐 fragment for that core with the displayed Σ- and 𝟐-clauses adjoined. Claims about this larger fragment use the observational-CIC metatheory only when their theorem statement says so.
Reduce 𝑡≈𝐴𝑢 after 𝐴 reaches weak-head normal form. At an inductive type, first reduce the endpoints enough to expose their constructors. The clauses below are definitional equalities in 𝖲𝖯𝗋𝗈𝗉.
The dependent-pair clause exposes why a homogeneous componentwise definition does not typecheck. Given 𝑝,𝑞:∑𝑥:𝐴𝐵, their second projections have types 𝐵[𝗉𝗋1𝑝/𝑥] and 𝐵[𝗉𝗋1𝑞/𝑥] respectively, so the tempting second conjunct 𝗉𝗋2𝑝≈𝐵[𝗉𝗋1𝑝/𝑥]𝗉𝗋2𝑞 is ill-formed. The first component equality must first be mapped through 𝐵 and used to cast 𝗉𝗋2𝑝 into the type of 𝗉𝗋2𝑞; this is the cast visible in the dependent-pair clause.
For the rule display, abbreviate the first-component equality and the cast second component by 𝐸𝐴(𝑝,𝑞):=𝗉𝗋1𝑝≈𝐴𝗉𝗋1𝑞,𝑝𝑒2:=𝖼𝖺𝗌𝗍(𝐵[𝗉𝗋1𝑝/𝑥],𝐵[𝗉𝗋1𝑞/𝑥],𝖺𝗉𝐵(𝑒),𝗉𝗋2𝑝),𝐸𝐵(𝑝,𝑞,𝑒):=𝑝𝑒2≈𝐵[𝗉𝗋1𝑞/𝑥]𝗉𝗋2𝑞. Also put 𝛿𝟐(𝑏,𝑏′):=⊤ when the two canonical constructors agree, and 𝛿𝟐(𝑏,𝑏′):=⊥ otherwise.
At each former (endpoints of the given type):
Γ⊢𝑓,𝑔:∏𝑥:𝐴𝐵
Γ⊢(𝑓≈∏𝑥:𝐴𝐵𝑔)≡∏𝑥:𝐴𝑓𝑥≈𝐵𝑔𝑥:𝖲𝖯𝗋𝗈𝗉
Obs-Pi
Γ⊢𝑝,𝑞:∑𝑥:𝐴𝐵
Γ⊢(𝑝≈∑𝑥:𝐴𝐵𝑞)≡∃(𝑒:𝐸𝐴(𝑝,𝑞)).𝐸𝐵(𝑝,𝑞,𝑒):𝖲𝖯𝗋𝗈𝗉
Obs-Sg
Γ𝖼𝗍𝗑
Γ⊢(𝟢≈ℕ𝟢)≡⊤:𝖲𝖯𝗋𝗈𝗉
Obs-Nat-ZZ
Γ⊢𝑚,𝑛:ℕ
Γ⊢(𝗌𝗎𝖼(𝑚)≈ℕ𝗌𝗎𝖼(𝑛))≡(𝑚≈ℕ𝑛):𝖲𝖯𝗋𝗈𝗉
Obs-Nat-SS
Γ⊢𝑛:ℕ
Γ⊢(𝟢≈ℕ𝗌𝗎𝖼(𝑛))≡⊥:𝖲𝖯𝗋𝗈𝗉
Obs-Nat-ZS
Γ⊢𝑛:ℕ
Γ⊢(𝗌𝗎𝖼(𝑛)≈ℕ𝟢)≡⊥:𝖲𝖯𝗋𝗈𝗉
Obs-Nat-SZ
𝑏,𝑏′arecanonicalBooleanconstructors
Γ⊢(𝑏≈𝟐𝑏′)≡𝛿𝟐(𝑏,𝑏′):𝖲𝖯𝗋𝗈𝗉
Obs-Bool
At the sorts (endpoints are types). Write 𝗁𝖽(𝐴) for the head constructor of a weak-head normal type: 𝗁𝖽(ℕ)=ℕ, 𝗁𝖽(𝟐)=𝟐, 𝗁𝖽(𝑠𝑖)=𝑠𝑖, and 𝗁𝖽 of a Π-, Σ- or quotient type is its former. For 𝑒:𝐴≈U𝑖𝐴′, abbreviate 𝑎′𝑒:=𝖼𝖺𝗌𝗍(𝐴′,𝐴,𝑒−1,𝑎′),𝐷Π(𝑒):=∏𝑎′:𝐴′𝐵[𝑎′𝑒/𝑥]≈U𝑗𝐵′[𝑎′/𝑥],𝑎𝑒:=𝖼𝖺𝗌𝗍(𝐴,𝐴′,𝑒,𝑎),𝐷Σ(𝑒):=∏𝑎:𝐴𝐵[𝑎/𝑥]≈U𝑗𝐵′[𝑎𝑒/𝑥].
Two rules of definition 79.11 lower the universe level as they compute, and are well-typed only thanks to Cum. In Obs-Prop, the left-hand side inhabits 𝖲𝖯𝗋𝗈𝗉𝑖+1 (form 𝑃≈𝖲𝖯𝗋𝗈𝗉𝑖𝑄 via 𝖲𝖯𝗋𝗈𝗉𝑖:U𝑖+1), while the right-hand side inhabits 𝖲𝖯𝗋𝗈𝗉𝑖; the rule is an equation at 𝖲𝖯𝗋𝗈𝗉𝑖+1 after lifting by Cum. In Obs-U-Pi, the component equalities inhabit 𝖲𝖯𝗋𝗈𝗉𝑖+1 and 𝖲𝖯𝗋𝗈𝗉𝑗+1, while the left side inhabits 𝖲𝖯𝗋𝗈𝗉𝑘+1 for 𝑘≥𝑖,𝑗. Cumulativity embeds both component propositions at that common level.
Proof of Theorem 79.15 — Extensionality, judgmentally
Proof. (1) is an instance of Irr, since 𝑡≈𝐴𝑢:𝖲𝖯𝗋𝗈𝗉𝑖. (2) By Obs-Pi the codomain is judgmentally the domain; the identity function typechecks by conversion (definition 26.22). (3) Identical, by Obs-Prop. ◻
With + defined by recursion on its first argument, there is a closed term ℎ:𝜆𝑛.𝑛+𝟢≈ℕ→ℕ𝜆𝑛.𝑛. By Obs-Pi, it suffices to inhabit ∏𝑛:ℕ𝑛+𝟢≈ℕ𝑛. Induct on 𝑛 with that 𝖲𝖯𝗋𝗈𝗉-valued motive. The zero case computes to ⊤ by Obs-Nat-ZZ; the successor case computes by Obs-Nat-SS to the induction hypothesis. The eliminator assembled from these two clauses is the required ℎ.
By Obs-Pi, the type of pointwise equality is judgmentally the type of function equality, so 𝜆ℎ.ℎ proves function extensionality. This computation replaces the reflection step used in ETT. The remaining local metatheoretic obligation is to show that the new equations preserve normalization and decidable conversion (theorem 79.26).
★★★ Verify the typing of the three clauses of construction 79.10 in detail, exhibiting each motive and its sort. Then define the dependent 𝖺𝗉𝖽: for Γ⊢𝑓:∏𝑥:𝐴𝐵 and Γ⊢𝑒:𝑡≈𝐴𝑢, construct a proof of 𝖼𝖺𝗌𝗍(𝐵[𝑡/𝑥],𝐵[𝑢/𝑥],𝖺𝗉𝐵(𝑒),𝑓𝑡)≈𝐵[𝑢/𝑥]𝑓𝑢.
★★☆ Write the eliminator term implicit in construction 215.15, including its motive and both branches, and check its type by the computation rules for + and observational equality. Then repeat the construction for 𝜆𝑛.𝟢+𝑛, noting which direction of recursion makes its successor branch compute by the natural-number equations.
★★★ Formulate the computation rules of ≈ for the W-types of chapter 28 (definition 28.28): the rule at 𝖶𝑥:𝐴𝐵≈U𝖶𝑥:𝐴′𝐵′, and the rule for two elements 𝗌𝗎𝗉(𝑎,𝑓), 𝗌𝗎𝗉(𝑎′,𝑓′), following the pattern of Obs-U-Sg and Obs-Sg. Check that your rule for elements makes the encoded numerals of theorem 28.32 with distinct child-functions observationally equal.
★★☆ Show that the non-dependent special case of Transp (motive 𝐵:𝐴→𝖲𝖯𝗋𝗈𝗉𝑗 not depending on the proof) suffices to derive the full rule, using Irr to repair the proof-dependency.
𝖼𝖺𝗌𝗍 computes by the following rules (levels and sorts compressed per convention 79.2). For the dependent rules, write 𝑎𝑒(𝑎′):=𝖼𝖺𝗌𝗍(𝐴′,𝐴,(𝗉𝗋1𝑒)−1,𝑎′),𝑒𝐵(𝑎′):=(𝗉𝗋2𝑒)𝑎′,𝑏𝑒,𝑓(𝑎′):=𝖼𝖺𝗌𝗍(𝐵[𝑎𝑒(𝑎′)/𝑥],𝐵′[𝑎′/𝑥],𝑒𝐵(𝑎′),𝑓𝑎𝑒(𝑎′)),𝖼𝗉(𝑒,𝑓):=𝜆𝑎′.𝑏𝑒,𝑓(𝑎′),𝑎𝑒(𝑝):=𝖼𝖺𝗌𝗍(𝐴,𝐴′,𝗉𝗋1𝑒,𝗉𝗋1𝑝),𝑏𝑒(𝑝):=𝖼𝖺𝗌𝗍(𝐵[𝗉𝗋1𝑝/𝑥],𝐵′[𝑎𝑒(𝑝)/𝑥],(𝗉𝗋2𝑒)(𝗉𝗋1𝑝),𝗉𝗋2𝑝),𝖼𝗌(𝑒,𝑝):=(𝑎𝑒(𝑝),𝑏𝑒(𝑝)).
Γ⊢𝑒:ℕ≈U0ℕ
Γ⊢𝖼𝖺𝗌𝗍(ℕ,ℕ,𝑒,𝟢)≡𝟢:ℕ
Cast-Nat-Z
Γ⊢𝑒:ℕ≈U0ℕΓ⊢𝑛:ℕ
Γ⊢𝖼𝖺𝗌𝗍(ℕ,ℕ,𝑒,𝗌𝗎𝖼(𝑛))≡𝗌𝗎𝖼(𝖼𝖺𝗌𝗍(ℕ,ℕ,𝑒,𝑛)):ℕ
Cast-Nat-S
Γ⊢𝑒:𝟐≈U0𝟐𝑏∈{𝗍𝗍,𝖿𝖿}
Γ⊢𝖼𝖺𝗌𝗍(𝟐,𝟐,𝑒,𝑏)≡𝑏:𝟐
Cast-Bool
Γ⊢𝑒:𝑠𝑖≈U𝑖+1𝑠𝑖Γ⊢𝐴:𝑠𝑖
Γ⊢𝖼𝖺𝗌𝗍(𝑠𝑖,𝑠𝑖,𝑒,𝐴)≡𝐴:𝑠𝑖
Cast-U
Γ⊢𝑒:∏𝑥:𝐴𝐵≈U∏𝑥:𝐴′𝐵′Γ⊢𝑓:∏𝑥:𝐴𝐵
Γ⊢𝖼𝖺𝗌𝗍(∏𝑥:𝐴𝐵,∏𝑥:𝐴′𝐵′,𝑒,𝑓)≡𝖼𝗉(𝑒,𝑓):∏𝑥:𝐴′𝐵′
Cast-Pi
Γ⊢𝑒:∑𝑥:𝐴𝐵≈U∑𝑥:𝐴′𝐵′Γ⊢𝑝:∑𝑥:𝐴𝐵
Γ⊢𝖼𝖺𝗌𝗍(∑𝑥:𝐴𝐵,∑𝑥:𝐴′𝐵′,𝑒,𝑝)≡𝖼𝗌(𝑒,𝑝):∑𝑥:𝐴′𝐵′
Cast-Sg
In Cast-Pi and Cast-Sg, the premise abbreviations are part of the rule. The direction of the domain cast in Cast-Pi is forced. A new argument 𝑎′:𝐴′ cannot be supplied directly to 𝑓:∏𝑥:𝐴𝐵; casting it forward would still have codomain 𝐴′. It must first be cast backward along the inverse of the domain equality, producing the 𝑎:𝐴 at which 𝑓 can be evaluated. Writing 𝑒𝐴 for the domain component and 𝑒𝐵 for the dependent codomain component of the equality proof, the two cast directions are 𝑎′:𝐴′𝖼𝖺𝗌𝗍(𝑒−1𝐴,−)↦←←←←←←←←←←←←←←←←←←←→𝑎:𝐴𝑓↦←←←←←→𝑓(𝑎):𝐵(𝑎)𝖼𝖺𝗌𝗍(𝑒𝐵(𝑎′),−)↦←←←←←←←←←←←←←←←←←←←←←←←→𝐵′(𝑎′), whereas a dependent pair first moves its first component forward and then moves the second component between the resulting fibers: 𝑎:𝐴𝖼𝖺𝗌𝗍(𝑒𝐴,−)↦←←←←←←←←←←←←←←←←←←→𝑎′:𝐴′,𝐵(𝑎)𝖼𝖺𝗌𝗍(𝑒𝐵(𝑎),−)↦←←←←←←←←←←←←←←←←←←←←←←→𝐵′(𝑎′). In Cast-Pi, the proof 𝑒 has, by Obs-U-Pi, the type ∃(𝑒0:𝐴≈U𝐴′).∏𝑎′:𝐴′𝐵[…/𝑥]≈U𝐵′[𝑎′/𝑥]. Thus 𝗉𝗋1𝑒 and 𝗉𝗋2𝑒 are its components; the new function coerces its argument backwards along (𝗉𝗋1𝑒)−1, applies 𝑓, and coerces the result forwards — the contravariant twist of the observational approach. 𝖼𝖺𝗌𝗍 between types with distinct heads is never provably possible (𝑒 would inhabit ⊥ by Obs-U-Neq), and is stuck; likewise when either type, or a required endpoint, is neutral.
𝖼𝖺𝗌𝗍(𝐴,𝐴,𝑒,𝑡) is not judgmentally 𝑡 in general — at a Π-type it unfolds to a cast-filled 𝜂-expansion. In the nondependent case a representative reduct is 𝖼𝖺𝗌𝗍(𝐴→𝐵,𝐴→𝐵,𝑒,𝑓)≡𝜆𝑎.𝖼𝖺𝗌𝗍(𝐵,𝐵,𝑒𝐵,𝑓(𝖼𝖺𝗌𝗍(𝐴,𝐴,𝑒−1𝐴,𝑎))). Rule Cast-Refl gives an inhabitant of the observational equality between this reduct and 𝑓, but not a judgmental equation.
For a family 𝐵:𝐴→U𝑗 and Γ⊢𝑝:𝐵𝑡, define 𝗌𝗎𝖻𝗌𝗍𝐵(𝑒,𝑝):=𝖼𝖺𝗌𝗍(𝐵𝑡,𝐵𝑢,𝖺𝗉𝐵(𝑒),𝑝):𝐵𝑢.
For a fully general motive 𝐶:∏𝑥:𝐴(𝑡≈𝐴𝑥)→U𝑗 and Γ⊢𝑐:𝐶𝑡𝗋𝖾𝖿𝗅(𝑡), set 𝐷:=𝜆𝑥.∏𝑒′:𝑡≈𝐴𝑥𝐶𝑥𝑒′:𝐴→U𝑗 and define 𝖩(𝐶,𝑐,𝑢,𝑒):=𝗌𝗎𝖻𝗌𝗍𝐷(𝑒,𝜆𝑒′.𝑐)𝑒:𝐶𝑢𝑒. The abstraction 𝜆𝑒′.𝑐 inhabits 𝐷𝑡 because for 𝑒′:𝑡≈𝐴𝑡 we have 𝑒′≡𝗋𝖾𝖿𝗅(𝑡) by Irr, hence 𝐶𝑡𝑒′≡𝐶𝑡𝗋𝖾𝖿𝗅(𝑡) by congruence.
Proof of Proposition 79.20 — Propositional computation of the derived
Proof. Write 𝐸:=𝖺𝗉𝐷(𝗋𝖾𝖿𝗅(𝑡)). By Cast-Refl, 𝖼𝖺𝗌𝗍𝗋𝖾𝖿𝗅(𝐷𝑡,𝜆𝑒′.𝑐) proves 𝜆𝑒′.𝑐≈𝐷𝑡𝖼𝖺𝗌𝗍(𝐷𝑡,𝐷𝑡,𝐸,𝜆𝑒′.𝑐). By Obs-Pi this proposition is judgmentally ∏𝑒′:𝑡≈𝐴𝑡𝑐≈𝐶𝑡𝑒′𝖼𝖺𝗌𝗍(𝐷𝑡,𝐷𝑡,𝐸,𝜆𝑒′.𝑐)𝑒′; instantiating at 𝗋𝖾𝖿𝗅(𝑡) and taking (⋅)−1 (construction 79.10) yields the claim, since 𝖩(𝐶,𝑐,𝑡,𝗋𝖾𝖿𝗅(𝑡))≡𝖼𝖺𝗌𝗍(𝐷𝑡,𝐷𝑡,𝐸,𝜆𝑒′.𝑐)𝗋𝖾𝖿𝗅(𝑡) by definition. Failure of the judgmental equation is remark 79.18: the left-hand side is a 𝛽-redex whose head 𝖼𝖺𝗌𝗍 unfolds by Cast-Pi into a coerced 𝜂-expansion, not into 𝑐. ◻
Recall the closed stuck transport of chapter 30: in ITT extended by a funext axiom, transporting 𝟢 along the axiom-supplied equality of 𝜆𝑛.𝑛+𝟢 and 𝜆𝑛.𝑛 at the constant family 𝜆𝑓.ℕ has no root reduction: the transport is blocked on the axiom (a judgmental inequality would require normalization for that extended signature). In TTobs22 the corresponding transport does compute. By construction 215.15 there is a term ℎ:𝜆𝑛.𝑛+𝟢≈ℕ→ℕ𝜆𝑛.𝑛, built from 𝗂𝗇𝖽ℕ, not postulated. Transporting at the constant family 𝑃:=𝜆𝑓.ℕ: 𝗌𝗎𝖻𝗌𝗍𝑃(ℎ,𝟢)≡𝖼𝖺𝗌𝗍(ℕ,ℕ,𝖺𝗉𝑃(ℎ),𝟢)≡𝟢 by Cast-Nat-Z — the cast never inspects ℎ. Where the axiomatic theory got stuck on an uninspectable proof, the observational theory computes on the types and ignores the irrelevant proof entirely.
★☆☆ Verify in detail that the right-hand side of Cast-Pi has type ∏𝑥:𝐴′𝐵′: identify the type of (𝗉𝗋2𝑒)𝑎′ supplied by Obs-U-Pi and check that the inner 𝖼𝖺𝗌𝗍 is well-formed.
★★☆ Explain why no computation rule for 𝖼𝖺𝗌𝗍(ℕ,ℕ,𝑒,𝑛) with 𝑛 neutral can be added without breaking confluence with Cast-Nat-Z/Cast-Nat-S, and why 𝖼𝖺𝗌𝗍(𝑋,𝑋,𝑒,𝑡) must be stuck for a type variable 𝑋. (Compare the neutral forms of the base, chapter 49.)
Quotients are the payoff: every type already carries its 𝖲𝖯𝗋𝗈𝗉-valued equality, so a quotient merely replaces it. Write TTobs22+𝖰𝗎𝗈 for the 2022 core with the rules in this section adjoined.
For Γ⊢𝐴:U𝑖, a relation Γ⊢𝑅:𝐴→𝐴→𝖲𝖯𝗋𝗈𝗉𝑖, and proofs 𝑅𝑟,𝑅𝑠,𝑅𝑡 of its reflexivity, symmetry and transitivity, write 𝐴/𝑅 for the quotient carrying all four pieces of data. The witnesses are proof-irrelevant and may be suppressed in terms, but they remain premises of formation: For the longer rules, use the following abbreviations: 𝑥𝑒:=𝖼𝖺𝗌𝗍(𝐴,𝐴′,𝑒,𝑥),𝐷𝑅(𝑒):=∏𝑥,𝑦:𝐴𝑅𝑥𝑦≈𝖲𝖯𝗋𝗈𝗉𝑖𝑅′(𝑥𝑒)(𝑦𝑒),𝑐𝐵,𝑒(𝑏𝑦):=𝖼𝖺𝗌𝗍(𝐵𝜋(𝑦),𝐵𝜋(𝑥),𝖺𝗉𝐵(𝑒)−1,𝑏𝑦),𝑇𝐵,𝑏(𝑥,𝑦,𝑒):=𝑏𝑥≈𝐵𝜋(𝑥)𝑐𝐵,𝑒(𝑏𝑦),𝖢𝗈𝗆𝗉𝖺𝗍𝑅(𝐵,𝑏):=∏𝑥,𝑦:𝐴∏𝑒:𝑅𝑥𝑦𝑇𝐵,𝑏(𝑥,𝑦,𝑒),𝗊𝖾(𝐵,𝑏,𝑏∼,𝑢):=𝗂𝗇𝖽𝐴/𝑅(𝐵,𝑏,𝑏∼,𝑢),𝗊𝗂(𝑃,𝑝,𝑢):=𝗂𝗇𝖽irr𝐴/𝑅(𝑃,𝑝,𝑢).
In the compatibility premise of Quo-E-Rel, the proof 𝑒:𝑅𝑥𝑦 is, by Obs-Quo read right to left, already a proof of 𝜋(𝑥)≈𝐴/𝑅𝜋(𝑦), so 𝖺𝗉𝐵(𝑒) is well-formed (construction 79.10). Rule Quo-E-Irr needs no value-equality premise: both candidate results inhabit the same strict proposition after transport, and Irr identifies them. This split is essential because −≈𝑃− is not formed when 𝑃:𝖲𝖯𝗋𝗈𝗉𝑖.
Obs-Quo makes the quotient effective by computation: 𝜋(𝑡)≈𝐴/𝑅𝜋(𝑢) does not merely imply 𝑅𝑡𝑢 — it is𝑅𝑡𝑢, judgmentally. Compare the set quotients of chapter 68 (definition 68.38), where effectivity is a theorem requiring univalence. The restriction purchasing this convenience is that 𝑅 must be 𝖲𝖯𝗋𝗈𝗉-valued: no proof-relevant information can be extracted from an equality in a quotient, in contrast with the higher inductive types of chapter 68.
★★★ Define ℤ:=(ℕ×ℕ)/𝑅 with 𝑅(𝑎,𝑏)(𝑐,𝑑):=𝑎+𝑑≈ℕ𝑐+𝑏. Check 𝑅’s equivalence-relation obligations, and compute, by the rules of definition 79.11, definition 79.22, the weak-head normal form of 𝜋(𝗌𝗎𝖼(𝟢),𝟢)≈ℤ𝜋(𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢)),𝗌𝗎𝖼(𝟢)) down to a proposition built from ⊤.
★★☆ State and prove the universal property: for 𝐶:U𝑗, precomposition with 𝜋 is a bijection — up to ≈ — between functions 𝐴/𝑅→𝐶 and functions 𝑓:𝐴→𝐶 equipped with ∏𝑥:𝐴∏𝑦:𝐴𝑅𝑥𝑦→𝑓𝑥≈𝐶𝑓𝑦.
The two calculi solve the dependent-Σ equality problem differently: the 2007 calculus uses heterogeneous equality, while TTobs22 casts the first component before comparing the second.
The theory of Altenkirch, McBride and Swierstra is built over a core with ground types 𝟎,𝟏,𝟐, binders Π,Σ,𝖶, no universe hierarchy, and a separate syntactic class of propositions 𝑃::=⊥∣⊤∣𝑃∧𝑃∣∀𝑥:𝑆.𝑃, interpreted as proof-erasable sets. Its equality apparatus consists of four primitives: a type equality 𝑆=𝑇, a heterogeneous value equality relating inhabitants of two arbitrary types, a coercion, and a coherence:
Γ⊢𝑠:𝑆Γ⊢𝑡:𝑇
Γ⊢(𝑠:𝑆)=(𝑡:𝑇)𝗉𝗋𝗈𝗉
Het-Eq
Γ⊢𝑄:𝑆=𝑇Γ⊢𝑠:𝑆
Γ⊢𝑠[𝑄:𝑆=𝑇⟩:𝑇
Coe
Γ⊢𝑄:𝑆=𝑇Γ⊢𝑠:𝑆
Γ⊢{𝑠‖𝑄:𝑆=𝑇}:(𝑠:𝑆)=(𝑠[𝑄:𝑆=𝑇⟩:𝑇)
Coh
Both equalities compute by recursion on (pairs of) types: off-diagonal type equalities compute to ⊥, binders to the componentwise formulas, and value equality at Π to pointwise heterogeneous equality. Coercion at 𝖶 proceeds by structural recursion, coercing shapes forwards and child-positions backwards.
The 2007 equality compares (𝑠:𝑆) directly with (𝑡:𝑇) and requires a separate proof 𝑆=𝑇 when coercion is used. The 2022 equality first forms 𝑒:𝑆≈U𝑇, casts 𝑠 to 𝑇, and then compares 𝖼𝖺𝗌𝗍(𝑆,𝑇,𝑒,𝑠) with 𝑡. Thus Coh is primitive in the first calculus, whereas Cast-Refl gives propositional coherence in the second [AMS07, PT22].
Earlier homogeneous and heterogeneous variants, and the W-type encoding of inductive types that motivated them, are compared in [AMS07, PT22]. In each variant, type-directed equality identifies child functions pointwise, making the encoded natural-number induction principle derivable.
★★★ Translate the heterogeneous equality into TTobs: define (𝑠:𝑆)=(𝑡:𝑇):=∃(𝑒:𝑆≈U𝑖𝑇).𝖼𝖺𝗌𝗍(𝑆,𝑇,𝑒,𝑠)≈𝑇𝑡, construct the coercion and coherence operators for it, and show that at 𝑆≡𝑇 it is interprovable with 𝑠≈𝑆𝑡. Where is Cast-Refl indispensable?
We distinguish the 2022 core, its quotient extension, and observational CIC by the signatures in their theorem statements. The consistency clause for the 2022 core is relative to the source’s constructive set theory with induction–recursion and one Grothendieck universe; this is the metatheory in which its setoid universe and soundness proof are constructed.
Let TTobs22 be the calculus of Pujet and Tabareau (2022): two cumulative sort hierarchies, Π, ℕ, the strict propositional formers ∃,⊥,⊤, and the observational equality, 𝖼𝖺𝗌𝗍, and their reduction clauses. Then:
(Normalization) Every well-typed term of proof-relevant type has a weak-head normal form, computed by the oriented reading of the rules of definition 79.11, definition 79.17.
(Relative consistency) In the constructive set-theoretic metatheory named above there is no closed term of type ⊥.
(Canonicity) Every closed term of type ℕ is judgmentally equal to a numeral 𝗌𝗎𝖼𝑘(𝟢).
(Decidability) Conversion and type checking are decidable.
Proof. Corollary 3.6 gives normalization. Section 3.4 constructs sound and complete algorithmic conversion and the induced type-checking procedure. The setoid interpretation is proved sound in Theorem 3.10 in the metatheory named above, and Theorem 3.7 gives consistency. For canonicity, a closed weak-head normal form of type ℕ is a numeral or a neutral, and a closed neutral would contain a proof of ⊥, contradicting consistency. These are exactly the four claims imported from [PT22]. ◻
The four conclusions of theorem 79.26 are proved here only for TTobs22. Section 4.1 of [PT22] proposes quotient extensions and says that the fundamental lemma can be extended, but it leaves the universe equality, interpretation, and compatibility obligations to the reader and does not formalize them. Moreover, definition 79.22 separates relevant and irrelevant elimination, whereas the source presents a single eliminator.
Consequently this chapter does not infer normalization, consistency, canonicity, or decidable conversion for TTobs22+𝖰𝗎𝗈. Such a theorem requires three additional constructions: a quotient clause in the reducibility fundamental lemma; quotient equality and decoding in the setoid universe; and interpretation cases for Quo-E-Rel and Quo-E-Irr, with their computation and cast equations. None of the subsequent results depends on that open extension.
In the observational calculus of inductive constructions of [PLT25]—predicative CIC with a strict proposition sort, a general inductive scheme, irrelevant equality destructors, and constructor-commuting casts—algorithmic conversion and declarative conversion are decidable. Relative to ZFC with a countable hierarchy of Grothendieck universes, the calculus is consistent, and every closed inhabitant of ℕ is convertible to a canonical numeral.
Proof of Theorem 215.28 — Versioned observational-CIC comparison
Proof. Declarative and algorithmic conversion coincide, the conversion algorithm terminates, and the consistency argument rules out closed neutrals at ℕ; hence closed terms reduce to numerals [PLT25]. Section 6 explicitly constructs the model in ZFC with the stated countable Grothendieck-universe hierarchy; Theorem 6.5 is therefore a relative consistency result, not an assumption-free assertion about the object theory. ◻
Proof-irrelevant terms are neutral and carry no reduction behavior. Thus normalization alone permits a closed neutral 𝗋𝖾𝖼⊥(ℕ,𝑝); consistency rules out 𝑝:⊥, and only then does every closed normal inhabitant of ℕ have numeral form. At a 𝖲𝖯𝗋𝗈𝗉-type, conversion succeeds immediately by Irr and never inspects either proof.
Let CCobs be TTobs with 𝖲𝖯𝗋𝗈𝗉 made impredicative: ∏𝑥:𝐴𝑃:𝖲𝖯𝗋𝗈𝗉 for any type 𝐴 (of any level) with 𝑃:𝖲𝖯𝗋𝗈𝗉. All four properties of theorem 79.26 persist; its consistency clause is relative to the predicative Martin–Löf type theory, with the finite universe overhead, in which the cited normalization and model arguments are carried out.
Proof of Theorem 79.28 — Impredicative propositions
Proof. Theorem 3.2 identifies declarative and algorithmic conversion; the decision procedure is the remainder of §3.4. Theorem 4.1 gives normalization in Martin-Löf type theory with the stated finite universe overhead, while Theorems 5.3–5.5 give soundness, consistency, absence of closed neutrals, and hence canonicity [PT23]. The result is sharper than it may appear: Abel and Coquand showed [AC20] that definitional proof irrelevance with a UIP-style equality breaks the normalization algorithm of Coq’s impredicative Prop; the observational design circumvents the counterexample because irrelevant terms are never reduced (remark 79.27), and the normalization proof for CCobs is carried out in plain Martin-Löf type theory, showing that irrelevant impredicativity adds no computational content. ◻
Scaling definition 79.11 from ℕ to the full scheme of indexed inductive families (chapter 28, remark 28.36) is the content of the observational calculus of inductive constructions [PT24, PLT25]. Equality of two instances of an inductive former is there specified not by a closed formula but by irrelevant destructor axioms (e.g., from 𝗅𝗂𝗌𝗍𝐴≈U𝗅𝗂𝗌𝗍𝐴′ one extracts 𝐴≈U𝐴′), and 𝖼𝖺𝗌𝗍 commutes with constructors, recursively casting their arguments; indexed families additionally thread casts along their indices. The system is implemented in a fork of Rocq. A setoidal version of Swan’s identity types — an inductive equality with a 𝖩 computing judgmentally on 𝗋𝖾𝖿𝗅 — can also be added, making TTobs a proper extension of the intensional base of chapter 30[PT22].
★☆☆ Exhibit, in a context containing ℎ:⊥, a well-typed term of type ℕ that is a weak-head normal form but not a numeral. Conclude that theorem 79.26(3) genuinely depends on (2), and compare with the situation in the base, where the corresponding dependency runs in the opposite direction.
The displayed fragment derives observational UIP, function extensionality, and propositional computation for 𝖩, but it does not admit equality reflection or univalence. Its 2022 core retains normalization and decidable checking. These are the precise comparisons proved below; no claim about proof-theoretic strength is made.
Proof of Proposition 79.30 — No equality reflection
Proof. Take 𝑓:=𝜆𝑛.𝑛+𝟢 and 𝑔:=𝜆𝑛.𝑛, with the equality proof of construction 215.15. If 𝑓≡𝑔 held, then by completeness of the conversion algorithm of theorem 79.26(4) the 𝜂-expanded bodies 𝑛+𝟢 and 𝑛 would be algorithmically convertible in the context 𝑛:ℕ; but both are weak-head normal (𝑛+𝟢 is stuck elimination on the variable 𝑛), with distinct neutral heads, and the algorithm rejects. Hence adding reflection would change — in fact, by theorem 48.47, destroy — the conversion relation. ◻
Over the chapter 26–chapter 30 base, TTobs22 proves the observational versions of the three reflection consequences used in this chapter: UIP and function extensionality hold, and 𝖩 is derivable with a propositional computation rule.
The derived observational 𝖩 satisfies its reflexivity equation only up to ≈. Hofmann’s translation in theorem 35.39 requires the target eliminator’s specified computation law, so that theorem cannot be instantiated with this 𝖩.
Proof. (1) is Cast-Bool; note 𝟐≈U0𝟐≡⊤ by Obs-U-Atom, so 𝑒≡⋆ carries no information. (2) If 𝗌𝗐𝖺𝗉=𝖼𝖺𝗌𝗍(𝟐,𝟐,𝑒,−) up to ≈, then evaluating at 𝗍𝗍 gives an inhabitant of 𝗍𝗍≈𝟐𝖿𝖿, which computes to ⊥ by Obs-Bool; consistency of the exact observational-CIC extension (theorem 215.28) forbids it. (3) Let 𝑈 be the transcribed axiom. Applying 𝑈 to 𝗌𝗐𝖺𝗉 produces 𝑒:𝟐≈U0𝟐 whose cast is observationally equal to 𝗌𝗐𝖺𝗉. Evaluate that equality at 𝗍𝗍. Rule Cast-Bool reduces its left endpoint to 𝗍𝗍, whereas Boolean computation reduces the right endpoint to 𝖿𝖿; Obs-Bool then reduces the resulting observational equality to ⊥. This is an internal map 𝑈→⊥, independent of the external consistency assumption used in (2). ◻
Observational equality computes by recursion on type formers and places its proofs in 𝖲𝖯𝗋𝗈𝗉, so UIP holds. Cubical path equality instead retains proof-relevant higher structure and computes transport with interval and Kan operations. The two signatures contain different equality formers; neither is obtained from the other by adding a single computation rule.
★★☆ Show that in the Σ/𝟐 fragment the type 𝟐≈U0𝟐 has exactly one inhabitant up to judgmental equality, while in the univalent base (chapter 65) the corresponding identity type 𝟐=U0𝟐 is equivalent to 𝟐 by proposition 193.24. Where does the encode–decode computation used there break down observationally?
★★☆ Hedberg’s theorem (theorem 66.29) derives UIP from decidable equality. For arbitrary 𝐴,𝑡,𝑢, show directly from Irr that any two inhabitants of 𝑡≈𝐴𝑢 are judgmentally equal, without constructing a decision procedure. Then let 𝑃:𝖲𝖯𝗋𝗈𝗉0 and use Obs-Prop to show that a uniform decision procedure for 𝑃≈𝖲𝖯𝗋𝗈𝗉0⊤ would decide 𝑃. This isolates the difference between proof irrelevance and decidability without assuming that the ambient theory validates excluded middle.
★★☆ Derive cast through a dependent product, keeping the domain coercion contravariant and the codomain coercion dependent on it. Specialize the formula to a nondependent function and calculate both identity-type cases.
★★★Practical project.observational-equality-normalizer Implement in Agda or Kappa the Boolean, natural-number, product, and function clauses of observational equality and cast. Preserve the source and target type of every cast. Normalize casts along reflexivity and the displayed product equality, reject a covariant function-domain cast, and use a mutation that reverses the domain coercion to make that rejection test fail.
Observational type theory was announced in Altenkirch, McBride and Swierstra’s Observational Equality, Now![AMS07], of which the 2006 draft [AM06] is the precursor; the design distills Altenkirch’s earlier setoid model construction and Hofmann’s analysis of extensional concepts in intensional theories [Hof95], and the heterogeneous equality descends from McBride’s thesis [McB99]. The core theory TTobs22 and the metatheory of theorem 79.26 are due to Pujet and Tabareau [PT22]. The quotient rules of definition 79.22 adapt the proposal in their Section 4.1; the open metatheoretic obligations are recorded in remark 215.27. Its sorts of strict propositions follow Gilbert, Cockx, Sozeau and Tabareau’s 𝖲𝖯𝗋𝗈𝗉 (POPL 2019) [GCST19], as implemented in Agda and Rocq, and the mechanized normalization proof extends the Agda formalization of Abel, Öhman and Vezzosi (POPL 2018) [A"OV18]; see also Abel’s habilitation [Abe13] for the underlying technique, and chapter 49 for the base-theory instance. The core 2022 calculus contains Π, ℕ, and the propositional formers. The Σ- and 𝟐-rules displayed here are the 2007 componentwise definitions transposed to homogeneous 𝖼𝖺𝗌𝗍 form; their normalization support comes from the later observational-CIC extension rather than from an unstated general inductive scheme. The impredicative extension CCobs (theorem 79.28) is from [PT23], answering the normalization failure observed by Abel and Coquand for naive definitional UIP [AC20]; the extension to the inductive families of CIC (remark 79.29) is from [PT24] and its journal version with Leray [PLT25]. A cubical-syntax cousin, XTT (Sterling, Angiuli and Gratzer, 2019–2022), presents a UIP-theory with boundary-separated equality; Angiuli and Gratzer survey the observational family and its place in the history of equality in [AG26], §4.4, which this chapter follows in spirit. Swan’s identity types, mentioned in remark 79.29, and the two-level proposals combining an observational and a univalent hierarchy are discussed in [PT22], §1 and §4.3. For the contrast drawn in remark 79.33, see [CCHM18] and [ABC^+21] for the cubical resolutions.