Theorems · Theorem · category theory

CategoryTheory.bijection_symm_apply_id

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory D] [inst_6 : CategoryTheory.ExponentialIdeal i]
  [inst_7 : CategoryTheory.BraidedCategory C] (A B : C),
  (CategoryTheory.bijection i A B
          (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.reflector i).obj A)
            ((CategoryTheory.reflector i).obj B))).symm
      (CategoryTheory.CategoryStruct.id
        (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.reflector i).obj A)
          ((CategoryTheory.reflector i).obj B))) =
    CategoryTheory.CartesianMonoidalCategory.prodComparison (CategoryTheory.reflector i) A B

Defined in

Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.ReflectiveCategoryTheory.MonoidalClosedCategoryTheory.CartesianMonoidalCategoryCategoryTheory.ExponentialIdealCategoryTheory.BraidedCategory