MvPFunctor.map_eq

theorem MvPFunctor.map_eq : ∀ {n : ℕ} (P : MvPFunctor.{u} n) {α β : TypeVec.{u} n} (g : α.Arrow β) (a : P.A) (f : (P.B a).Arrow α), MvFunctor.map g ⟨a, f⟩ = ⟨a, TypeVec.comp g f⟩

The theorem `MvPFunctor.map_eq` states that for any natural number `n`, any multivariate functor `P` of `n` types, any `n-tuple` of types `α` and `β`, any arrow `g` from `α` to `β`, any object `a` in the domain of `P`, and any arrow `f` from `P.B a` to `α`, the application of the `map` function from the multivariate functor class to `g` and the pair `{ fst := a, snd := f }` results in a pair where the first element is `a` and the second element is the composition of the arrows `g` and `f`. This theorem essentially describes how mapping over a multivariate functor behaves in relation to function composition in the category of `n-tuples` of types.

More concisely: For any multivariate functor `P`, natural number `n`, types `α` and `β`, arrow `g : α → β`, object `a` in the domain of `P`, and arrow `f : P.B a → α`, the map function `map P g { a, f } = g ∘ f`.