LawfulMvFunctor.comp_map
theorem LawfulMvFunctor.comp_map :
∀ {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} [inst : MvFunctor F] [self : LawfulMvFunctor F] {α β γ : TypeVec.{u_2} n}
(g : α.Arrow β) (h : β.Arrow γ) (x : F α),
MvFunctor.map (TypeVec.comp h g) x = MvFunctor.map h (MvFunctor.map g x)
The theorem `LawfulMvFunctor.comp_map` states that for any natural number `n`, any multivariate functor `F` from `n`-tuples of types to a type, any lawful multivariate functor on `F`, and any three `n`-tuples of types `α`, `β`, and `γ`, if `g` is a mapping from `α` to `β` and `h` is a mapping from `β` to `γ`, and `x` is any element of the functor `F` on `α`, then applying the multivariate functor map operation to the composition of `h` and `g` on `x` is equal to first applying the multivariate functor map operation to `g` on `x` and then applying the multivariate functor map operation to `h` on the result. In essence, it's saying that the `map` operation of a lawful multivariate functor preserves the composition of arrows, a crucial property that is expected of functors in category theory.
More concisely: Given a lawful multivariate functor F and natural number n, for any mappings g: α → β and h: β → γ between n-tuples of types, and any element x of F α, the application of the functor map F.map to the composition of g and h is equal to the composition of the applications of F.map to g and h: F.map (g ∘ h) (F.map g x) = F.map h (F.map g x).
|
MvFunctor.map_map
theorem MvFunctor.map_map :
∀ {n : ℕ} {α β γ : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] [inst_1 : LawfulMvFunctor F]
(g : α.Arrow β) (h : β.Arrow γ) (x : F α),
MvFunctor.map h (MvFunctor.map g x) = MvFunctor.map (TypeVec.comp h g) x
The theorem `MvFunctor.map_map` states that for any natural number `n`, any three `n`-tuples of types `α`, `β`, `γ`, and any type constructor `F` that takes an `n`-tuple of types to a type, given that `F` is a multivariate functor (MvFunctor) and respects the laws of a lawful multivariate functor (LawfulMvFunctor), and given two arrows `g` and `h` in the category of `n`-tuples of types (`TypeVec`) and an `n`-tuple of types `x`, mapping `x` first by `g` and then by `h` (i.e., `MvFunctor.map h (MvFunctor.map g x)`) is equivalent to mapping `x` directly by the composition of `h` and `g` (i.e., `MvFunctor.map (TypeVec.comp h g) x`). This is a form of functor law in this specific category of n-tuples of types.
More concisely: For any natural number `n`, given an `n`-tuple `x` of types, a multivariate functor `F` that is lawful, and arrows `g` and `h` in the category of `n`-tuples, `MvFunctor.map (TypeVec.comp h g) x = MvFunctor.map (h ∘ g) x`.
|
MvFunctor.id_map
theorem MvFunctor.id_map :
∀ {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] [inst_1 : LawfulMvFunctor F]
(x : F α), MvFunctor.map TypeVec.id x = x
The theorem `MvFunctor.id_map` asserts that for any natural number `n`, any n-tuple of types `α`, and any multivariate functor `F` that abides by the laws of a `LawfulMvFunctor`, applying the `MvFunctor.map` operation with the identity function `TypeVec.id` to any element `x` of `F α` simply produces `x` itself. In other words, mapping the identity function over any value in a lawful multivariate functor leaves that value unchanged. This is the multivariate functor version of the identity law.
More concisely: For any lawful multivariate functor F and any n-tuple of types α, the application of the map function with the identity function to any element x in F α results in x.
|
LawfulMvFunctor.id_map
theorem LawfulMvFunctor.id_map :
∀ {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} [inst : MvFunctor F] [self : LawfulMvFunctor F] {α : TypeVec.{u_2} n}
(x : F α), MvFunctor.map TypeVec.id x = x
The theorem `LawfulMvFunctor.id_map` states that for any natural number `n`, any multivariate functor `F` mapping `n`-tuples of types to some type (i.e., `F : TypeVec.{u_2} n → Type u_1`), and any `n`-tuple of types `α`, the `map` function preserves identities. In more specific terms, it means that if we apply the `map` function to the identity function on `α` and some value `x : F α`, we get back the same value `x`. This is a property we would expect from any functor, as it shows consistency with the functorial nature of `map`, which should preserve the identity morphism (or function, in this case) in the category.
More concisely: For any multivariate functor `F` and any `n-tuple` of types `α`, the `map` function applied to the identity function on `α` is the identity function on `F α`.
|