MvQPF.comp_map

theorem MvQPF.comp_map : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [inst : MvFunctor F] [q : MvQPF F] {α β γ : TypeVec.{u} n} (f : α.Arrow β) (g : β.Arrow γ) (x : F α), MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)

The theorem `MvQPF.comp_map` states that for any natural number `n`, any multivariate functor `F` of `TypeVec n` to some type, and any three `n`-tuples of types `α`, `β`, and `γ`, if we have arrows `f` from `α` to `β` and `g` from `β` to `γ`, and an element `x` of the functor applied to `α`, then mapping the composition of `g` and `f` over `x` is the same as first mapping `f` over `x`, and then mapping `g` over the result. In other words, the process of mapping over the functor respects the composition of arrows, a property that is commonly expected in many kinds of structure in mathematics.

More concisely: For any multivariate functor `F` and natural number `n`, if `f : α → β` and `g : β → γ` are functions, then the application of the composition `g ∘ f` to an element `x : F α` is equal to the composition of the application of `g` to the application of `f` to `x`. In symbols, `(g ∘ f) (F x) = g (F (f x))`.