# 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.

• map : {α β : Type u₀} → α βf αf β

The action of f on isomorphisms.

• map_refl' : ∀ (α : Type u₀), = id

map of f preserves the identity morphism.

• map_trans' : ∀ {α β γ : Type u₀} (k : α β) (h : β γ), EquivFunctor.map (k.trans h) =

map is functorial on equivalences.

Instances
@[simp]
theorem EquivFunctor.map_refl' {f : Type u₀ → Type u₁} [self : ] (α : Type u₀) :
= id

map of f preserves the identity morphism.

theorem EquivFunctor.map_trans' {f : Type u₀ → Type u₁} [self : ] {α : Type u₀} {β : Type u₀} {γ : Type u₀} (k : α β) (h : β γ) :
EquivFunctor.map (k.trans h) =

map is functorial on equivalences.

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

An EquivFunctor in fact takes every equiv to an equiv.

Equations
• = { toFun := , invFun := EquivFunctor.map e.symm, left_inv := , right_inv := }
Instances For
@[simp]
theorem EquivFunctor.mapEquiv_apply (f : Type u₀ → Type u₁) [] {α : Type u₀} {β : Type u₀} (e : α β) (x : f α) :
x =
theorem EquivFunctor.mapEquiv_symm_apply (f : Type u₀ → Type u₁) [] {α : Type u₀} {β : Type u₀} (e : α β) (y : f β) :
.symm y = EquivFunctor.map e.symm y
@[simp]
theorem EquivFunctor.mapEquiv_refl (f : Type u₀ → Type u₁) [] (α : Type u₀) :
= Equiv.refl (f α)
@[simp]
theorem EquivFunctor.mapEquiv_symm (f : Type u₀ → Type u₁) [] {α : Type u₀} {β : Type u₀} (e : α β) :
.symm = EquivFunctor.mapEquiv f e.symm
@[simp]
theorem EquivFunctor.mapEquiv_trans (f : Type u₀ → Type u₁) [] {α : Type u₀} {β : Type u₀} {γ : Type u₀} (ab : α β) (bc : β γ) :
.trans = EquivFunctor.mapEquiv f (ab.trans 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.

@[instance 100]
instance EquivFunctor.ofLawfulFunctor (f : Type u₀ → Type u₁) [] [] :
Equations
• = { map := fun {α β : Type u₀} (e : α β) => , map_refl' := , map_trans' := }
theorem EquivFunctor.mapEquiv.injective (f : Type u₀ → Type u₁) [] {α : Type u₀} {β : Type u₀} (h : ∀ (γ : Type u₀), ) :