Documentation

Mathlib.Control.EquivFunctor

Functions functorial with respect to equivalences #

An EquivFunctor is a function from Type → Type equipped with the additional data of coherently mapping equivalences to equivalences.

In categorical language, it is an endofunctor of the "core" of the category Type.

class EquivFunctor (f : Type u₀ → Type u₁) :
Type (max (u₀ + 1) u₁)

An EquivFunctor is only functorial with respect to equivalences.

To construct an EquivFunctor, it suffices to supply just the function f α → f β from an equivalence α ≃ β, and then prove the functor laws. It's then a consequence that this function is part of an equivalence, provided by EquivFunctor.mapEquiv.

Instances
    def EquivFunctor.mapEquiv (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} (e : α β) :
    f α f β

    An EquivFunctor in fact takes every equiv to an equiv.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem EquivFunctor.mapEquiv_apply (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} (e : α β) (x : f α) :
      theorem EquivFunctor.mapEquiv_symm_apply (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} (e : α β) (y : f β) :
      @[simp]
      theorem EquivFunctor.mapEquiv_refl (f : Type u₀ → Type u₁) [EquivFunctor f] (α : Type u₀) :
      @[simp]
      theorem EquivFunctor.mapEquiv_symm (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} (e : α β) :
      @[simp]
      theorem EquivFunctor.mapEquiv_trans (f : Type u₀ → Type u₁) [EquivFunctor f] {α : Type u₀} {β : Type u₀} {γ : Type u₀} (ab : α β) (bc : β γ) :

      The composition of mapEquivs is carried over the EquivFunctor. For plain Functors, this lemma is named map_map when applied or map_comp_map when not applied.

      Equations
      theorem EquivFunctor.mapEquiv.injective (f : Type u₀ → Type u₁) [Applicative f] [LawfulApplicative f] {α : Type u₀} {β : Type u₀} (h : ∀ (γ : Type u₀), Function.Injective pure) :