∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y}
  {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.fst