mathlib documentation


Functions functorial with respect to equivalences

An equiv_functor 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.

structure equiv_functor  :
(Type u₀Type u₁)Type (max (u₀+1) u₁)

An equiv_functor is only functorial with respect to equivalences.

To construct an equiv_functor, 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 equiv_functor.map_equiv.

def equiv_functor.map_equiv (f : Type u₀Type u₁) [equiv_functor f] {α β : Type u₀} :
α βf α f β

An equiv_functor in fact takes every equiv to an equiv.

theorem equiv_functor.map_equiv_apply (f : Type u₀Type u₁) [equiv_functor f] {α β : Type u₀} (e : α β) (x : f α) :

theorem equiv_functor.map_equiv_symm_apply (f : Type u₀Type u₁) [equiv_functor f] {α β : Type u₀} (e : α β) (y : f β) :

def equiv_functor.of_is_lawful_functor (f : Type u₀Type u₁) [functor f] [is_lawful_functor f] :