∀ (K : SSet) (x : K.obj (Opposite.op { len := 0 })) (Δ Δ' : SimplexCategoryᵒᵖ) (f : Δ ⟶ Δ'),
  (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet).map f) fun x_1 =>
      K.map ((Opposite.unop Δ').const { len := 0 } 0).op x) =
    CategoryTheory.CategoryStruct.comp (fun x_1 => K.map ((Opposite.unop Δ).const { len := 0 } 0).op x) (K.map f)