diff --git a/src/category_theory/limits/types.lean b/src/category_theory/limits/types.lean
index e23d350027b4d..17bc0def706b4 100644
--- a/src/category_theory/limits/types.lean
+++ b/src/category_theory/limits/types.lean
@@ -104,6 +104,10 @@ begin
   simp [w j],
 end
 
+lemma limit_ext_iff (F : J ⥤ Type u) (x y : limit F) :
+  x = y ↔ (∀ j, limit.π F j x = limit.π F j y) :=
+⟨λ t _, t ▸ rfl, limit_ext _ _ _⟩
+
 -- TODO: are there other limits lemmas that should have `_apply` versions?
 -- Can we generate these like with `@[reassoc]`?
 -- PROJECT: prove these for any concrete category where the forgetful functor preserves limits?