∀ {X Y Z : SSet.Truncated 2} (f : X ⟶ Y) (g : Y ⟶ Z),
  SSet.OneTruncation₂.map (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (SSet.OneTruncation₂.map f) (SSet.OneTruncation₂.map g)