No type introduced so far represents an impossible result. Such a type must have no constructors, yet it must still eliminate into any family once an impossible inhabitant is given. The empty type is the first instance of an inductive family: its constructors generate the elements, and its eliminator defines a section by giving one case for each constructor.
The empty type
The simplest inductive type has no constructors at all.
Extend the raw syntax of definition 26.1 by the nullary operator 𝟎 and the eliminator 𝗂𝗇𝖽𝟎(𝑥.𝐶;𝑎) of arity (1,0), binding 𝑥 only in the motive 𝐶. Capture-avoiding substitution in 𝐶 is the binder clause of definition 26.10.
Throughout this chapter, premises are compressed according to convention 26.14. Moreover:
If Γ,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾, we write 𝐵(𝑎) for the substitution instance 𝐵[𝑎/𝑥] when the displayed type judgment determines the binder 𝑥 uniquely; likewise 𝑏(𝑎) for 𝑏[𝑎/𝑥] when Γ,𝑥:𝐴⊢𝑏:𝐵.
Every eliminator carries the motive family displayed in its formation rule. Raw rule displays retain it. In derived terms we suppress the annotation only when the expected result type fixes it uniquely; the schematic token 𝗋𝖾𝖼𝟎 denotes 𝖺𝖻𝗈𝗋𝗍𝐶 only after that target 𝐶 has been fixed.
The printed abbreviation 𝜆𝑥.𝑏 suppresses the domain argument of the raw abstraction 𝜆(𝑥:𝐴).𝑏 only when typing fixes 𝐴 uniquely.
The empty type𝟎 is given by a formation rule and an elimination rule:
Γ𝖼𝗍𝗑
Γ⊢𝟎𝗍𝗒𝗉𝖾
-form
Γ,𝑥:𝟎⊢𝐶𝗍𝗒𝗉𝖾Γ⊢𝑎:𝟎
Γ⊢𝗂𝗇𝖽𝟎(𝑥.𝐶;𝑎):𝐶(𝑎)
-elim
There are no introduction rules, and consequently no computation rules: a computation rule describes the action of the eliminator on a constructor, and 𝟎 has none. Its congruence rule is the instance of the scheme in appendix A for the annotated eliminator.
For Γ⊢𝐶𝗍𝗒𝗉𝖾, instantiating 𝟎-elim at the weakened (constant) motive Γ,𝑥:𝟎⊢𝐶𝗍𝗒𝗉𝖾 and 𝜆-abstracting the scrutinee yields the recursor, the nondependent instance of the eliminator, 𝖺𝖻𝗈𝗋𝗍𝐶:=𝜆𝑎.𝗂𝗇𝖽𝟎(𝑥.𝐶;𝑎):𝟎→𝐶. The subscript is load-bearing raw information: empty elimination has no constructor from which its motive could be recovered. We omit it only when the expected result type fixes 𝐶 uniquely.
The judgment Γ⊢𝑎:𝟎 is derivable for many nonempty Γ: the variable rule alone gives 𝑥:𝟎⊢𝑥:𝟎. What the rules assert locally is not “there is no term of 𝟎,” but that every family treats 𝟎 as empty: any family over 𝟎 has a section, by 𝟎-elim. A claim that no closed term exists is instead a metatheoretic soundness statement, not an elimination rule.
For types 𝐴 and 𝐵 in context Γ there is a term Γ⊢𝜆𝑓.𝜆𝑔.𝜆𝑎.𝑔(𝑓𝑎):(𝐴→𝐵)→(¬𝐵→¬𝐴). Indeed, given 𝑓:𝐴→𝐵, 𝑔:¬𝐵, and 𝑎:𝐴 we have 𝑓𝑎:𝐵 and hence 𝑔(𝑓𝑎):𝟎, so the displayed 𝜆-term is well-typed by the rules of definition 27.2. No elimination out of 𝟎 is needed; ¬𝐴 is itself a Π-type.
★☆☆ Write out the definition of 𝗋𝖾𝖼𝟎 from definition 28.3 with the motive annotation of convention 28.1 restored, and display the instance of 𝟎-elim used, with all premises.
For Γ⊢𝐶𝗍𝗒𝗉𝖾, the recursor is the instance of 𝟐-elim at the weakened motive: 𝗋𝖾𝖼𝟐(𝑐𝑡,𝑐𝑓,𝑏):=𝗂𝗇𝖽𝟐(𝑐𝑡,𝑐𝑓,𝑏)(𝑐𝑡,𝑐𝑓:𝐶,𝑏:𝟐), of type 𝐶, with computation rules 𝗋𝖾𝖼𝟐(𝑐𝑡,𝑐𝑓,𝗍𝗍)≡𝑐𝑡 and 𝗋𝖾𝖼𝟐(𝑐𝑡,𝑐𝑓,𝖿𝖿)≡𝑐𝑓 inherited from 𝟐-comp1,2. We write 𝗂𝖿𝑏𝗍𝗁𝖾𝗇𝑐𝑡𝖾𝗅𝗌𝖾𝑐𝑓 for 𝗋𝖾𝖼𝟐(𝑐𝑡,𝑐𝑓,𝑏).
For a family Γ,𝑥:𝟐⊢𝐶𝗍𝗒𝗉𝖾, abstraction packages 𝟐-elim as 𝖻𝗈𝗈𝗅𝖨𝗇𝖽𝐶:𝐶(𝗍𝗍)→𝐶(𝖿𝖿)→∏𝑏:𝟐𝐶(𝑏), where 𝖻𝗈𝗈𝗅𝖨𝗇𝖽𝐶:=𝜆𝑐𝑡.𝜆𝑐𝑓.𝜆𝑏.𝗂𝗇𝖽𝟐(𝑥.𝐶;𝑐𝑡,𝑐𝑓,𝑏). Beta followed by Boolean computation gives 𝖻𝗈𝗈𝗅𝖨𝗇𝖽𝐶𝑐𝑡𝑐𝑓𝗍𝗍≡𝑐𝑡,𝖻𝗈𝗈𝗅𝖨𝗇𝖽𝐶𝑐𝑡𝑐𝑓𝖿𝖿≡𝑐𝑓. The two results inhabit the distinct fibers 𝐶(𝗍𝗍) and 𝐶(𝖿𝖿); the recursor of definition 28.8 is the constant-family case.
Put 𝗇𝖾𝗀:=𝜆𝑏.𝗋𝖾𝖼𝟐(𝖿𝖿,𝗍𝗍,𝑏). The body of 𝗇𝖾𝗀 is derived by the following tree. We write Var for the variable rule of definition 26.22; the first premise displays the constant motive required by 𝟐-elim.
𝑏:𝟐,𝑥:𝟐⊢𝟐𝗍𝗒𝗉𝖾
-form
𝑏:𝟐⊢𝖿𝖿:𝟐
-intro_2
𝑏:𝟐⊢𝗍𝗍:𝟐
-intro_1
𝑏:𝟐⊢𝑏:𝟐
Var
𝑏:𝟐⊢𝗋𝖾𝖼𝟐(𝖿𝖿,𝗍𝗍,𝑏):𝟐
-elim
One use of Π-intro now gives ⋅⊢𝗇𝖾𝗀:𝟐→𝟐. By 𝟐-comp1,2 and the 𝛽-rule of Π, 𝗇𝖾𝗀𝗍𝗍≡𝖿𝖿 and 𝗇𝖾𝗀𝖿𝖿≡𝗍𝗍.
Define 𝖺𝗇𝖽:=𝜆𝑎.𝜆𝑏.𝗋𝖾𝖼𝟐(𝑏,𝖿𝖿,𝑎) of type 𝟐→𝟐→𝟐. Then 𝖺𝗇𝖽𝗍𝗍𝑏≡𝑏 and 𝖺𝗇𝖽𝖿𝖿𝑏≡𝖿𝖿 for every 𝑏:𝟐 — in particular for a variable𝑏, where no case analysis on 𝑏 has been performed.
One may contemplate a uniqueness rule for 𝟐, asserting that a term depending on a boolean is determined by its values at the constructors:
Γ,𝑥:𝟐⊢𝐶𝗍𝗒𝗉𝖾Γ,𝑥:𝟐⊢𝑐:𝐶Γ⊢𝑏:𝟐
Γ⊢𝗂𝗇𝖽𝟐(𝑐(𝗍𝗍),𝑐(𝖿𝖿),𝑏)≡𝑐(𝑏):𝐶(𝑏)
-η
This rule is not part of the theory. More generally, none of the inductive types in this chapter has a judgmental 𝜂-rule. The local consequence is visible without a metatheorem: when 𝑏 is a variable, the term 𝗂𝗇𝖽𝟐(𝑐𝑡,𝑐𝑓,𝑏) is neutral with respect to the Boolean computation rules, because those two rules apply only to 𝗍𝗍 and 𝖿𝖿. Other equality rules may still identify its result—for example, every term of 𝟏 equals ⋆ by unit 𝜂—but no Boolean branch has fired. This contrasts with the primitive 𝜂-rules for Π, Σ, and 𝟏 in definition 27.2, definition 27.9, definition 27.14. Thus the design boundary is fixed by the selected judgmental equality, not by the informal description “inductive type.”
To separate 𝗍𝗍 from 𝖿𝖿 and rule out a closed inhabitant of 𝟎, an interpretation must assign one denotation to each raw expression, independently of its typing derivation. One might instead define the interpretation by induction on a typing derivation. That attempt fails at conversion: the same raw expression may arrive through different type equalities, so the induction produces a value only after a choice of derivation, while soundness needs one value shared by both routes. The domain annotation on raw abstraction nodes permits the stronger remedy: interpret raw syntax first, then prove that every derivation lands in that single partial interpretation.
Interpret raw contexts and official raw expressions before asking whether they are derivable. The recursion is partial: an ill-typed application, for example, need not denote. The kernel domain annotation on 𝜆(𝑥:𝐴).𝑏 from convention 27.1 is essential here. It fixes the set-theoretic domain of the function without consulting a typing derivation; the usual printed abbreviation 𝜆𝑥.𝑏 merely suppresses this raw argument. Put [[⋅]]={∗},[[Γ,𝑥:𝐴]]={(𝜌,𝑎)∣𝜌∈[[Γ]],𝑎∈[[𝐴]]Γ𝜌}. For a raw expression in a raw context, choose a representative of its alpha-class whose binders are fresh for the environment, and define [[𝑒]]Γ𝜌 by structural recursion on its raw binding tree. A variable denotes its coordinate of 𝜌. The binding clauses and the two dependent type formers are [[∏𝑥:𝐴𝐵]]Γ𝜌=∏𝑢∈[[𝐴]]Γ𝜌[[𝐵]]Γ,𝑥:𝐴(𝜌,𝑢),[[∑𝑥:𝐴𝐵]]Γ𝜌=∐𝑢∈[[𝐴]]Γ𝜌[[𝐵]]Γ,𝑥:𝐴(𝜌,𝑢),[[𝜆(𝑥:𝐴).𝑏]]Γ𝜌=(𝑢∈[[𝐴]]Γ𝜌↦[[𝑏]]Γ,𝑥:𝐴(𝜌,𝑢)). Application is evaluation, pairing is the dependent ordered pair, and the projections are its coordinate maps. Interpret 𝟏 by {∗} and ⋆ by ∗. Interpret 𝟎 by ∅ and its eliminator by the unique section out of the empty set. Interpret 𝟐 by {0,1}, with 𝗍𝗍 denoting 1 and 𝖿𝖿 denoting 0; Boolean elimination sends 1 to the true branch and 0 to the false branch. A context judgment is valid when its environment set is defined. A type judgment Γ⊢𝐴𝗍𝗒𝗉𝖾 is valid when 𝜌↦[[𝐴]]Γ𝜌 is a defined family of sets on [[Γ]]. A term judgment is valid when [[𝑎]]Γ𝜌∈[[𝐴]]Γ𝜌 for every environment. Type equality means equality of families, and term equality means pointwise equality of sections. Structural induction on raw binding trees shows that renaming a bound variable merely renames the corresponding environment coordinate. Hence the definition is independent of the representative and descends to the alpha-classes of convention 26.8.
The structural rules can remove a declaration followed by an arbitrary telescope, or insert one before such a telescope. The semantic equations must therefore have the same generality.
Let 𝐹 be any raw type or term expression in the indicated context.
Suppose that [[𝑎]]Γ𝜌 is defined at every environment 𝜌 under consideration. Define on raw environment tuples 𝑠𝑎,⋅(𝜌):=(𝜌,[[𝑎]]Γ𝜌),𝑠𝑎,Δ,𝑦:𝐷(𝛿,𝑑):=(𝑠𝑎,Δ(𝛿),𝑑). If 𝐹 is displayed in Γ,𝑥:𝐴,Δ and 𝑠𝑎,Δ(𝛿) is defined, then the two sides below are defined simultaneously and, when defined, [[𝐹[𝑎/𝑥]]]Γ,Δ[𝑎/𝑥]𝛿=[[𝐹]]Γ,𝑥:𝐴,Δ𝑠𝑎,Δ(𝛿).
Define the deletion map on raw tuples by 𝑤𝐴,⋅(𝜌,𝑎):=𝜌,𝑤𝐴,Δ,𝑦:𝐷(𝛿,𝑑):=(𝑤𝐴,Δ(𝛿),𝑑). If 𝐹 is displayed in Γ,Δ and 𝑤𝐴,Δ(𝛿) is defined, its weakening to Γ,𝑥:𝐴,Δ satisfies, whenever either side is defined, [[𝐹]]Γ,𝑥:𝐴,Δ𝛿=[[𝐹]]Γ,Δ𝑤𝐴,Δ(𝛿).
If Γ⊢𝑎:𝐴 is semantically valid, then 𝑠𝑎,Δ sends every valid environment of Γ,Δ[𝑎/𝑥] to one of Γ,𝑥:𝐴,Δ. If Γ⊢𝐴𝗍𝗒𝗉𝖾 is semantically valid, then 𝑤𝐴,Δ sends every valid environment of Γ,𝑥:𝐴,Δ to one of Γ,Δ.
Proof of Lemma 28.13 — Semantic substitution and weakening
Proof. For substitution, use structural induction on a representative of 𝐹 whose binders are fresh for 𝑎, with Δ universally quantified. A variable case replaces precisely the 𝑥-coordinate by [[𝑎]]𝜌, and a nonbinding operator follows from the induction hypotheses for its arguments. For a binder 𝑦 and a fixed 𝑑, the body induction hypothesis is [[𝐹]]Γ,𝑥:𝐴,Δ,𝑦:𝐷(𝑠𝑎,Δ(𝛿),𝑑)=[[𝐹[𝑎/𝑥]]]Γ,Δ[𝑎/𝑥],𝑦:𝐷[𝑎/𝑥](𝛿,𝑑). For the binder clause, the two functions have the same domain and the same value at every 𝑑, hence are equal as sets of ordered pairs. This includes the two dependent type formers.
For weakening, structural induction on a representative with a fresh binder 𝑦 gives, for every fixed 𝑑, [[𝐹]]Γ,𝑥:𝐴,Δ,𝑦:𝐷(𝛿,𝑑)=[[𝐹]]Γ,Δ,𝑦:𝐷(𝑤𝐴,Δ(𝛿),𝑑). The same equality of set-theoretic functions proves the binder clause. Finally, apply the appropriate equation to each successive declaration type of Δ; it shows that the unchanged last coordinate belongs to the required fiber. At the base of the substitution map, semantic validity of 𝑎:𝐴 puts the inserted coordinate in [[𝐴]]𝜌; at the base of weakening, semantic validity of 𝐴 makes that fiber a set. Induction along Δ proves the two final landing assertions. ◻
Proof. Proceed simultaneously over derivations of contexts and of the four expression judgments. The interpretation is a structural operation on the official raw subject; in particular, the domain of every abstraction is its raw 𝐴-annotation. Thus two occurrences of the common middle subject in a transitivity rule have literally the same interpretation. The context rules are the two defining clauses for [[⋅]] and [[Γ,𝑥:𝐴]], and each presupposition rule selects a valid premise. Rule Var is a coordinate projection. Rules Wk and Subst are (28.2) and (28.1). If 𝑎≡𝑎′:𝐴, the smaller-height equality premise gives equal sections; induction along Δ gives 𝑠𝑎,Δ=𝑠𝑎′,Δ and proves both equal-substitution rules. Equal declaration families give literally equal environment extensions, proving context conversion.
Reflexivity and symmetry are the corresponding laws of set-theoretic equality, and transitivity is set-theoretic transitivity on the one structurally interpreted middle expression. Congruence applies one defined set operation to equal arguments. If an equality premise interprets 𝐴 and 𝐵 as the same family, a section of [[𝐴]] is literally a section of [[𝐵]]; this proves conversion.
The added formers now follow from the clauses of definition 28.12. Pi-beta is evaluation and Pi-eta is equality of functions, with the weakened 𝑓 identified by (28.2). Sigma-beta is projection and Sigma-eta reconstructs an ordered pair. Unit-eta is equality in a singleton. The Void eliminator is the unique section out of the empty set; Boolean elimination evaluates at 1 or 0. This treats every primitive final-rule family in the stated fragment. ◻
Proof of Proposition 28.15 — A separating set interpretation
Proof. Soundness is lemma 73.15. A closed term of 𝟎 would denote an element of ∅, while the displayed closed Boolean equality would force 1=0. In context 𝑏:𝟐, the environment set is {0,1}; the variable denotes the identity function and the constructors denote the two constant functions. Pointwise equality separates the variable from each. ◻
A variable 𝑏:𝟐 is judgmentally equal to neither 𝗍𝗍 nor 𝖿𝖿, by proposition 28.15. Thus “two constructors” does not mean “two raw open terms”: variables and neutral eliminations remain. What 𝟐-elim says is instead that every family may define a value by treating the two constructors. The same proposition also proves that the closed judgment ⋅⊢𝗍𝗍≡𝖿𝖿:𝟐 is not derivable; no internal type expressing disequality is being used here.
★★☆ Define 𝗈𝗋, 𝗂𝗆𝗉𝗅𝗂𝖾𝗌, and 𝗑𝗈𝗋 of type 𝟐→𝟐→𝟐 using 𝗋𝖾𝖼𝟐. Orient the operations by the first argument and derive all six equations 𝗈𝗋𝗍𝗍𝑏≡𝗍𝗍,𝗈𝗋𝖿𝖿𝑏≡𝑏,𝗂𝗆𝗉𝗅𝗂𝖾𝗌𝗍𝗍𝑏≡𝑏,𝗂𝗆𝗉𝗅𝗂𝖾𝗌𝖿𝖿𝑏≡𝗍𝗍,𝗑𝗈𝗋𝗍𝗍𝑏≡𝗇𝖾𝗀𝑏,𝗑𝗈𝗋𝖿𝖿𝑏≡𝑏.
★★☆ For Γ,𝑥:𝟐⊢𝐶𝗍𝗒𝗉𝖾, 𝟐-elim constructs the function Γ⊢𝜆𝑐𝑡.𝜆𝑐𝑓.𝜆𝑏.𝗂𝗇𝖽𝟐(𝑥.𝐶;𝑐𝑡,𝑐𝑓,𝑏):𝐶(𝗍𝗍)→𝐶(𝖿𝖿)→∏𝑏:𝟐𝐶(𝑏). Derive this typing and its two computation equations, displaying the necessary weakening and Π-rules. Conversely, suppose a principle supplies, for every such 𝐶, a function of the displayed type with those two equations. Apply it successively to 𝑐𝑡, 𝑐𝑓, and 𝑏 to obtain a term of 𝐶(𝑏) and recover the two Boolean computations. Thus the two principles yield one another; no literal equality with the primitive eliminator subject is claimed.
The coproduct 𝐴+𝐵 is the disjoint union of two types; its constructors are unary, and its eliminator is case analysis with parameters.
Extend the raw syntax by 𝐴+𝐵, 𝗂𝗇𝗅(𝑎), 𝗂𝗇𝗋(𝑏), and 𝗂𝗇𝖽+(𝑧.𝐶;𝑓,𝑔;𝑠) of arities (0,0), (0), (0), and (1,0,0,0). Only the first eliminator argument binds, and it binds 𝑧 in 𝐶.
The left branch has type ∏𝑥:𝐴𝐶(𝗂𝗇𝗅(𝑥)), and the right branch has type ∏𝑦:𝐵𝐶(𝗂𝗇𝗋(𝑦)). Using ordinary functions for these branches keeps the coproduct eliminator itself nonbinding (cf. exercise 28.6).
For Γ⊢𝐶𝗍𝗒𝗉𝖾 and 𝑓:𝐴→𝐶, 𝑔:𝐵→𝐶, the recursor is the instance of +-elim at the weakened motive; we write [𝑓,𝑔]:=𝜆𝑠.𝗂𝗇𝖽+(𝑓,𝑔,𝑠):𝐴+𝐵→𝐶, so that [𝑓,𝑔](𝗂𝗇𝗅(𝑎))≡𝑓𝑎 and [𝑓,𝑔](𝗂𝗇𝗋(𝑏))≡𝑔𝑏.
The nondependent branch types do not suffice for a dependent motive. The tempting rule
Γ,𝑧:𝐴+𝐵⊢𝐶𝗍𝗒𝗉𝖾Γ⊢𝑓:𝐴→𝐶Γ⊢𝑔:𝐵→𝐶Γ⊢𝑠:𝐴+𝐵
Γ⊢𝗂𝗇𝖽+(𝑧.𝐶;𝑓,𝑔,𝑠):𝐶(𝑠)
failed
is not even well formed: 𝐶 is a type only in context Γ,𝑧:𝐴+𝐵. After substituting 𝗂𝗇𝗅(𝑎) for 𝑧, the left branch must produce 𝐶(𝗂𝗇𝗅(𝑎)), not an element of one fixed type.
Given Γ,𝑧:𝐴+𝐵⊢𝐶𝗍𝗒𝗉𝖾, package the eliminator as 𝖼𝖺𝗌𝖾𝐶:=𝜆𝑓.𝜆𝑔.𝜆𝑠.𝗂𝗇𝖽+(𝑧.𝐶;𝑓,𝑔;𝑠):(∏𝑥:𝐴𝐶(𝗂𝗇𝗅(𝑥)))→(∏𝑦:𝐵𝐶(𝗂𝗇𝗋(𝑦)))→∏𝑠:𝐴+𝐵𝐶(𝑠). For branch terms 𝑓 and 𝑔 of the displayed types, beta followed by the coproduct computations gives 𝖼𝖺𝗌𝖾𝐶𝑓𝑔(𝗂𝗇𝗅(𝑎))≡𝑓𝑎,𝖼𝖺𝗌𝖾𝐶𝑓𝑔(𝗂𝗇𝗋(𝑏))≡𝑔𝑏. The result fibers are 𝐶(𝗂𝗇𝗅(𝑎)) and 𝐶(𝗂𝗇𝗋(𝑏)), so this is a genuinely dependent instance even when those fibers happen to be judgmentally equal.
The term 𝗌𝗐𝖺𝗉:=[𝜆𝑎.𝗂𝗇𝗋(𝑎),𝜆𝑏.𝗂𝗇𝗅(𝑏)]:𝐴+𝐵→𝐵+𝐴 satisfies 𝗌𝗐𝖺𝗉(𝗂𝗇𝗅(𝑎))≡𝗂𝗇𝗋(𝑎) and 𝗌𝗐𝖺𝗉(𝗂𝗇𝗋(𝑏))≡𝗂𝗇𝗅(𝑏). Consequently 𝗌𝗐𝖺𝗉(𝗌𝗐𝖺𝗉(𝗂𝗇𝗅(𝑎)))≡𝗂𝗇𝗅(𝑎), and likewise on 𝗂𝗇𝗋. For a variable 𝑠:𝐴+𝐵, however, neither of the two coproduct computation rules applies to the outer case analysis. Thus the rules directly establish the displayed constructor calculations; no coproduct 𝜂-rule is assumed (remark 28.11).
★★☆ Define 𝟐′:=𝟏+𝟏, 𝗍𝗍′:=𝗂𝗇𝗅(⋆), 𝖿𝖿′:=𝗂𝗇𝗋(⋆). Derive the elimination and computation rules of definition 28.7 for 𝟐′, with the computation rules holding judgmentally. (Use 𝗂𝗇𝖽+ followed by the eliminator of 𝟏 in each branch, as derived in proposition 27.17.)
★★☆ Construct terms 𝛼:(𝐴+𝐵)+𝐶→𝐴+(𝐵+𝐶) and 𝛽:𝐴+(𝐵+𝐶)→(𝐴+𝐵)+𝐶 and verify by computation that 𝛽(𝛼𝑠)≡𝑠 for 𝑠 each of the three constructor forms 𝗂𝗇𝗅(𝗂𝗇𝗅(𝑎)), 𝗂𝗇𝗅(𝗂𝗇𝗋(𝑏)), 𝗂𝗇𝗋(𝑐).
★★☆ Construct terms 𝐹:(𝐴+𝐵→𝐶)→(𝐴→𝐶)×(𝐵→𝐶),𝐺:(𝐴→𝐶)×(𝐵→𝐶)→(𝐴+𝐵→𝐶), where × is the non-dependent Σ of remark 27.11. Verify the three constructor equations 𝐹(𝐺((𝑓,𝑔)))≡(𝑓,𝑔),𝐺(𝐹ℎ)(𝗂𝗇𝗅(𝑎))≡ℎ(𝗂𝗇𝗅(𝑎)),𝐺(𝐹ℎ)(𝗂𝗇𝗋(𝑏))≡ℎ(𝗂𝗇𝗋(𝑏)).
With ℕ a recursive constructor appears for the first time: the successor takes a natural number and returns one.
Extend the raw syntax by the nullary operators ℕ,𝟢, the unary operator 𝗌𝗎𝖼(𝑛), and 𝗂𝗇𝖽ℕ(𝑥.𝐶;𝑐0,𝑐𝑠;𝑚) of arity (1,0,0,0). The variable 𝑥 is bound only in the motive 𝐶.
The type ℕ of natural numbers is given by: for a family 𝑥:ℕ⊢𝐶, write 𝖲𝗍𝖾𝗉ℕ(𝐶):=∏𝑛:ℕ𝐶(𝑛)→𝐶(𝗌𝗎𝖼(𝑛)). To keep the two computation rules readable, abbreviate the raw eliminator by 𝐼𝐶(𝑐0,𝑐𝑠;𝑚):=𝗂𝗇𝖽ℕ(𝑥.𝐶;𝑐0,𝑐𝑠,𝑚).
Γ𝖼𝗍𝗑
Γ⊢ℕ𝗍𝗒𝗉𝖾
-form
Γ𝖼𝗍𝗑
Γ⊢𝟢:ℕ
-intro_1
Γ⊢𝑛:ℕ
Γ⊢𝗌𝗎𝖼(𝑛):ℕ
-intro_2
Γ,𝑥:ℕ⊢𝐶𝗍𝗒𝗉𝖾Γ⊢𝑐0:𝐶(𝟢)Γ⊢𝑐𝑠:𝖲𝗍𝖾𝗉ℕ(𝐶)Γ⊢𝑚:ℕ
Γ⊢𝐼𝐶(𝑐0,𝑐𝑠;𝑚):𝐶(𝑚)
-elim
Γ,𝑥:ℕ⊢𝐶𝗍𝗒𝗉𝖾Γ⊢𝑐0:𝐶(𝟢)Γ⊢𝑐𝑠:𝖲𝗍𝖾𝗉ℕ(𝐶)
Γ⊢𝐼𝐶(𝑐0,𝑐𝑠;𝟢)≡𝑐0:𝐶(𝟢)
-comp_1
Γ,𝑥:ℕ⊢𝐶𝗍𝗒𝗉𝖾Γ⊢𝑐0:𝐶(𝟢)Γ⊢𝑐𝑠:𝖲𝗍𝖾𝗉ℕ(𝐶)Γ⊢𝑚:ℕ
Γ⊢𝐼𝐶(𝑐0,𝑐𝑠;𝗌𝗎𝖼(𝑚))≡𝑐𝑠𝑚(𝐼𝐶(𝑐0,𝑐𝑠;𝑚)):𝐶(𝗌𝗎𝖼(𝑚))
-comp_2
The step 𝑐𝑠 receives the predecessor 𝑛 and the inductive hypothesis𝐶(𝑛), and produces 𝐶(𝗌𝗎𝖼(𝑛)). Thus ℕ-elim is the type-theoretic principle of mathematical induction.
Let Γ⊢𝐶𝗍𝗒𝗉𝖾, 𝑐0:𝐶, 𝑐𝑠:ℕ→𝐶→𝐶, and 𝑚:ℕ. The recursor𝗋𝖾𝖼ℕ(𝑐0,𝑐𝑠,𝑚):𝐶 is the instance of ℕ-elim at the weakened motive. Its computation rules read 𝗋𝖾𝖼ℕ(𝑐0,𝑐𝑠,𝟢)≡𝑐0,𝗋𝖾𝖼ℕ(𝑐0,𝑐𝑠,𝗌𝗎𝖼(𝑚))≡𝑐𝑠𝑚(𝗋𝖾𝖼ℕ(𝑐0,𝑐𝑠,𝑚)). This is exactly the primitive recursion scheme.
We construct 𝖺𝖽𝖽:ℕ→ℕ→ℕ satisfying the judgmental specification 𝖺𝖽𝖽𝑚𝟢≡𝑚,𝖺𝖽𝖽𝑚(𝗌𝗎𝖼(𝑛))≡𝗌𝗎𝖼(𝖺𝖽𝖽𝑚𝑛), and write 𝑚+𝑛 for 𝖺𝖽𝖽𝑚𝑛. Working in context 𝑚:ℕ, we recur on the second argument at the constant motive ℕ: the base case is 𝑚 itself, and the step ignores the predecessor and applies 𝗌𝗎𝖼 to the inductive hypothesis. That is, 𝖺𝖽𝖽:=𝜆𝑚.𝜆𝑛.𝗋𝖾𝖼ℕ(𝑚,𝜆𝑘.𝜆𝑟.𝗌𝗎𝖼(𝑟),𝑛). The specification holds by ℕ-comp1,2 and 𝛽-reduction for Π: for the second clause, 𝖺𝖽𝖽𝑚(𝗌𝗎𝖼(𝑛))≡(𝜆𝑘.𝜆𝑟.𝗌𝗎𝖼(𝑟))𝑛(𝖺𝖽𝖽𝑚𝑛)≡𝗌𝗎𝖼(𝖺𝖽𝖽𝑚𝑛).
Using addition in the step, define 𝗆𝗎𝗅:=𝜆𝑚.𝜆𝑛.𝗋𝖾𝖼ℕ(𝟢,𝜆𝑘.𝜆𝑟.𝑟+𝑚,𝑛):ℕ→ℕ→ℕ. The predecessor 𝑘 is unused and the recursive result 𝑟 has type ℕ. The two recursor computations therefore give 𝗆𝗎𝗅𝑚𝟢≡𝟢,𝗆𝗎𝗅𝑚(𝗌𝗎𝖼(𝑛))≡𝗆𝗎𝗅𝑚𝑛+𝑚.
Write ――𝑘 for the numeral obtained by applying 𝗌𝗎𝖼 exactly 𝑘 times to 𝟢. Then ――2+――2ℕ−𝑐𝑜𝑚𝑝2≡𝗌𝗎𝖼(――2+――1)ℕ−𝑐𝑜𝑚𝑝2≡𝗌𝗎𝖼(𝗌𝗎𝖼(――2+――0))ℕ−𝑐𝑜𝑚𝑝1≡𝗌𝗎𝖼(𝗌𝗎𝖼(――2))numeralnotation≡――4. This calculation uses only that both arguments are constructors.
The defining equations unfold along the second argument only. Thus 𝑚+𝟢≡𝑚 and 𝑚+𝗌𝗎𝖼(𝑛)≡𝗌𝗎𝖼(𝑚+𝑛) compute immediately, even when 𝑚 is a variable. By contrast, if 𝑛 is a variable, neither 𝟢+𝑛 nor 𝗌𝗎𝖼(𝑚)+𝑛 matches a recursor computation rule, so both are stuck. This is a statement about the displayed recursor’s root rules.
★☆☆ Assume Γ⊢𝐶𝗍𝗒𝗉𝖾, 𝑐0:𝐶, 𝑓:𝐶→𝐶, and 𝑛:ℕ. Define the iterator 𝗂𝗍𝖾𝗋𝑐0𝑓𝑛:𝐶 satisfying 𝗂𝗍𝖾𝗋𝑐0𝑓𝟢≡𝑐0 and 𝗂𝗍𝖾𝗋𝑐0𝑓(𝗌𝗎𝖼(𝑛))≡𝑓(𝗂𝗍𝖾𝗋𝑐0𝑓𝑛), as a special case of 𝗋𝖾𝖼ℕ. Then define 𝖺𝖽𝖽 using 𝗂𝗍𝖾𝗋 alone.
★★☆ Let Γ,𝑛:ℕ⊢𝐶𝗍𝗒𝗉𝖾. Use the dependent natural-number eliminator to construct 𝗂𝗇𝖽𝐶:𝐶(𝟢)→(∏𝑘:ℕ𝐶(𝑘)→𝐶(𝗌𝗎𝖼(𝑘)))→∏𝑛:ℕ𝐶(𝑛). Begin with 𝜆𝑐0.𝜆𝑐𝑠.𝜆𝑛.𝗂𝗇𝖽ℕ(𝑛.𝐶;𝑐0,𝜆𝑘.𝜆𝑟.𝑐𝑠𝑘𝑟;𝑛). Display the weakenings that place 𝑐0 and 𝑐𝑠 in the eliminator premises, and derive the judgmental equations at 𝟢 and 𝗌𝗎𝖼(𝑘). This is the binder form of dependent induction, not the constant-motive recursor.
★★★ Construct the Ackermann–Péter function 𝖺𝖼𝗄:ℕ→ℕ→ℕ with 𝖺𝖼𝗄𝟢𝑛≡𝗌𝗎𝖼(𝑛),𝖺𝖼𝗄(𝗌𝗎𝖼(𝑚))𝟢≡𝖺𝖼𝗄𝑚――1,𝖺𝖼𝗄(𝗌𝗎𝖼(𝑚))(𝗌𝗎𝖼(𝑛))≡𝖺𝖼𝗄𝑚(𝖺𝖼𝗄(𝗌𝗎𝖼(𝑚))𝑛), by recursion at the type ℕ→ℕ. Use the ℕ-recursor with constant motive ℕ→ℕ; unlike addition, its recursive results are themselves functions.
★★★ Construct 𝖾𝗊:ℕ→ℕ→𝟐 by recursion such that 𝖾𝗊――𝑚――𝑛 computes to 𝗍𝗍 if 𝑚=𝑛 and to 𝖿𝖿 otherwise, and verify 𝖾𝗊――2――2≡𝗍𝗍. Let the outer recursion return a function ℕ→𝟐; in the successor branch use the predecessor result to compare the two predecessors.
Let Γ be a well-formed context and let 𝐴, 𝐵, 𝐶 be types in Γ, with Γ,𝑥:ℕ⊢𝑃𝗍𝗒𝗉𝖾 a family over ℕ. The following types have inhabitants in context Γ, uniformly in the given data:
Proof. For the first clause, the term is 𝗋𝖾𝖼𝟎 (definition 28.3). For the second, 𝜆𝑓.𝜆𝑔.[𝑓,𝑔] (definition 28.18). For the third, 𝜆𝑐0.𝜆𝑐𝑠.𝜆𝑛.𝗂𝗇𝖽ℕ(𝑐0,𝑐𝑠,𝑛), using ℕ-elim under the three 𝜆-abstractions. Weakening places 𝑐0 and 𝑐𝑠 in the eliminator context; its zero and successor computations become the two induction equations after the three Π-𝛽 steps. ◻
Read 𝟏 as truth. Natural-number induction proves ∏𝑛:ℕ𝟏 from the base proof ⋆ and the step 𝜆𝑘.𝜆𝑢.⋆: 𝑝:=𝜆𝑛.𝗂𝗇𝖽ℕ(𝑛.𝟏;⋆,𝜆𝑘.𝜆𝑢.⋆;𝑛):∏𝑛:ℕ𝟏. The zero computation gives 𝑝𝟢≡⋆; the successor computation gives 𝑝(𝗌𝗎𝖼(𝑛))≡(𝜆𝑘.𝜆𝑢.⋆)𝑛(𝑝𝑛)≡⋆. Thus the proof term, its induction hypothesis, and both constructor calculations are visible rather than supplied only by the dictionary.
The reading is proof-relevant: a term of 𝐴+𝐵carries the tag of the case that holds, and a term of ∑𝑥:𝐴𝐵 carries an explicit witness. Consequently a term of 𝐴+¬𝐴 supplies more than an unlabeled truth value: it is a decision procedure, returning either an element of 𝐴 or a function 𝐴→𝟎. In this chapter, “𝐴 or 𝐵” therefore means the tagged data 𝐴+𝐵.
★☆☆ Construct a term of type ¬¬(𝐴+¬𝐴) for any type 𝐴; thus the classical case split is stable under double negation. (Given ℎ:¬(𝐴+¬𝐴), first obtain 𝑘:¬𝐴 by 𝑘𝑎:=ℎ(𝗂𝗇𝗅(𝑎)), and then apply ℎ to 𝗂𝗇𝗋(𝑘).)
Each inductive type so far required its own rules. W-types capture their common tree shape: a W-type is determined by a type of constructor symbols and a family of arities. Under explicit hypotheses on such an arity family, theorem 28.32 constructs the recursors of the encoded natural numbers, lists, and binary trees.
Extend the raw syntax by 𝖶𝑥:𝐴𝐵 of arity (0,1), 𝗌𝗎𝗉(𝑎,𝑓) of arity (0,0), and 𝗂𝗇𝖽𝖶(𝑤.𝐶;ℎ,𝑡) of arity (1,0,0). The W-former binds 𝑥 in 𝐵, and the eliminator binds 𝑤 only in 𝐶.
For Γ⊢𝐴𝗍𝗒𝗉𝖾 and Γ,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾, the type 𝖶𝑥:𝐴𝐵 of well-founded trees is given by the rules below; we abbreviate 𝑊:=𝖶𝑥:𝐴𝐵. For a family 𝑤:𝑊⊢𝐶, also write 𝖲𝗍𝖾𝗉𝖶(𝐶):=∏𝑎:𝐴∏𝛼:𝐵(𝑎)→𝑊(∏𝑦:𝐵(𝑎)𝐶(𝛼𝑦))→𝐶(𝗌𝗎𝗉(𝑎,𝛼)). For ℎ:𝖲𝗍𝖾𝗉𝖶(𝐶) and 𝑓:𝐵(𝑎)→𝑊, abbreviate the family of recursive results by 𝑅𝐶,ℎ(𝑓):=𝜆𝑦.𝗂𝗇𝖽𝖶(𝑤.𝐶;ℎ,𝑓𝑦).
Γ⊢𝐴𝗍𝗒𝗉𝖾Γ,𝑥:𝐴⊢𝐵𝗍𝗒𝗉𝖾
Γ⊢𝖶𝑥:𝐴𝐵𝗍𝗒𝗉𝖾
W-form
Γ⊢𝑎:𝐴Γ⊢𝑓:𝐵(𝑎)→𝑊
Γ⊢𝗌𝗎𝗉(𝑎,𝑓):𝑊
W-intro
Γ,𝑤:𝑊⊢𝐶𝗍𝗒𝗉𝖾Γ⊢ℎ:𝖲𝗍𝖾𝗉𝖶(𝐶)Γ⊢𝑡:𝑊
Γ⊢𝗂𝗇𝖽𝖶(𝑤.𝐶;ℎ,𝑡):𝐶(𝑡)
W-elim
Γ,𝑤:𝑊⊢𝐶𝗍𝗒𝗉𝖾Γ⊢ℎ:𝖲𝗍𝖾𝗉𝖶(𝐶)Γ⊢𝑎:𝐴Γ⊢𝑓:𝐵(𝑎)→𝑊
Γ⊢𝗂𝗇𝖽𝖶(𝑤.𝐶;ℎ,𝗌𝗎𝗉(𝑎,𝑓))≡ℎ𝑎𝑓(𝑅𝐶,ℎ(𝑓)):𝐶(𝗌𝗎𝗉(𝑎,𝑓))
W-comp
In W-elim, 𝐵(𝑎) means the substitution instance 𝐵[𝑎/𝑥] of the arity family fixed in the formation premise. A tree 𝗌𝗎𝗉(𝑎,𝑓) has root labeled by the symbol 𝑎 and a 𝐵(𝑎)-indexed family of immediate subtrees 𝑓; the step ℎ receives the label, the subtrees, and the inductive hypotheses for all subtrees.
Let 𝑊:=𝖶𝑥:𝐴𝐵 and suppose Γ,𝑤:𝑊⊢𝐶𝗍𝗒𝗉𝖾. Given the explicitly typed step ℎ:∏𝑎:𝐴∏𝛼:𝐵(𝑎)→𝑊(∏𝑦:𝐵(𝑎)𝐶(𝛼𝑦))→𝐶(𝗌𝗎𝗉(𝑎,𝛼)), W-elimination constructs the section 𝗂𝗇𝖽𝑊ℎ:=𝜆𝑡.𝗂𝗇𝖽𝖶(𝑤.𝐶;ℎ,𝑡):∏𝑡:𝑊𝐶(𝑡). Its value on a constructed tree exposes exactly the inductive hypotheses: 𝗂𝗇𝖽𝑊ℎ(𝗌𝗎𝗉(𝑎,𝑓))Π−𝛽≡𝗂𝗇𝖽𝖶(𝑤.𝐶;ℎ,𝗌𝗎𝗉(𝑎,𝑓))𝑊−𝑐𝑜𝑚𝑝≡ℎ𝑎𝑓(𝜆𝑦.𝗂𝗇𝖽𝖶(𝑤.𝐶;ℎ,𝑓𝑦))Π−𝛽≡ℎ𝑎𝑓(𝜆𝑦.𝗂𝗇𝖽𝑊ℎ(𝑓𝑦)):𝐶(𝗌𝗎𝗉(𝑎,𝑓)). Thus W-elimination constructs the whole dependent section; recursion below is its constant-family instance.
For Γ⊢𝐶𝗍𝗒𝗉𝖾, weaken 𝐶 to the constant family over 𝑊. The resulting step has type ℎ:∏𝑎:𝐴∏𝛼:𝐵(𝑎)→𝑊((𝐵(𝑎)→𝐶)→𝐶). Define 𝗋𝖾𝖼𝖶(ℎ,𝑡):=𝗂𝗇𝖽𝖶(ℎ,𝑡):𝐶. Its computation rule is 𝗋𝖾𝖼𝖶(ℎ,𝗌𝗎𝗉(𝑎,𝑓))≡ℎ𝑎𝑓(𝜆𝑦.𝗋𝖾𝖼𝖶(ℎ,𝑓𝑦)):𝐶. Here 𝑓:𝐵(𝑎)→𝑊 is the family of immediate subtrees, while the last argument sends each index 𝑦:𝐵(𝑎) to the recursively computed value of the subtree 𝑓𝑦. If 𝑡:𝑊 is a variable, 𝗋𝖾𝖼𝖶(ℎ,𝑡) is neutral: W-comp fires only when its target is displayed as 𝗌𝗎𝗉(𝑎,𝑓).
Let Γ⊢𝐴𝗍𝗒𝗉𝖾 and take the constant arity family 𝐵(𝑥):=𝟎. Then 𝐿𝐴:=𝖶𝑥:𝐴𝟎 has a leaf 𝗅𝖾𝖺𝖿𝑎:=𝗌𝗎𝗉(𝑎,𝗋𝖾𝖼𝟎) for every 𝑎:𝐴. Given 𝑘:𝐴→𝐶, the W-recursor with ℎ:=𝜆𝑎.𝜆𝛼.𝜆𝑞.𝑘𝑎 satisfies 𝗋𝖾𝖼𝖶(ℎ,𝗅𝖾𝖺𝖿𝑎)≡𝑘𝑎. The unused arguments 𝛼:𝟎→𝐿𝐴 and 𝑞:𝟎→𝐶 record that a leaf has no subtrees and hence no recursive results.
The more familiar encodings require arity families whose values depend on a Boolean or a coproduct. The fixed signature cannot construct such families, so the arity families in the theorem are explicit hypotheses.
For example, the tempting definition 𝐵𝑁(𝑏)?:=𝗋𝖾𝖼𝟐(𝟎,𝟏,𝑏) does not type-check. The Boolean recursor consumes two terms of one result type 𝐶, whereas 𝟎 and 𝟏 are types: Γ⊢𝟎𝗍𝗒𝗉𝖾Γ⊢𝟏𝗍𝗒𝗉𝖾Γ,𝑏:𝟐⊢𝗋𝖾𝖼𝟐(𝟎,𝟏,𝑏):𝐶failed has no possible term-typing premises for its two branches. With a universe closed under 𝟎 and 𝟏, one could derive Γ⊢𝟎:U𝑖 and Γ⊢𝟏:U𝑖 and eliminate 𝑏:𝟐 into U𝑖. Without that former, the arity families must remain explicit hypotheses.
Assume Γ⊢𝐴𝗍𝗒𝗉𝖾 and three arity families Γ,𝑏:𝟐⊢𝐵𝑁𝗍𝗒𝗉𝖾,Γ,𝑠:𝟏+𝐴⊢𝐵𝐿𝗍𝗒𝗉𝖾,Γ,𝑏:𝟐⊢𝐵𝑇𝗍𝗒𝗉𝖾, with the following equalities of types in the displayed contexts: Γ⊢𝐵𝑁(𝖿𝖿)≡𝟎𝗍𝗒𝗉𝖾,Γ⊢𝐵𝑁(𝗍𝗍)≡𝟏𝗍𝗒𝗉𝖾,Γ,𝑢:𝟏⊢𝐵𝐿(𝗂𝗇𝗅(𝑢))≡𝟎𝗍𝗒𝗉𝖾,Γ,𝑎:𝐴⊢𝐵𝐿(𝗂𝗇𝗋(𝑎))≡𝟏𝗍𝗒𝗉𝖾,Γ⊢𝐵𝑇(𝖿𝖿)≡𝟎𝗍𝗒𝗉𝖾,Γ⊢𝐵𝑇(𝗍𝗍)≡𝟐𝗍𝗒𝗉𝖾. No universe term is meant here: these are ordinary type families given as judgment-level hypotheses. Define 𝑁:=𝖶𝑥:𝟐𝐵𝑁(𝑥),𝐿:=𝖶𝑥:𝟏+𝐴𝐵𝐿(𝑥),𝑇:=𝖶𝑥:𝟐𝐵𝑇(𝑥). For every Γ⊢𝐶𝗍𝗒𝗉𝖾, the following recursion principles hold:
Put 𝑧:=𝗌𝗎𝗉(𝖿𝖿,𝗋𝖾𝖼𝟎) in Γ, and in Γ,𝑛:𝑁 put 𝑠𝑛:=𝗌𝗎𝗉(𝗍𝗍,𝜆𝑢.𝑛). For every 𝑐0:𝐶 and 𝑐𝑠:𝑁→𝐶→𝐶, there is 𝗋𝖾𝖼𝑁:𝑁→𝐶 with 𝗋𝖾𝖼𝑁𝑧≡𝑐0,𝗋𝖾𝖼𝑁(𝑠𝑛)≡𝑐𝑠𝑛(𝗋𝖾𝖼𝑁𝑛).
Put 𝗇𝗂𝗅:=𝗌𝗎𝗉(𝗂𝗇𝗅(⋆),𝗋𝖾𝖼𝟎) in Γ, and in Γ,𝑎:𝐴,ℓ:𝐿 put 𝖼𝗈𝗇𝗌𝑎ℓ:=𝗌𝗎𝗉(𝗂𝗇𝗋(𝑎),𝜆𝑢.ℓ). For every 𝑐𝑛:𝐶 and 𝑐𝑐:𝐴→𝐿→𝐶→𝐶, there is 𝗋𝖾𝖼𝐿:𝐿→𝐶 with 𝗋𝖾𝖼𝐿𝗇𝗂𝗅≡𝑐𝑛,𝗋𝖾𝖼𝐿(𝖼𝗈𝗇𝗌𝑎ℓ)≡𝑐𝑐𝑎ℓ(𝗋𝖾𝖼𝐿ℓ).
Put 𝗅𝖾𝖺𝖿:=𝗌𝗎𝗉(𝖿𝖿,𝗋𝖾𝖼𝟎) in Γ. In Γ,ℓ:𝑇,𝑟:𝑇, write 𝖻𝗋ℓ,𝑟:=𝜆𝑏.𝗋𝖾𝖼𝟐(ℓ,𝑟,𝑏), put 𝗇𝗈𝖽𝖾ℓ𝑟:=𝗌𝗎𝗉(𝗍𝗍,𝖻𝗋ℓ,𝑟). For every 𝑐𝑙:𝐶 and 𝑐𝑛:𝑇→𝑇→𝐶→𝐶→𝐶, there is 𝗋𝖾𝖼𝑇:𝑇→𝐶 with 𝗋𝖾𝖼𝑇𝗅𝖾𝖺𝖿≡𝑐𝑙,𝗋𝖾𝖼𝑇(𝗇𝗈𝖽𝖾ℓ𝑟)≡𝑐𝑛ℓ𝑟(𝗋𝖾𝖼𝑇ℓ)(𝗋𝖾𝖼𝑇𝑟).
Proof. First verify how the arity equalities type the displayed constructors. For example, 𝗋𝖾𝖼𝟎:𝟎→𝑁. Symmetry of 𝐵𝑁(𝖿𝖿)≡𝟎, followed by dependent-product congruence, gives 𝟎→𝑁≡𝐵𝑁(𝖿𝖿)→𝑁. Rule Conv therefore types 𝗋𝖾𝖼𝟎 at 𝐵𝑁(𝖿𝖿)→𝑁, and W-intro gives 𝑧=𝗌𝗎𝗉(𝖿𝖿,𝗋𝖾𝖼𝟎):𝑁.
For the list constructor, substitute the given 𝑎:𝐴 into the arity equality to obtain 𝐵𝐿(𝗂𝗇𝗋(𝑎))≡𝟏. Symmetry and function-type congruence give 𝟏→𝐿≡𝐵𝐿(𝗂𝗇𝗋(𝑎))→𝐿. Thus Conv types 𝜆𝑢.ℓ at 𝐵𝐿(𝗂𝗇𝗋(𝑎))→𝐿, and W-intro derives 𝖼𝗈𝗇𝗌𝑎ℓ:𝐿. The typings of 𝑠, 𝗇𝗂𝗅, 𝗅𝖾𝖺𝖿, and 𝗇𝗈𝖽𝖾 use the same conversion along their corresponding arity equalities. The same conversion changes 𝛼,𝑞 to functions with the familiar domain 𝟏 or 𝟐 before the applications at ⋆, 𝗍𝗍, and 𝖿𝖿 below. This is the mechanism by which the judgment-level arity hypotheses enter every construction.
For the first encoding, let 𝐶, 𝑐0, 𝑐𝑠 be given. Write 𝑀𝑁 for the family 𝑥:𝟐⊢(𝐵𝑁(𝑥)→𝑁)→(𝐵𝑁(𝑥)→𝐶)→𝐶, and note the judgmental equalities 𝑀𝑁(𝗍𝗍)≡(𝟏→𝑁)→(𝟏→𝐶)→𝐶 and 𝑀𝑁(𝖿𝖿)≡(𝟎→𝑁)→(𝟎→𝐶)→𝐶, by the assumed values of 𝐵𝑁 and congruence. Define 𝑒𝑡:=𝜆𝛼.𝜆𝑔.𝑐𝑠(𝛼⋆)(𝑔⋆):𝑀𝑁(𝗍𝗍),𝑒𝑓:=𝜆𝛼.𝜆𝑔.𝑐0:𝑀𝑁(𝖿𝖿), and ℎ:=𝜆𝑥.𝗂𝗇𝖽𝟐(𝑒𝑡,𝑒𝑓,𝑥), a term of the step type of definition 28.30 for the constant motive 𝐶. Put 𝗋𝖾𝖼𝑁:=𝜆𝑡.𝗋𝖾𝖼𝖶(ℎ,𝑡). Then 𝗋𝖾𝖼𝑁𝑧𝑊−𝑐𝑜𝑚𝑝≡ℎ𝖿𝖿𝗋𝖾𝖼𝟎(𝜆𝑦.𝗋𝖾𝖼𝑁(𝗋𝖾𝖼𝟎𝑦))𝟐−𝑐𝑜𝑚𝑝2≡𝑒𝑓𝗋𝖾𝖼𝟎(𝜆𝑦.𝗋𝖾𝖼𝑁(𝗋𝖾𝖼𝟎𝑦))Π−𝛽≡𝑐0, and 𝗋𝖾𝖼𝑁(𝑠𝑛)𝑊−𝑐𝑜𝑚𝑝≡ℎ𝗍𝗍(𝜆𝑦.𝑛)(𝜆𝑦.𝗋𝖾𝖼𝑁𝑛)𝟐−𝑐𝑜𝑚𝑝1≡𝑐𝑠((𝜆𝑦.𝑛)⋆)((𝜆𝑦.𝗋𝖾𝖼𝑁𝑛)⋆)Π−𝛽≡𝑐𝑠𝑛(𝗋𝖾𝖼𝑁𝑛). Both computation rules are judgmental, as claimed.
For the second encoding, put 𝑀𝐿(𝑣):=(𝐵𝐿(𝑣)→𝐿)→(𝐵𝐿(𝑣)→𝐶)→𝐶. The two coproduct branches of a step ∏𝑣:𝟏+𝐴𝑀𝐿(𝑣) are 𝑒nil:=𝜆𝑢.𝜆𝛼.𝜆𝑞.𝑐𝑛:∏𝑢:𝟏𝑀𝐿(𝗂𝗇𝗅(𝑢)),𝑒cons:=𝜆𝑎.𝜆𝛼.𝜆𝑞.𝑐𝑐𝑎(𝛼⋆)(𝑞⋆):∏𝑎:𝐴𝑀𝐿(𝗂𝗇𝗋(𝑎)). Let ℎ𝐿:=𝜆𝑣.𝗂𝗇𝖽+(𝑒nil,𝑒cons,𝑣) and 𝗋𝖾𝖼𝐿:=𝜆𝑡.𝗋𝖾𝖼𝖶(ℎ𝐿,𝑡). For 𝗇𝗂𝗅, W-computation, left coproduct computation, and beta give 𝗋𝖾𝖼𝐿𝗇𝗂𝗅𝑊−𝑐𝑜𝑚𝑝,+−𝑐𝑜𝑚𝑝1≡𝑒nil(⋆,𝗋𝖾𝖼𝟎,𝜆𝑦.𝗋𝖾𝖼𝐿(𝗋𝖾𝖼𝟎𝑦))Π−𝛽≡𝑐𝑛. For a cons cell the same three rules, now in the right branch, give 𝗋𝖾𝖼𝐿(𝖼𝗈𝗇𝗌𝑎ℓ)𝑊−𝑐𝑜𝑚𝑝,+−𝑐𝑜𝑚𝑝2≡𝑒cons𝑎(𝜆𝑢.ℓ)(𝜆𝑢.𝗋𝖾𝖼𝐿ℓ)Π−𝛽≡𝑐𝑐𝑎ℓ(𝗋𝖾𝖼𝐿ℓ).
For the third encoding, write 𝖻𝗋ℓ,𝑟:=𝜆𝑏.𝗋𝖾𝖼𝟐(ℓ,𝑟,𝑏):𝟐→𝑇, so that 𝖻𝗋ℓ,𝑟𝗍𝗍≡ℓ and 𝖻𝗋ℓ,𝑟𝖿𝖿≡𝑟. Put 𝑀𝑇(𝑏):=(𝐵𝑇(𝑏)→𝑇)→(𝐵𝑇(𝑏)→𝐶)→𝐶 and define 𝑒leaf:=𝜆𝛼.𝜆𝑞.𝑐𝑙:𝑀𝑇(𝖿𝖿),𝑒node:=𝜆𝛼.𝜆𝑞.𝑐𝑛(𝛼𝗍𝗍)(𝛼𝖿𝖿)(𝑞𝗍𝗍)(𝑞𝖿𝖿):𝑀𝑇(𝗍𝗍). Let ℎ𝑇:=𝜆𝑏.𝗂𝗇𝖽𝟐(𝑒node,𝑒leaf,𝑏) and 𝗋𝖾𝖼𝑇:=𝜆𝑡.𝗋𝖾𝖼𝖶(ℎ𝑇,𝑡). The false branch gives 𝗋𝖾𝖼𝑇𝗅𝖾𝖺𝖿≡𝑐𝑙. For a node, W-computation gives 𝑒node the subtree family 𝖻𝗋ℓ,𝑟 and the recursive-results family 𝜆𝑏.𝗋𝖾𝖼𝑇(𝖻𝗋ℓ,𝑟𝑏). Evaluating each at the two Boolean constructors therefore yields 𝗋𝖾𝖼𝑇(𝗇𝗈𝖽𝖾ℓ𝑟)𝑊−𝑐𝑜𝑚𝑝,𝟐−𝑐𝑜𝑚𝑝1,2,Π−𝛽≡𝑐𝑛ℓ𝑟(𝗋𝖾𝖼𝑇ℓ)(𝗋𝖾𝖼𝑇𝑟), by W-computation, Boolean computation, and beta. This proves all three recursion principles in the stated fragment. ◻
Use the first recursion principle of theorem 28.32 at result type 𝑁, base 𝑧, and step 𝜆𝑛.𝜆𝑟.𝑠(𝑠𝑟). The resulting 𝖽𝗈𝗎𝖻𝗅𝖾𝑁:𝑁→𝑁 satisfies 𝖽𝗈𝗎𝖻𝗅𝖾𝑁𝑧≡𝑧,𝖽𝗈𝗎𝖻𝗅𝖾𝑁(𝑠𝑛)≡𝑠(𝑠(𝖽𝗈𝗎𝖻𝗅𝖾𝑁𝑛)). The first equation is the encoded-nullary computation in the proof above; the second is W-computation at the unit-indexed subtree followed by Π-𝛽.
The word recursion in theorem 28.32 is deliberate. The W-type itself has the dependent eliminator of definition 28.28, but an encoded nullary constructor may be displayed as 𝗌𝗎𝗉(𝖿𝖿,𝛼) for an arbitrary 𝛼:𝟎→𝑁, not only as 𝑧=𝗌𝗎𝗉(𝖿𝖿,𝗋𝖾𝖼𝟎). The constant motives above ignore this difference, so their computation equations are judgmental. A Nat-style dependent motive would have to compare its fibers at those two displayed trees. No such comparison rule is part of the Nat induction data established here, and the theorem makes no claim about dependent elimination for this encoding.
★☆☆ Use clause 3 of theorem 28.32 to define 𝗅𝖾𝖺𝗏𝖾𝗌:𝑇→ℕ with 𝗅𝖾𝖺𝗏𝖾𝗌𝗅𝖾𝖺𝖿≡――1,𝗅𝖾𝖺𝗏𝖾𝗌(𝗇𝗈𝖽𝖾ℓ𝑟)≡𝗅𝖾𝖺𝗏𝖾𝗌ℓ+𝗅𝖾𝖺𝗏𝖾𝗌𝑟. State the four arguments passed to the node step before writing the term.
★★☆ Suppose Γ⊢𝑘:∏𝑥:𝐴𝐵, i.e. every arity is pointed. Construct a term of type ¬𝖶𝑥:𝐴𝐵. (Use W-elim with the constant motive 𝟎: the inductive hypothesis at 𝑘𝑥 yields the contradiction.)
The syntax and rules for coproducts, natural numbers, and W-types are now in scope, so their semantic clauses can be checked against the displays they interpret.
Extend definition 28.12 as follows. A coproduct is the tagged union {0}×[[𝐴]]Γ𝜌∪{1}×[[𝐵]]Γ𝜌, with the two injections inserting their tags and elimination selecting the tagged branch. Interpret ℕ by the metatheoretic natural numbers, with zero, successor, and dependent recursion.
For 𝖶𝑥:𝐴𝐵 at 𝜌, put 𝐴𝜌:=[[𝐴]]Γ𝜌 and 𝐵𝜌,𝑎:=[[𝐵]]Γ,𝑥:𝐴(𝜌,𝑎). Choose an infinite regular cardinal 𝜅 strictly larger than every |𝐵𝜌,𝑎|. Define an increasing family by transfinite recursion: 𝑊0𝜌=∅,𝑊𝛼+1𝜌=∐𝑎∈𝐴𝜌(𝐵𝜌,𝑎→𝑊𝛼𝜌),𝑊𝜆𝜌=⋃𝛼<𝜆𝑊𝛼𝜌(𝜆limit). where an element of the successor stage is written 𝗌𝗎𝗉(𝑎,𝑓). Set 𝑊𝜌=⋃𝛼<𝜅𝑊𝛼𝜌. If 𝑓:𝐵𝜌,𝑎→𝑊𝜌, regularity of 𝜅 bounds the ranks of all 𝑓(𝑦) below one 𝛼<𝜅; hence 𝗌𝗎𝗉(𝑎,𝑓)∈𝑊𝜌. Conversely, induction on 𝛼 shows that every set closed under 𝗌𝗎𝗉 contains 𝑊𝛼𝜌, so 𝑊𝜌 is the least closed set.
Declare 𝑓(𝑦)◃𝗌𝗎𝗉(𝑎,𝑓). The least stage containing 𝑓(𝑦) is smaller than the least stage containing 𝗌𝗎𝗉(𝑎,𝑓), so ◃ is well founded. The W-eliminator is well-founded recursion on this relation; at 𝗌𝗎𝗉(𝑎,𝑓) it applies the step to 𝑎, 𝑓, and 𝑦↦𝗋𝖾𝖼(𝑓(𝑦)).
Proof of Lemma 28.14 — Soundness of the partial interpretation
Proof. The cases through booleans are lemma 73.15. Structural induction on raw expressions adds the three clauses of lemma 28.13: tagged union and ordinary recursion commute with reindexing, while the transfinite construction of 𝑊𝜌 is determined only by the reindexed families 𝐴𝜌 and 𝐵𝜌,𝑎.
It remains to inspect the new final rules. Coproduct introduction inserts a tag, elimination selects that tag, and the two computation rules are literal case equations. The natural-number rules are the formation, zero, successor, and dependent-recursion clauses of ℕ. W-formation uses the set 𝑊𝜌 just constructed; W-introduction is closure under 𝗌𝗎𝗉; and the elimination and computation rules are the defining equations of well-founded recursion on ◃. Congruence applies the same set operation to equal arguments. These are all new rule families. ◻
ZFC proves that the theory through W-types has no closed term of 𝟎 and does not derive 𝗍𝗍≡𝖿𝖿:𝟐. Hence consistency of ZFC implies consistency of this displayed type theory.
Proof of Corollary 73.41 — Relative consistency of the inductive fragment
Proof. By lemma 28.14, a closed term of 𝟎 would denote an element of ∅, and the Boolean equation would force 1=0. ◻
The general pattern
Every type of this chapter is an instance of one schema. For each constructor 𝑐𝑖, the eliminator has one branch whose arguments are the constructor’s nonrecursive data, recursive subtrees, and an induction hypothesis for each subtree. The following schema covers the nonindexed signatures used in this chapter and keeps each induction hypothesis visible. Recursive occurrences are restricted to outputs of the displayed arity functions. It does not cover indexed families such as identity types or vectors, mutual blocks, nested recursive occurrences such as 𝖫𝗂𝗌𝗍(𝑋), or induction–recursion such as a Tarski universe. Those require strictly stronger declaration disciplines than the polynomial signature defined here.
A polynomial inductive signature specifies finitely many constructors by nonrecursive parameter telescopes and recursive arity telescopes. For each constructor index 𝑖, choose:
a telescope Δ𝑖 of non-recursive parameters, whose types are formed over Γ and earlier entries of Δ𝑖; and
finitely many recursive arity telescopesΘ𝑖1,…,Θ𝑖𝑟𝑖, formed over Γ,Δ𝑖.
None of these telescope types mentions the fresh symbol 𝑋. If ⃗𝑢:Δ𝑖 and ⃗𝑧:Θ𝑖𝑗, the 𝑖th constructor has the scheme 𝖼𝑖:∏⃗𝑢:Δ𝑖∏𝑓1:∏⃗𝑧:Θ𝑖1𝑋⋯∏𝑓𝑟𝑖:∏⃗𝑧:Θ𝑖𝑟𝑖𝑋𝑋.(𝖢𝑖) The dots denote the displayed finite telescope in increasing order; they are not a function product over a finite index type. The formation judgment is Γ⊢𝖨𝗇𝖽𝗍𝗒𝗉𝖾. The primitive introduction rule says that well-typed arguments ⃗𝑢:Δ𝑖,𝑓𝑗:∏⃗𝑧:Θ𝑖𝑗𝖨𝗇𝖽(1≤𝑗≤𝑟𝑖) produce 𝖼𝑖(⃗𝑢,𝑓1,…,𝑓𝑟𝑖):𝖨𝗇𝖽. Display (𝖢𝑖) is the Pi-coded telescope of those premises, not a change from the primitive operator syntax. The product over an empty arity telescope is 𝑋 itself, so direct recursive arguments are included.
For a motive Γ,𝑤:𝖨𝗇𝖽⊢𝐶𝗍𝗒𝗉𝖾, the corresponding case has one inductive-hypothesis family immediately after each recursive argument: write 𝐹𝑖𝑗:=∏⃗𝑧:Θ𝑖𝑗𝖨𝗇𝖽,𝑄𝑖𝑗(𝑓):=∏⃗𝑧:Θ𝑖𝑗𝐶(𝑓(⃗𝑧)). Then its case telescope is ∏⃗𝑢:Δ𝑖∏𝑓1:𝐹𝑖1∏𝑞1:𝑄𝑖1(𝑓1)⋯∏𝑓𝑟𝑖:𝐹𝑖𝑟𝑖∏𝑞𝑟𝑖:𝑄𝑖𝑟𝑖(𝑓𝑟𝑖)𝐶(𝖼𝑖(⃗𝑢,𝑓1,…,𝑓𝑟𝑖)).(𝖤𝑖) If 𝑑𝑖 has this case type for every 𝑖 and 𝑡:𝖨𝗇𝖽, the full elimination judgment is Γ⊢𝗂𝗇𝖽(𝑤.𝐶;𝑑1,…,𝑑𝑘;𝑡):𝐶(𝑡). Its 𝑖th computation rule is obtained by writing 𝐼𝑗(𝑓𝑗):=𝜆⃗𝑧.𝗂𝗇𝖽(𝑤.𝐶;⃗𝑑;𝑓𝑗(⃗𝑧)). It is the equation 𝗂𝗇𝖽(𝑤.𝐶;⃗𝑑;𝖼𝑖(⃗𝑢,⃗𝑓))≡𝑑𝑖(⃗𝑢,𝑓1,𝐼1(𝑓1),…,𝑓𝑟𝑖,𝐼𝑟𝑖(𝑓𝑟𝑖)):𝐶(𝖼𝑖(⃗𝑢,⃗𝑓)). Thus the 𝑖th case is applied to ⃗𝑢, to every 𝑓𝑗, and to the recursively computed family for every 𝑗. In (𝖢𝑖), the symbol 𝑋 occurs only as the final result of an arity product. This restriction is strict positivity: no constructor argument places 𝑋 to the left of an arrow.
Equivalently for this polynomial fragment, the admissible constructor result types are generated by the following predicate, decidable by structural recursion on the finite type expression: 𝖲𝖯𝑋(𝑋)𝑋∉FV(𝐶)𝖲𝖯𝑋(𝑇)𝖲𝖯𝑋(∏𝑧:𝐶𝑇)𝖠𝗋𝑋(𝐹)𝖲𝖯𝑋(𝑇)𝑓∉FV(𝑇)𝖲𝖯𝑋(∏𝑓:𝐹𝑇), where recursive arities are generated separately by 𝖠𝗋𝑋(𝑋)𝑋∉FV(𝐶)𝖠𝗋𝑋(𝑇)𝖠𝗋𝑋(∏𝑧:𝐶𝑇). Thus the last 𝖲𝖯 clause admits a recursive-argument domain such as 𝑋 or Θ→𝑋, while 𝖠𝗋 rejects 𝑋→𝑋: the recursive type may occur only as the arity’s final result. The telescope display above is a normal form for these clauses after permuting independent Π-binders. This checker still rejects nested occurrences under a previously declared positive constructor. A larger checker may admit them by recording, for each parameter of that earlier constructor, whether the parameter occurs only positively, only negatively, or in both polarities.
The ordering in (𝖤𝑖) is interleaved only to keep each recursive argument adjacent to its induction hypothesis. Permuting independent Π-binders gives the grouped convention used by many implementations: all recursive arguments first, then all induction hypotheses.
When the universe hierarchy is installed, the schema has an accompanying closure obligation: if every type in Δ𝑖 and Θ𝑖𝑗 is coded at the same external level, then the generated 𝖨𝗇𝖽 is coded at that level. This is a rule schema, not a consequence of formation in 𝗍𝗒𝗉𝖾; large or indexed inductives require additional level constraints.
For 𝟢, take Δ0 empty and 𝑟0=0. Its case is 𝑐0:𝐶(𝟢). For 𝗌𝗎𝖼, again take Δ𝑠 empty, but take one recursive argument with empty arity telescope. Formula (𝖢𝑖) becomes 𝗌𝗎𝖼:ℕ→ℕ, and (𝖤𝑖) becomes 𝑐𝑠:∏𝑛:ℕ(𝐶(𝑛)→𝐶(𝗌𝗎𝖼(𝑛))). The generated computation equations are exactly 𝗂𝗇𝖽ℕ(𝑐0,𝑐𝑠,𝟢)≡𝑐0,𝗂𝗇𝖽ℕ(𝑐0,𝑐𝑠,𝗌𝗎𝖼(𝑛))≡𝑐𝑠𝑛(𝗂𝗇𝖽ℕ(𝑐0,𝑐𝑠,𝑛)). Thus the recursive argument 𝑛 generates the inductive hypothesis 𝐶(𝑛)—the characteristic extra premise of induction.
The remaining rule displays fit the same template. 𝟎 has no constructors; 𝟐 has two constructors with empty Δ and no recursive arguments; the two coproduct constructors have parameter telescopes 𝑎:𝐴 and 𝑏:𝐵; and W has one constructor with parameter 𝑎:𝐴 and one recursive arity telescope 𝑦:𝐵(𝑎). These give precisely definition 28.2, definition 28.7, definition 28.17, definition 28.28.
Every polynomial signature admitted by definition 28.34 extends the set interpretation by a set [[𝖨𝗇𝖽]]Γ𝜌 validating its formation, introduction, elimination, and computation rules.
Proof of Proposition 73.44 — Set soundness of the polynomial schema
Proof. Fix an environment 𝜌. Interpreting a nonrecursive parameter telescope gives the set [[Δ𝑖]]𝜌 of its assignments. For an arity telescope define its factor recursively, retaining the curried dependent product represented by the syntax: 𝑅𝜌,⃗𝑢()(𝑋):=𝑋,𝑅𝜌,⃗𝑢(𝑧:𝐶,Θ)(𝑋):=∏𝑧∈[[𝐶]]𝜌,⃗𝑢𝑅𝜌,⃗𝑢,𝑧Θ(𝑋). The constructors therefore determine the polynomial operator 𝐹𝜌(𝑋)=∐𝑖∐⃗𝑢∈[[Δ𝑖]]𝜌𝑟𝑖∏𝑗=1𝑅𝜌,⃗𝑢Θ𝑖𝑗(𝑋). In particular the empty telescope denotes 𝑋 itself, while (𝑧:𝐶,𝑤:𝐷(𝑧)) denotes ∏𝑧∈[[𝐶]]∏𝑤∈[[𝐷(𝑧)]]𝑋 on the nose, rather than the merely isomorphic set of functions from uncurried assignment tuples. Choose an infinite regular cardinal larger than every domain set occurring in the displayed arity telescopes and iterate 𝐹𝜌 from ∅ exactly as in definition 73.39. Regularity makes the union stage closed under 𝐹𝜌, and transfinite induction makes it the least closed set. The immediate-subtree relation decreases the construction rank, so it is well founded. Well-founded recursion supplies the eliminator and gives the displayed computation equation at each constructor. Reindexing commutes with the polynomial operator because every Δ𝑖 and Θ𝑖𝑗 is a telescope of previously interpreted types. The derivation-induction proof of lemma 28.14 therefore gains precisely the advertised rule cases. ◻
The requirement that the recursive type occur only in the codomains displayed in definition 28.34 is the strict-positivity condition. It is a genuine restriction. Suppose we admitted a type 𝐷 with the single constructor 𝖿𝗈𝗅𝖽:(𝐷→𝟎)→𝐷(𝑋occursnegatively), together with the case-analysis recursor the schema would prescribe: for every 𝐶 and 𝑒:(𝐷→𝟎)→𝐶 a map 𝗋𝖾𝖼𝐷(𝑒):𝐷→𝐶 with 𝗋𝖾𝖼𝐷(𝑒,𝖿𝗈𝗅𝖽(𝑢))≡𝑒𝑢. Taking 𝐶:=𝐷→𝟎 and 𝑒:=𝜆𝑢.𝑢 yields 𝗎𝗇𝖿𝗈𝗅𝖽:𝐷→(𝐷→𝟎) with 𝗎𝗇𝖿𝗈𝗅𝖽(𝖿𝗈𝗅𝖽(𝑢))≡𝑢. Now set 𝛿:=𝜆𝑑.𝗎𝗇𝖿𝗈𝗅𝖽𝑑𝑑:𝐷→𝟎,𝜔:=𝛿(𝖿𝗈𝗅𝖽(𝛿)):𝟎. The typing is worth checking before the reduction. In context 𝑑:𝐷, 𝗎𝗇𝖿𝗈𝗅𝖽𝑑:𝐷→𝟎, hence 𝗎𝗇𝖿𝗈𝗅𝖽𝑑𝑑:𝟎; abstraction gives 𝛿:𝐷→𝟎, so 𝖿𝗈𝗅𝖽(𝛿):𝐷 and finally 𝜔:𝟎 in the empty context. Orient beta and recursor computation from left to right, allow either rule to act in any subterm position, and write 𝑡⟶𝑡′ for one such contextual step. A normal form has no outgoing step; a term is strongly normalizing when no infinite sequence of steps starts from it. Put 𝑑0:=𝖿𝗈𝗅𝖽(𝛿). Beta and the bad recursor equation give the nonempty cycle 𝜔⟶𝗎𝗇𝖿𝗈𝗅𝖽𝑑0𝑑0⟶((𝜆𝑢.𝑢)𝛿)𝑑0⟶𝛿𝑑0=𝜔. Repeating it produces an infinite reduction sequence, while the typed term 𝜔 makes the theory extended by 𝐷 syntactically inconsistent: it derives a closed term of 𝟎. It also shows that the separating set interpretation cannot be extended to this 𝐷. The strict-positivity condition excludes this simultaneous failure of consistency and normalization; it is not a bureaucratic side condition.
The same schema makes the indexed boundary visible. A vector family would need constructor conclusions 𝗏𝗇𝗂𝗅:𝖵𝖾𝖼(𝐴,𝟢),𝗏𝖼𝗈𝗇𝗌:∏𝑛:ℕ𝐴→𝖵𝖾𝖼(𝐴,𝑛)→𝖵𝖾𝖼(𝐴,𝗌𝗎𝖼(𝑛)). But every constructor generated by (𝖢𝑖) must end in the one fixed type 𝖨𝗇𝖽: (𝖢𝑖)requiresconclusion𝖨𝗇𝖽𝗏𝖼𝗈𝗇𝗌(𝑛,𝑎,𝑣):𝖨𝗇𝖽(𝗌𝗎𝖼𝑛)failed. The application 𝖨𝗇𝖽(𝗌𝗎𝖼𝑛) is not even formed, since 𝖨𝗇𝖽 is a type rather than a family. Replacing it by the single type ∏𝑛:ℕ𝖵𝖾𝖼(𝐴,𝑛) would make a constructor return an entire family, not the required fiber. Indexed constructor conclusions are therefore genuinely outside this unindexed schema.
★★☆ Instantiate definition 28.34 for primitive lists over 𝐴 (constructors 𝗇𝗂𝗅:𝖫𝗂𝗌𝗍(𝐴) and 𝖼𝗈𝗇𝗌:𝐴→𝖫𝗂𝗌𝗍(𝐴)→𝖫𝗂𝗌𝗍(𝐴)): display all formation, introduction, elimination, and computation rules in the format of definition 28.21. For the cons case, the generated branch type must contain, in order, 𝑎:𝐴, ℓ:𝖫𝗂𝗌𝗍(𝐴), and the inductive hypothesis for ℓ.
★★★ Carry out the computation of remark 28.36 in detail: exhibit the typing derivations of 𝛿 and 𝜔 in the extended theory. Exhibit the nonempty reduction cycle displayed there and conclude that an infinite reduction sequence starts at 𝜔, so 𝜔 is not strongly normalizing. Finally show that no reduct on this cycle is a normal form. (Intermediate one-step reducts need not be syntactically 𝜔.)
The polynomial schema above and W-types both organize recursive data as a constructor label together with immediate subtrees. Turning that observation into an initial-algebra theorem requires more equality than the intensional core supplies. The distinction matters already for an encoded nullary constructor: remark 28.33 exhibited many terms 𝛼:𝟎→𝑁 that the core cannot identify with 𝗋𝖾𝖼𝟎. We therefore reconstruct the external theorem in a separate source calculus and state its equality assumptions before using them.
Write TD for extensional Martin-Löf type theory with dependent products and sums, empty and unit types 𝑁0,𝑁1, binary sums and products, W-types, identity types, and a first Russell universe U0 closed under these formers. Thus a family over a closed type 𝐴 may be given by a term 𝐵:𝐴→U0, and elimination into U0 is available.
Identity types have reflexivity and 𝐽, and the calculus validates equality reflection: Γ⊢𝑝:𝖨𝖽𝐴(𝑎,𝑏)Γ⊢𝑎≡𝑏:𝐴Eq−reflect. Identity proofs are unique. Function extensionality is available in the typed form 𝖿𝗎𝗇𝖾𝗑𝗍𝑓,𝑔:(∏𝑥:𝐴𝖨𝖽𝐵(𝑥)(𝑓𝑥,𝑔𝑥))→𝖨𝖽∏𝑥:𝐴𝐵(𝑥)(𝑓,𝑔). The usual uniqueness laws for 𝑁0, 𝑁1, sums, products, and W-recursion are also available. In particular, for maps 𝑦:𝑁0→𝐶 and 𝑦:𝑁1→𝐶, respectively, there are terms 𝜖0𝑦:𝖨𝖽𝑁0→𝐶(𝑦,𝜆(𝑥:𝑁0).𝗋𝖾𝖼𝟎𝑥),𝜖1𝑦:𝖨𝖽𝑁1→𝐶(𝑦,𝜆(𝑥:𝑁1).𝑦⋆). Functions out of a coproduct are equal when their two restrictions are equal. The W-equation and W-induction rule are those of definition 28.28, read in this extensional equality. Unadorned equality in this starred section denotes the judgmental equality obtained by reflection. Objects below are closed types of TD, and arrows are functions modulo that equality.
The two displayed uniqueness equations are not derived in the intensional theory of this chapter. They are among the extensional equalities used in Dybjer’s normalization of strictly positive operators. Naming TD prevents the following theorem from being silently transferred to the core theory 𝑇0.
Fix a new type symbol 𝑃. Constructor 𝑖 consists of a nonrecursive telescope Γ𝑖 and finitely many recursive arity telescopes Δ𝑖1(𝛾),…,Δ𝑖𝑟𝑖(𝛾), none containing 𝑃. It has the form 𝗂𝗇𝗍𝗋𝗈𝑖:∏𝛾:Γ𝑖(Δ𝑖1(𝛾)→𝑃)→⋯→(Δ𝑖𝑟𝑖(𝛾)→𝑃)→𝑃. Here a displayed arrow from a telescope abbreviates its iterated dependent product. Equality of the parameters and all recursive maps, after transport along the parameter equality, gives 𝗂𝗇𝗍𝗋𝗈𝑖(𝛾,𝑏1,…,𝑏𝑟𝑖)=𝗂𝗇𝗍𝗋𝗈𝑖(𝛾′,𝑏′1,…,𝑏′𝑟𝑖):𝑃.
Given a family 𝑧:𝑃⊢𝑀(𝑧)𝗍𝗒𝗉𝖾 and steps 𝑑𝑖:∏𝛾:Γ𝑖∏𝑏1:Δ𝑖1(𝛾)→𝑃⋯∏𝑏𝑟𝑖:Δ𝑖𝑟𝑖(𝛾)→𝑃⎛⎜
⎜
⎜
⎜⎝∏𝑢1:Δ𝑖1(𝛾)𝑀(𝑏1𝑢1)⎞⎟
⎟
⎟
⎟⎠→⋯→⎛⎜
⎜
⎜
⎜
⎜⎝∏𝑢𝑟𝑖:Δ𝑖𝑟𝑖(𝛾)𝑀(𝑏𝑟𝑖𝑢𝑟𝑖)⎞⎟
⎟
⎟
⎟
⎟⎠→𝑀(𝗂𝗇𝗍𝗋𝗈𝑖(𝛾,𝑏1,…,𝑏𝑟𝑖)), the schema supplies 𝖾𝗅𝗂𝗆𝑃(𝑑1,…,𝑑𝑛):∏𝑧:𝑃𝑀(𝑧) and the equations 𝖾𝗅𝗂𝗆𝑃(⃗𝑑,𝗂𝗇𝗍𝗋𝗈𝑖(𝛾,𝑏1,…,𝑏𝑟𝑖))=𝑑𝑖(𝛾,𝑏1,…,𝑏𝑟𝑖,𝜆𝑢1.𝖾𝗅𝗂𝗆𝑃(⃗𝑑,𝑏1𝑢1),…,𝜆𝑢𝑟𝑖.𝖾𝗅𝗂𝗆𝑃(⃗𝑑,𝑏𝑟𝑖𝑢𝑟𝑖)). This is an external dependent-elimination schema for one unindexed type in TD. It is not an indexed family schema, and no rule in the display is imported into the intensional core 𝑇0.
For a set 𝑈, an Aczel rule set on 𝑈 is a set of pairs (𝑢,𝑣) with 𝑢⊆𝑈 and 𝑣∈𝑈, displayed 𝑢/𝑣. A subset of 𝑈 is closed under the rule set when it contains 𝑣 whenever it contains every member of 𝑢. The rule set is deterministic when two rules with the same conclusion have the same premise set [Acz77].
Fix a signature of definition 73.47 whose parameter and arity telescopes have set interpretations. Choose an infinite regular cardinal 𝜅 such that every parameter and arity interpretation lies in 𝑉𝜅 and every interpreted arity has cardinality smaller than 𝜅. Then the signature determines a deterministic Aczel rule set on 𝑉𝜅. Its least closed subset interprets 𝑃 and the dependent elimination equations.
Proof of Proposition 73.48 — Rule-set interpretation
Proof. Interpret a parameter tuple 𝛾:Γ𝑖 and recursive maps 𝑏𝑘:Δ𝑖𝑘(𝛾)→𝑉𝜅. Form the rule ⋃1≤𝑘≤𝑟𝑖rng(𝑏𝑘)⟨𝑖,𝛾,𝑏1,…,𝑏𝑟𝑖⟩. The numerator denotes the set of premises, not one premise containing their union. The cardinal bound and regularity put every map 𝑏𝑘 and every premise set in 𝑉𝜅; infinitude and closure under finite tupling put the finite tag and tuple forming the conclusion there as well. Hence these pairs form a rule set on 𝑉𝜅. Its conclusion records 𝑖, 𝛾, and all the 𝑏𝑘, so equal conclusions determine equal premise sets: the rule set is deterministic.
Let 𝐼 be the intersection of all subsets of 𝑉𝜅 closed under these rules. Closure makes every tagged conclusion an element of 𝐼 when all values of its 𝑏𝑘 lie in 𝐼, which interprets 𝗂𝗇𝗍𝗋𝗈𝑖. Conversely, the definition of 𝐼 gives induction on rule generation.
Interpret 𝑀 as a family of sets over 𝐼. For steps 𝑑𝑖, deterministic rule recursion defines a section at a tagged conclusion by applying 𝑑𝑖 to 𝛾, the maps 𝑏𝑘, and the already-defined sections at every value 𝑏𝑘𝑢. Rule induction proves that the section is defined on all of 𝐼; determinism makes the defining clause independent of a choice of generating rule, and induction gives uniqueness. Evaluating it at one rule conclusion is exactly the elimination equation in definition 73.47. ◻
The second result starts from operators rather than constructor lists.
For closed types 𝐾 of TD, define Φ(𝑋)::=𝑋∣𝐾∣Φ0(𝑋)+Φ1(𝑋)∣Φ0(𝑋)×Φ1(𝑋)∣𝐾→Φ0(𝑋). The variable 𝑋 is forbidden to the left of an arrow. Each expression acts on functions by identity, constant, sum, product, and postcomposition, respectively, and hence defines an endofunctor on the extensional category of closed types.
Suppose a signature of definition 73.47 has finitely many constructors and, for each 𝑖,𝑗, the recursive arity telescope has a closed total type 𝐷𝑖𝑗 independent of the parameter 𝛾. If 𝐺𝑖 is the closed total type of the parameter telescope Γ𝑖, then its constructor endofunctor Φ(𝑋):=∑𝑖⎛⎜
⎜
⎜
⎜⎝𝐺𝑖×𝑟𝑖∏𝑗=1(𝐷𝑖𝑗→𝑋)⎞⎟
⎟
⎟
⎟⎠ is generated by the grammar of definition 73.49.
Proof of Lemma 73.50 — Bridge from constant-telescope signatures
Proof. Each factor 𝐷𝑖𝑗→𝑋 is an exponential clause applied to the identity operator. Finite products combine the factors, with 𝑁1 for the empty product; product with the constant 𝐺𝑖 adds the nonrecursive parameters. Finite sums then combine the constructor cases. These are exactly the five clauses of the operator grammar. ◻
When an arity Δ𝑖𝑗(𝛾) genuinely depends on 𝛾, the displayed endofunctor contains a dependent family of exponentials and need not belong to the 1997 grammar. The rule-set interpretation above covers that dependent case; the W-representation theorem below applies to the constant-telescope fragment isolated by lemma 73.50 and to every other operator generated directly by the grammar.
For every operator Φ of definition 73.49, there are a closed type 𝐴, a family 𝐵:𝐴→U0, and a natural isomorphism 𝜈𝑋:Φ(𝑋)≅∑𝑎:𝐴(𝐵(𝑎)→𝑋). Writing 𝗆𝖺𝗉𝐴,𝐵(𝑟)((𝑎,𝑞)):=(𝑎,𝑟∘𝑞), naturality means that, for every 𝑟:𝑋→𝑌 and 𝑥:Φ(𝑋), 𝜈𝑌(Φ(𝑟)(𝑥))=𝗆𝖺𝗉𝐴,𝐵(𝑟)(𝜈𝑋𝑥).
Proof. Induct on the grammar of Φ. For 𝑋, take 𝐴=𝑁1 and 𝐵(⋆)=𝑁1; evaluation at ⋆ and constant abstraction are inverse. For a constant 𝐾, take 𝐴=𝐾 and 𝐵(𝑘)=𝑁0; the unique map 𝑁0→𝑋 carries no data.
Suppose the induction hypothesis gives (𝐴𝑗,𝐵𝑗,𝜈𝑗) for Φ𝑗. For a sum take 𝐴=𝐴0+𝐴1 and use coproduct elimination into U0 to choose 𝐵 by cases from 𝐵0 and 𝐵1. The two tagged summands give the required inverse maps. For a product take 𝐴=𝐴0×𝐴1,𝐵(𝑎0,𝑎1)=𝐵0(𝑎0)+𝐵1(𝑎1). A function out of the displayed coproduct is the same as a pair of functions, one from each summand. Combining that equality with 𝜈0𝑋×𝜈1𝑋 gives the product isomorphism.
For 𝐾→Φ0(𝑋), take 𝐴=𝐾→𝐴0,𝐵(𝑓)=∑𝑘:𝐾𝐵0(𝑓(𝑘)). Pointwise use of 𝜈0𝑋 sends ℎ:𝐾→Φ0(𝑋) to (𝜆𝑘.𝗉𝗋1(𝜈0𝑋(ℎ𝑘)),𝜆𝑝.𝗉𝗋2(𝜈0𝑋(ℎ(𝗉𝗋1(𝑝))))(𝗉𝗋2(𝑝))). The inverse sends (𝑓,𝑞) to 𝜆𝑘.(𝜈0𝑋)−1((𝑓𝑘,𝜆𝑏.𝑞((𝑘,𝑏)))). Dependent beta and eta, function extensionality, and the induction-hypothesis inverse laws prove that the two composites are identities. Each construction commutes with postcomposition in 𝑋. For identity and constants this is a beta calculation; for sums it is the calculation in the selected summand; and for products it is componentwise. In the exponential case, for 𝑟:𝑋→𝑌, the second component along either composite is (𝑘,𝑏)↦𝑟(𝑞((𝑘,𝑏))), while the first component is unchanged. These five calculations prove the displayed naturality equation. ◻
Proof of Theorem 73.52 — Dybjer's W-representation theorem
Proof. Choose 𝐴,𝐵,𝜈 from lemma 73.51, and put 𝑊:=𝖶𝑎:𝐴𝐵(𝑎). Its algebra structure is 𝜄Φ:=𝜆𝑥.𝗌𝗎𝗉(𝗉𝗋1(𝜈𝑊𝑥),𝗉𝗋2(𝜈𝑊𝑥)):Φ(𝑊)→𝑊. Let 𝑒:Φ(𝐶)→𝐶 be any algebra. W-recursion defines 𝖿𝗈𝗅𝖽𝑒:𝑊→𝐶 using the step 𝑑𝑒𝑎𝑏ℎ:=𝑒(𝜈−1𝐶((𝑎,ℎ))),ℎ:𝐵(𝑎)→𝐶. For 𝑥:Φ(𝑊), write 𝜈𝑊𝑥=(𝑎,𝑏). W-computation and the naturality equation in lemma 73.51 give 𝖿𝗈𝗅𝖽𝑒(𝜄Φ𝑥)=𝑒(𝜈−1𝐶((𝑎,𝖿𝗈𝗅𝖽𝑒∘𝑏)))=𝑒(Φ(𝖿𝗈𝗅𝖽𝑒)(𝑥)), so 𝖿𝗈𝗅𝖽𝑒 is an algebra morphism.
For uniqueness, let ℎ:𝑊→𝐶 be another algebra morphism. Apply W-induction to the motive 𝑤:𝑊⊢𝖨𝖽𝐶(ℎ𝑤,𝖿𝗈𝗅𝖽𝑒𝑤). At 𝗌𝗎𝗉(𝑎,𝑏) its induction hypotheses are ℎ(𝑏𝑦)=𝖿𝗈𝗅𝖽𝑒(𝑏𝑦) for every 𝑦:𝐵(𝑎). Function extensionality identifies ℎ∘𝑏 with 𝖿𝗈𝗅𝖽𝑒∘𝑏. Since 𝗌𝗎𝗉(𝑎,𝑏)=𝜄Φ(𝜈−1𝑊((𝑎,𝑏))), the algebra-morphism law for ℎ, naturality of 𝜈, and the induction hypotheses calculate ℎ(𝗌𝗎𝗉(𝑎,𝑏))=𝑒(𝜈−1𝐶((𝑎,ℎ∘𝑏)))=𝑒(𝜈−1𝐶((𝑎,𝖿𝗈𝗅𝖽𝑒∘𝑏)))=𝖿𝗈𝗅𝖽𝑒(𝗌𝗎𝗉(𝑎,𝑏)). W-induction followed by function extensionality gives ℎ=𝖿𝗈𝗅𝖽𝑒. Thus (𝑊,𝜄Φ) is initial. ◻
The proof used extensional uniqueness in the constant, product, and exponential cases and again when proving uniqueness of the algebra morphism. Dybjer explicitly notes that the representation does not work directly in intensional type theory. Setoids provide an indirect interpretation [Hof95], but that construction is not a theorem that the encoded W-types of theorem 28.32 possess judgmental dependent eliminators. Neither lemma 73.51 nor theorem 73.52 is asserted for 𝑇0.
★★☆ Verify the naturality equation of lemma 73.51 for the product constructor Φ0(𝑋)×Φ1(𝑋). Then specialize the proved equation to 𝑟=𝖿𝗈𝗅𝖽𝑒 and 𝜈𝑊(𝑥)=(𝑎,𝑏), obtaining 𝜈𝐶(Φ(𝖿𝗈𝗅𝖽𝑒)(𝑥))=(𝑎,𝖿𝗈𝗅𝖽𝑒∘𝑏), and recalculate the algebra-morphism square as a check.
★★★ Explain why beta alone does not make an arbitrary 𝑦:𝑁0→𝐶 definitionally equal to 𝜆(𝑥:𝑁0).𝗋𝖾𝖼𝟎(𝑥), or an arbitrary 𝑦:𝑁1→𝐶 definitionally equal to 𝜆(𝑥:𝑁1).𝑦⋆. Identify the two base cases of lemma 73.51 that need these equalities. Then state the pointwise empty- and unit-type uniqueness principles which, together with function extensionality, establish the two function equalities in TD.
Source boundary. The constructor telescope and rule-set reconstruction follow [Dyb91]; the dependent eliminator and its set interpretation follow [Dyb91]. The operator grammar, container normal form, initial-algebra theorem, and warning about the intensional setting follow [Dyb97]. The displayed TD signature records the extensional equalities used on those pages; it is not an attribution of the theorem to the intensional signature fixed earlier in this chapter. The name 𝑇0 in this book denotes that local intensional core; it is not Dybjer’s separately numbered base calculus 𝑇0 in the 1991 source.
Suggested first pass.
None of these problems is a prerequisite for a later chapter. Begin with exercise 73.27, then complete exercise 73.30.
★★☆ Derive the W-recursor from W-elimination by taking a constant motive 𝐶. Write the branch type and calculate the constructor equation. Then explain why the same specialization cannot recover an eliminator whose motive depends on the particular tree.
★★★ Instantiate the polynomial-signature eliminator for binary trees with leaves labelled in 𝐴. Define leaf count and mirror, calculate both constructor cases, and prove that mirroring twice is judgmentally the identity by tree induction.
★★★ Suppose, contrary to strict positivity, that one admitted a type 𝐷 with constructor 𝗋𝗈𝗅𝗅:(𝐷→𝐷)→𝐷 and a pattern equation 𝗎𝗇𝗋𝗈𝗅𝗅(𝗋𝗈𝗅𝗅(𝑓))≡𝑓. Define 𝛿:𝐷→𝐷 by 𝛿𝑥:=𝗎𝗇𝗋𝗈𝗅𝗅𝑥𝑥 and calculate the reduction of 𝛿(𝗋𝗈𝗅𝗅(𝛿)). Explain which occurrence of 𝐷 in the constructor argument is negative and which metatheoretic property the resulting loop refutes.
★★★Practical project.inductive-positivity-checker Implement in Agda or Kappa the strict-positivity traversal of definition 28.34. The maintained sign records whether the current position is positive. Accept natural numbers, lists, and W-trees; reject 𝐷→𝐷 when that whole function type occurs as a constructor argument, that is, reject (𝐷→𝐷)→𝐷 and report the path to its negative occurrence. By contrast, accept 𝐷→𝐷 as the whole type of a constructor with one recursive argument. Mutation test: preserving instead of reversing the sign at a Π-domain must make the negative example fail the acceptance suite. Before implementing the traversal, classify the natural-number, W-tree, and negative 𝐷 signatures on paper and record the path and sign at every Π-domain. This finite trace is the checker’s specification.
Sources. Natural numbers and finite types occur in Martin-Löf’s early systems [ML98]; W-types and their tree reading are developed in [ML82, ML84]. Textbook treatments include [NPS90, NPS00, Tho91, Pal14]. The higher-type natural-number recursor is Gödel’s System T [GLT89]. The polynomial-signature viewpoint and the role of strict positivity are treated in [AG26] and [Har16].