C : Type u
inst✝ : Category C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ ∀ (j : Discrete WalkingPair),
    tensorHom ℬ (𝟙 X₁) (𝟙 X₂) ≫ (ℬ X₁ X₂).cone.π.app j = 𝟙 (tensorObj ℬ X₁ X₂) ≫ (ℬ X₁ X₂).cone.π.app j
C : Type u
inst✝ : Category C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ tensorHom ℬ (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj ℬ X₁ X₂)
apply IsLimit.hom_ext (ℬ _ _).isLimit
case mk.right
C : Type u
inst✝ : Category C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
⊢ IsLimit.lift (ℬ X₁ X₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ 𝟙 X₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ 𝟙 X₂)) ≫
      BinaryFan.snd (ℬ X₁ X₂).cone =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ BinaryFan.snd (ℬ X₁ X₂).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₁ X₂ : C
⊢ tensorHom ℬ (𝟙 X₁) (𝟙 X₂) ≫ (ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ (ℬ X₁ X₂).cone.π.app { as := WalkingPair.right }
dsimp [tensorHom]
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₁ X₂ : C
⊢ IsLimit.lift (ℬ X₁ X₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ 𝟙 X₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ 𝟙 X₂)) ≫
      BinaryFan.snd (ℬ X₁ X₂).cone =
    𝟙 (tensorObj ℬ X₁ X₂) ≫ BinaryFan.snd (ℬ X₁ X₂).cone
simp