Lean4
/-- Construct an instance of `CartesianMonoidalCategory C` given a terminal object and limit cones
over arbitrary pairs of objects. -/
abbrev ofChosenFiniteProducts : CartesianMonoidalCategory C :=
letI : MonoidalCategoryStruct C :=
{ tensorUnit := 𝒯.cone.pt
tensorObj := tensorObj ℬ
tensorHom := tensorHom ℬ
whiskerLeft X {_ _} g := tensorHom ℬ (𝟙 X) g
whiskerRight {_ _} f Y := tensorHom ℬ f (𝟙 Y)
associator := BinaryFan.associatorOfLimitCone ℬ
leftUnitor X := BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X).isLimit
rightUnitor X := BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit }
{ toMonoidalCategory :=
.ofTensorHom (id_tensorHom_id := id_tensorHom_id ℬ) (tensorHom_comp_tensorHom := tensorHom_comp_tensorHom ℬ)
(pentagon := pentagon ℬ) (triangle := triangle 𝒯 ℬ) (leftUnitor_naturality := leftUnitor_naturality 𝒯 ℬ)
(rightUnitor_naturality := rightUnitor_naturality 𝒯 ℬ) (associator_naturality := associator_naturality ℬ)
isTerminalTensorUnit := .ofUniqueHom (𝒯.isLimit.lift <| asEmptyCone ·) fun _ _ ↦ 𝒯.isLimit.hom_ext (by simp)
fst X Y := BinaryFan.fst (ℬ X Y).cone
snd X Y := BinaryFan.snd (ℬ X Y).cone
tensorProductIsBinaryProduct X
Y :=
BinaryFan.IsLimit.mk _ (fun f g ↦ (BinaryFan.IsLimit.lift' (ℬ X Y).isLimit f g).1)
(fun f g ↦ (BinaryFan.IsLimit.lift' (ℬ X Y).isLimit f g).2.1)
(fun f g ↦ (BinaryFan.IsLimit.lift' (ℬ X Y).isLimit f g).2.2)
(fun f g m hf hg ↦ BinaryFan.IsLimit.hom_ext (ℬ X Y).isLimit (by simpa using hf) (by simpa using hg))
fst_def X Y := (((ℬ X 𝒯.cone.pt).isLimit.fac (BinaryFan.mk _ _) ⟨.left⟩).trans (Category.comp_id _)).symm
snd_def X Y := (((ℬ 𝒯.cone.pt Y).isLimit.fac (BinaryFan.mk _ _) ⟨.right⟩).trans (Category.comp_id _)).symm }
