mathlib documentation

data.​equiv.​functor

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] [is_lawful_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] [is_lawful_functor f] (h : α β) (x : f α) :

@[simp]
theorem functor.​map_equiv_symm_apply {α β : Type u} (f : Type uType v) [functor f] [is_lawful_functor f] (h : α β) (y : f β) :

@[simp]
theorem functor.​map_equiv_refl {α : Type u} (f : Type uType v) [functor f] [is_lawful_functor f] :

def bifunctor.​map_equiv {α β : Type u} {α' β' : Type v} (F : Type uType vType w) [bifunctor F] [is_lawful_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] [is_lawful_bifunctor F] (h : α β) (h' : α' β') (x : F α α') :

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

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