# mathlibdocumentation

data.equiv.functor

# Functor and bifunctors can be applied to equivs.

We define

def functor.map_equiv (f : Type u → Type v) [functor f] [is_lawful_functor f] :
α ≃ β → f α ≃ f β


and

def bifunctor.map_equiv (F : Type u → Type v → Type w) [bifunctor F] [is_lawful_bifunctor F] :
α ≃ β → α' ≃ β' → F α α' ≃ F β β'

def functor.map_equiv {α β : Type u} (f : Type uType v) [functor f]  :
α βf α f β

Apply a functor to an equiv.

Equations
@[simp]
theorem functor.map_equiv_apply {α β : Type u} (f : Type uType v) [functor f] (h : α β) (x : f α) :
h) x = h <$> x @[simp] theorem functor.map_equiv_symm_apply {α β : Type u} (f : Type uType v) [functor f] (h : α β) (y : f β) : h).symm) y = (h.symm) <$> y

@[simp]
theorem functor.map_equiv_refl {α : Type u} (f : Type uType v) [functor f]  :
= equiv.refl (f α)

def bifunctor.map_equiv {α β : Type u} {α' β' : Type v} (F : Type uType vType w) [bifunctor F]  :
α βα' β'F α α' F β β'

Apply a bifunctor to a pair of equivs.

Equations
@[simp]
theorem bifunctor.map_equiv_apply {α β : Type u} {α' β' : Type v} (F : Type uType vType w) [bifunctor F] (h : α β) (h' : α' β') (x : F α α') :
h') x = h' x

@[simp]
theorem bifunctor.map_equiv_symm_apply {α β : Type u} {α' β' : Type v} (F : Type uType vType w) [bifunctor F] (h : α β) (h' : α' β') (y : F β β') :
h h').symm) y = bimap (h.symm) (h'.symm) y

@[simp]
theorem bifunctor.map_equiv_refl_refl {α : Type u} {α' : Type v} (F : Type uType vType w) [bifunctor F]  :
(equiv.refl α') = equiv.refl (F α α')