∀ (X : SSet) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst X (SSet.stdSimplex.obj (SimplexCategory.mk 1))) h) =
    h