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 β β'
Apply a functor to an equiv.
Equations
- functor.map_equiv f h = {to_fun := functor.map ⇑h, inv_fun := functor.map ⇑(h.symm), left_inv := _, right_inv := _}
@[simp]
theorem
functor.map_equiv_apply
{α β : Type u}
(f : Type u → Type v)
[functor f]
[is_lawful_functor f]
(h : α ≃ β)
(x : f α) :
⇑(functor.map_equiv f h) x = ⇑h <$> x
@[simp]
theorem
functor.map_equiv_symm_apply
{α β : Type u}
(f : Type u → Type v)
[functor f]
[is_lawful_functor f]
(h : α ≃ β)
(y : f β) :
@[simp]
theorem
functor.map_equiv_refl
{α : Type u}
(f : Type u → Type v)
[functor f]
[is_lawful_functor f] :
functor.map_equiv f (equiv.refl α) = equiv.refl (f α)
def
bifunctor.map_equiv
{α β : Type u}
{α' β' : Type v}
(F : Type u → Type v → Type w)
[bifunctor F]
[is_lawful_bifunctor F] :
Apply a bifunctor to a pair of equivs.
Equations
- bifunctor.map_equiv F h h' = {to_fun := bifunctor.bimap ⇑h ⇑h', inv_fun := bifunctor.bimap ⇑(h.symm) ⇑(h'.symm), left_inv := _, right_inv := _}
@[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 α α') :
⇑(bifunctor.map_equiv F h h') x = bifunctor.bimap ⇑h ⇑h' x
@[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 β β') :
⇑((bifunctor.map_equiv F h h').symm) y = bifunctor.bimap ⇑(h.symm) ⇑(h'.symm) y
@[simp]
theorem
bifunctor.map_equiv_refl_refl
{α : Type u}
{α' : Type v}
(F : Type u → Type v → Type w)
[bifunctor F]
[is_lawful_bifunctor F] :
bifunctor.map_equiv F (equiv.refl α) (equiv.refl α') = equiv.refl (F α α')