The eight iota rules of the menagerie hold in the ideal definitional equality

Proved

LeanTT2.menagerie_iota

by Lucas · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

definitionalequalityiotareductionmenagerietypetheory

For every extended fragment, every context, and all terms a, b, e, f, x: the first projection of an explicit pair is definitionally equal to the first component; the second projection to the second component; the case analysis of the binary sum is definitionally equal to the left branch applied to the argument on the left injection, and to the right branch applied to the argument on the right injection; the universe unlift of a lifted term is definitionally the term; the W-recursor applied to an explicit supremum is definitionally equal to the step applied to the seed, the branching function, and the recursive continuation; the equality recursor computes on reflexivity; and the accessibility recursor computes on an explicit introduction, with the recursive continuation. These are the eight iota equations of page 28 of the thesis, lifted from the reduction relation to the ideal definitional equality.

Preamble

import Mathlib
import Definitions.Def_LeanTT2_frag
import Definitions.Def_LeanTT2_spec
import Definitions.Def_LeanTT2_counter

Formal statement

universe u

/-!
# The iota rules of the menagerie in the ideal definitional equality

The eight iota rules displayed on page 28 of Mario Carneiro's thesis
"The Type Theory of Lean" (2019), lifted from the reduction relation of
the fragment to the ideal definitional equality by the conversion
principle `red_deq`: the two projections of an explicit pair, the case
analysis of the binary sum on the two injections, the universe unlift
after a lift, the W-recursor on an explicit supremum (with the recursive
continuation `recW_cont` standing for the function
`b ↦ rec_W e (f b)`), the equality recursor on reflexivity, and the
accessibility recursor on an explicit introduction (with the recursive
continuation `recAcc_cont` standing for the function
`(y, h) ↦ rec_acc e y (f y h)`).
-/

namespace LeanTT2

/-- All eight iota rules of the menagerie (thesis page 28) hold in the
ideal definitional equality of every extended fragment: for every
context and all terms `a`, `b`, `e`, `f`, `x`, the displayed equations
hold up to `deq`. -/
theorem menagerie_iota (F : Frag.{u}) (Γ : F.Ctx) (a b e f x : F.E) :
    F.deq Γ (F.fst (F.pairT a b)) a ∧
    F.deq Γ (F.snd (F.pairT a b)) b ∧
    F.deq Γ (F.caseT a b (F.inl x)) (F.app a x) ∧
    F.deq Γ (F.caseT a b (F.inr x)) (F.app b x) ∧
    F.deq Γ (F.down (F.up x)) x ∧
    F.deq Γ (F.recW e (F.supT a f))
      (F.app (F.app (F.app e a) f) (F.recW_cont e f)) ∧
    F.deq Γ (F.recEq e a (F.reflT a)) e ∧
    F.deq Γ (F.recAcc e x (F.introAcc x f))
      (F.app (F.app (F.app e x) f) (F.recAcc_cont e f)) := by sorry

end LeanTT2

Source

M. Carneiro, The Type Theory of Lean, 2019, section 5.1 (p. 28).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: in any extended fragment, the eight iota-reduction equations of page 28 (the two projections of a pair, the two case analyses of the sum, the unlift of a lift, the W-recursor on a supremum with its continuation, the equality recursor on reflexivity, and the accessibility recursor on an introduction with its continuation) all hold as definitional equalities.

View graph