fix(category_theory/equivalence): duplicated namespace prefix

leanprover-community · Feb 1, 2019 · 8a9734c · 8a9734c
1 parent d8f6dc4
commit 8a9734c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/category_theory/equivalence.lean b/src/category_theory/equivalence.lean
@@ -199,7 +199,7 @@ def fun_obj_preimage_iso (F : C ⥤ D) [ess_surj F] (d : D) : F.obj (F.obj_preim
 ess_surj.iso F d
 end functor
 
-namespace category_theory.equivalence
+namespace equivalence
 
 def ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F :=
 ⟨ λ Y : D, F.inv.obj Y, λ Y : D, (nat_iso.app F.inv_fun_id Y) ⟩
@@ -252,6 +252,6 @@ def equivalence_of_fully_faithfully_ess_surj
     (by obviously) }
 end
 
-end category_theory.equivalence
+end equivalence
 
 end category_theory