MvQPF.Fix.rec_eq

theorem MvQPF.Fix.rec_eq : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [inst : MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α.append1 β) → β) (x : F (α.append1 (MvQPF.Fix F α))), MvQPF.Fix.rec g (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: MvQPF.Fix.rec g) x)

The theorem `MvQPF.Fix.rec_eq` states that for any natural number `n`, and for any functor `F` of a tuple of types (or `TypeVec`) with `n+1` number of types, given a multivariate quasi-polynomial functor `q` of `F` and an instance `inst` of `F` being a multivariate functor, for any tuple of types `α` with `n` number of types and any type `β`, and given a function `g` from `F` applied to the type vector `α` and `β` to `β` and a value `x` of type `F` applied to the type vector `α` and the least fixed point of `F` applied to `α`, the recursor of the least fixed point of `F` applied to `α` using the function `g`, when applied to the constructor of the least fixed point of `F` applied to `α` with the value `x`, is equal to `g` applied to the result of mapping the function composed of the identity function and the recursor of the least fixed point of `F` applied to `α` using the function `g` to `x`. In mathematical terms, this theorem justifies the process of recursion on data types defined as fixed points of functors in a category-theoretic context by showing that the recursor is equivalent to applying a function to a mapped value.

More concisely: For any multivariate quasi-polynomial functor `q` and instance `F` of a multivariate functor, the recursor of the least fixed point of `F` applied to a tuple of types `α` using a function `g`, when applied to the constructor of the least fixed point with a value `x`, equals `g` applied to the mapped value of `x` and the recursor of `g` applied to the least fixed point of `F` using `g`.