flippingEquiv — Mathlib

English

The equivalence between two bifunctor types given by currying and flipping

Русский

Эквивалентность между типами бифункторов, задаваемая каррированием и переворотом

LaTeX

$$$C \ ⥤ D \ ⥤ E \simeq D \ ⥤ C \ ⥤ E$$$

Lean4

/-- The equivalence of types of bifunctors giving by flipping the arguments. -/
@[simps!]
def flippingEquiv : C ⥤ D ⥤ E ≃ D ⥤ C ⥤ E where
  toFun F := F.flip
  invFun F := F.flip
  left_inv _ := rfl
  right_inv _ := rfl

Похожие утверждения