English
A recursor principle for finite types: given data to transport along Equivalences, a base case for Empty, and a base case for Option α, one can produce a value of P α up to truncation.
Русский
Рекурсивный принцип по конечным типам: данные, транспорт по эквиваленциям, базовые случаи для Empty и для Option α дают упрощённую величину P α.
LaTeX
$$truncRecEmptyOption {P : Type u → Sort v} (of_equiv : ∀ {α β}, α ≃ β → P α → P β) (h_empty : P PEmpty) (h_option : ∀ {α} [Fintype α] [DecidableEq α], P α → P (Option α)) (α : Type u) [Fintype α] [DecidableEq α] : Trunc (P α)$$
Lean4
/-- A recursor principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
def truncRecEmptyOption {P : Type u → Sort v} (of_equiv : ∀ {α β}, α ≃ β → P α → P β) (h_empty : P PEmpty)
(h_option : ∀ {α} [Fintype α] [DecidableEq α], P α → P (Option α)) (α : Type u) [Fintype α] [DecidableEq α] :
Trunc (P α) :=
by
suffices ∀ n : ℕ, Trunc (P (ULift <| Fin n))
by
apply Trunc.bind (this (Fintype.card α))
intro h
apply Trunc.map _ (Fintype.truncEquivFin α)
intro e
exact of_equiv (Equiv.ulift.trans e.symm) h
intro n
induction n with
| zero =>
have : card PEmpty = card (ULift (Fin 0)) := by simp only [card_fin, card_pempty, card_ulift]
apply Trunc.bind (truncEquivOfCardEq this)
intro e
apply Trunc.mk
exact of_equiv e h_empty
| succ n
ih =>
have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by simp only [card_fin, card_option, card_ulift]
apply Trunc.bind (truncEquivOfCardEq this)
intro e
apply Trunc.map _ ih
intro ih
exact of_equiv e (h_option ih)
