∀ (X Y : SSet.Truncated 2)
  [inst : Unique (Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.Truncated.Edge.tensor._proof_1 }))]
  [inst_1 :
    Subsingleton
      (Y.obj
        (Opposite.op
          { obj := SimplexCategory.mk 1, property := SSet.Truncated.HomotopyCategory.isoTerminal._proof_1 }))],
  CategoryTheory.Prod.fst X.HomotopyCategory ↑CategoryTheory.Cat.chosenTerminal =
    ((CategoryTheory.Functor.id X.HomotopyCategory).prod
          (SSet.Truncated.HomotopyCategory.isoTerminal Y).inv.toFunctor).comp
      ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
        (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)))