Theorems · Theorem · category theory

MvQPF.recF_eq

∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β)
  (a : (MvQPF.P F).A) (f' : ((MvQPF.P F).drop.B a).Arrow α) (f : (MvQPF.P F).last.B a → (MvQPF.P F).W α),
  MvQPF.recF g ((MvQPF.P F).wMk a f' f) = g (MvQPF.abs ⟨a, TypeVec.splitFun f' (MvQPF.recF g ∘ f)⟩)

Defined in

Mathlib.Data.QPF.Multivariate.Constructions.Fix

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

MvQPF