∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (f : E ≅ F),
  (CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso f).inverse =
    CategoryTheory.PreOneHypercover.Hom.mapMulticospan f.inv