Theorems · Theorem · category theory

CategoryTheory.Equivalence.symmEquivInverse_map_app

∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X Y : (D ≌ C)ᵒᵖ} (f : X ⟶ Y) (X_1 : C),
  ((CategoryTheory.Equivalence.symmEquivInverse C D).map f).app X_1 =
    CategoryTheory.CategoryStruct.comp ((Opposite.unop X).inverse.map ((Opposite.unop Y).counitInv.app X_1))
      (CategoryTheory.CategoryStruct.comp
        ((Opposite.unop X).inverse.map
          ((CategoryTheory.Equivalence.asNatTrans f.unop).app ((Opposite.unop Y).inverse.obj X_1)))
        ((Opposite.unop X).unitInv.app ((Opposite.unop Y).inverse.obj X_1)))

Defined in

Mathlib.CategoryTheory.Equivalence.Symmetry

Cited by

0 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category