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
.
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
.
The action of
f
on isomorphisms.- map_refl' (α : Type u₀) : EquivFunctor.map (Equiv.refl α) = id
map
off
preserves the identity morphism. - map_trans' {α β γ : Type u₀} (k : α ≃ β) (h : β ≃ γ) : EquivFunctor.map (k.trans h) = EquivFunctor.map h ∘ EquivFunctor.map k
map
is functorial on equivalences.
Instances
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 := ⋯ }
Instances For
The composition of mapEquiv
s is carried over the EquivFunctor
.
For plain Functor
s, this lemma is named map_map
when applied
or map_comp_map
when not applied.
Equations
- EquivFunctor.ofLawfulFunctor f = { map := fun {x x_1 : Type ?u.26} (e : x ≃ x_1) => Functor.map ⇑e, map_refl' := ⋯, map_trans' := ⋯ }