EquivFunctor.mapEquiv_trans
theorem EquivFunctor.mapEquiv_trans :
∀ (f : Type u₀ → Type u₁) [inst : EquivFunctor f] {α β γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ),
(EquivFunctor.mapEquiv f ab).trans (EquivFunctor.mapEquiv f bc) = EquivFunctor.mapEquiv f (ab.trans bc)
The theorem `EquivFunctor.mapEquiv_trans` states that for any `EquivFunctor` f and any two equivalences `ab : α ≃ β` and `bc : β ≃ γ`, the composition of `EquivFunctor.mapEquiv f` applied to `ab` and `bc` is the same as `EquivFunctor.mapEquiv f` applied to the composition of `ab` and `bc`. In other words, the process of mapping equivalences is consistent with the operation of composing equivalences. For plain `Functor`s, this fact is known as the `map_map` theorem when it is applied or `map_comp_map` when it is not applied.
More concisely: The map function of an EquivFunctor preserves composition of equivalences.
|
EquivFunctor.map_refl'
theorem EquivFunctor.map_refl' :
∀ {f : Type u₀ → Type u₁} [self : EquivFunctor f] (α : Type u₀), EquivFunctor.map (Equiv.refl α) = id
The theorem `EquivFunctor.map_refl'` states that for any type functor `f` that is an instance of the `EquivFunctor` class, and for any type `α`, the `map` function of `f` preserves the identity morphism. In other words, when the `map` function is applied to the reflexive equivalence (an equivalence from a type to itself), the result is the identity function. This highlights a key property of the `EquivFunctor` class: it respects the identity morphism in the category of types.
More concisely: For any type functor `f` that is an instance of `EquivFunctor`, `f.map (Refl : α ≃ α) = id : f α → f α`.
|
EquivFunctor.map_trans'
theorem EquivFunctor.map_trans' :
∀ {f : Type u₀ → Type u₁} [self : EquivFunctor f] {α β γ : Type u₀} (k : α ≃ β) (h : β ≃ γ),
EquivFunctor.map (k.trans h) = EquivFunctor.map h ∘ EquivFunctor.map k
The theorem `EquivFunctor.map_trans'` states that for any type map `f` that is an `EquivFunctor` and for any types `α`, `β`, and `γ`, the `map` operation of the `EquivFunctor` is functorial on equivalences. Specifically, if `k` is an equivalence from `α` to `β`, and `h` is an equivalence from `β` to `γ`, then mapping the composition of `k` and `h` (denoted `k.trans h`) is equivalent to the composition of the map of `h` and the map of `k`, i.e., `EquivFunctor.map (k.trans h) = EquivFunctor.map h ∘ EquivFunctor.map k`. In simpler terms, it tells us that mapping the composition of two equivalences is the same as composing the maps of each equivalence, which is a property expected from a functor (preservation of composition).
More concisely: For any EquivFunctor `f` and equivalences `k : α ≡ β` and `h : β ≡ γ`, `EquivFunctor.map (k.trans h) = EquivFunctor.map h ∘ EquivFunctor.map k`.
|