∀ {D : CompHaus},
  CategoryTheory.CategoryStruct.comp (CompHausLike.ofHom (fun x => True) { toFun := id, continuous_toFun := ⋯ })
      (CompHausLike.ofHom (fun x => True) { toFun := id, continuous_toFun := ⋯ }) =
    CategoryTheory.CategoryStruct.id (compactumToCompHaus.obj (Compactum.ofTopologicalSpace ↑D.toTop))