∀ (X X_1 : Type u_1),
  (CategoryTheory.Limits.Types.binaryProductLimit X X_1).lift
      (CategoryTheory.Limits.BinaryFan.mk Prod.fst
        (CategoryTheory.CategoryStruct.comp Prod.snd (CategoryTheory.CategoryStruct.id X_1))) =
    CategoryTheory.CategoryStruct.id (X × X_1)