C : Type u
inst✝ : Category C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom ≫
      (IsLimit.conePointUniqueUpToIso (ℬ Y X).isLimit (IsLimit.swapBinaryFan (ℬ X Y).isLimit)).hom =
    𝟙 (tensorObj ℬ X Y)
C : Type u
inst✝ : Category C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom ≫ (BinaryFan.braiding (ℬ Y X).isLimit (ℬ X Y).isLimit).hom =
    𝟙 (tensorObj ℬ X Y)
dsimp [tensorHom, Limits.BinaryFan.braiding]
C : Type u
inst✝ : Category C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ∀ (j : Discrete WalkingPair),
    ((IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom ≫
          (IsLimit.conePointUniqueUpToIso (ℬ Y X).isLimit (IsLimit.swapBinaryFan (ℬ X Y).isLimit)).hom) ≫
        (ℬ X Y).cone.π.app j =
      𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app j
C : Type u
inst✝ : Category C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom ≫
      (IsLimit.conePointUniqueUpToIso (ℬ Y X).isLimit (IsLimit.swapBinaryFan (ℬ X Y).isLimit)).hom =
    𝟙 (tensorObj ℬ X Y)
apply (ℬ _ _).isLimit.hom_ext
case mk.right
C : Type u
inst✝ : Category C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (IsLimit.lift (ℬ Y X).isLimit (BinaryFan.swap (ℬ X Y).cone) ≫
        IsLimit.lift (ℬ X Y).isLimit (BinaryFan.swap (ℬ Y X).cone)) ≫
      BinaryFan.snd (ℬ X Y).cone =
    𝟙 (tensorObj ℬ X Y) ≫ BinaryFan.snd (ℬ X Y).cone
case mk.right
C : Type u
inst✝ : Category C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom ≫
        (IsLimit.conePointUniqueUpToIso (ℬ Y X).isLimit (IsLimit.swapBinaryFan (ℬ X Y).isLimit)).hom) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right }
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
no goals
case mk.right
C : Type u
inst✝ : Category C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (IsLimit.lift (ℬ Y X).isLimit (BinaryFan.swap (ℬ X Y).cone) ≫
        IsLimit.lift (ℬ X Y).isLimit (BinaryFan.swap (ℬ Y X).cone)) ≫
      BinaryFan.snd (ℬ X Y).cone =
    𝟙 (tensorObj ℬ X Y) ≫ BinaryFan.snd (ℬ X Y).cone
simp