∀ {X Y Z W : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W} {cond : CategoryTheory.CategoryStruct.comp f g = 0},
  CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelDesc cond) h = SemiNormedGrp.explicitCokernelDesc ⋯