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₀) : map (Equiv.refl α) = id

  map of f preserves the identity morphism.

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

  map is functorial on equivalences.

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

An EquivFunctor in fact takes every equiv to an equiv.

Equations

• EquivFunctor.mapEquiv f e = { toFun := EquivFunctor.map e, invFun := EquivFunctor.map e.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem EquivFunctor.mapEquiv_apply (f : Type u₀ → Type u₁) [EquivFunctor f] {α β : Type u₀} (e : α ≃ β) (x : f α) : (mapEquiv f e) x = map e x

theorem EquivFunctor.mapEquiv_symm_apply (f : Type u₀ → Type u₁) [EquivFunctor f] {α β : Type u₀} (e : α ≃ β) (y : f β) : (mapEquiv f e).symm y = map e.symm y

@[simp]

theorem EquivFunctor.mapEquiv_refl (f : Type u₀ → Type u₁) [EquivFunctor f] (α : Type u₀) : mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

@[simp]

theorem EquivFunctor.mapEquiv_symm (f : Type u₀ → Type u₁) [EquivFunctor f] {α β : Type u₀} (e : α ≃ β) : (mapEquiv f e).symm = mapEquiv f e.symm

@[simp]

theorem EquivFunctor.mapEquiv_trans (f : Type u₀ → Type u₁) [EquivFunctor f] {α β γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ) : (mapEquiv f ab).trans (mapEquiv f bc) = 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.

@[implicit_reducible, instance 100]

instance EquivFunctor.ofLawfulFunctor (f : Type u₀ → Type u₁) [Functor f] [LawfulFunctor f] : EquivFunctor f

Equations

• EquivFunctor.ofLawfulFunctor f = { map := fun {x x_1 : Type ?u.27} (e : x ≃ x_1) => Functor.map ⇑e, map_refl' := ⋯, map_trans' := ⋯ }

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