mathlib3 documentation

logic.equiv.functor

Functor and bifunctors can be applied to equivs. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 u Type v) [functor f] [is_lawful_functor f] (h : α β) :
f α f β

Apply a functor to an equiv.

Equations
@[simp]
theorem functor.map_equiv_apply {α β : Type u} (f : Type u Type v) [functor f] [is_lawful_functor f] (h : α β) (x : f α) :
@[simp]
theorem functor.map_equiv_symm_apply {α β : Type u} (f : Type u Type v) [functor f] [is_lawful_functor f] (h : α β) (y : f β) :
@[simp]
def bifunctor.map_equiv {α β : Type u} {α' β' : Type v} (F : Type u Type v Type w) [bifunctor F] [is_lawful_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 u Type v Type w) [bifunctor F] [is_lawful_bifunctor F] (h : α β) (h' : α' β') (x : F α α') :
@[simp]
theorem bifunctor.map_equiv_symm_apply {α β : Type u} {α' β' : Type v} (F : Type u Type v Type w) [bifunctor F] [is_lawful_bifunctor F] (h : α β) (h' : α' β') (y : F β β') :
@[simp]
theorem bifunctor.map_equiv_refl_refl {α : Type u} {α' : Type v} (F : Type u Type v Type w) [bifunctor F] [is_lawful_bifunctor F] :