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] (h : α β) :
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] (h : α β) (h' : α' β') :
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 α α')