Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit b084cfc

Browse files
kim-emrwbarton
authored andcommitted
fix(category_theory/equivalence): duplicated namespace prefix (#669)
1 parent e501d02 commit b084cfc

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/category_theory/equivalence.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -199,7 +199,7 @@ def fun_obj_preimage_iso (F : C ⥤ D) [ess_surj F] (d : D) : F.obj (F.obj_preim
199199
ess_surj.iso F d
200200
end functor
201201

202-
namespace category_theory.equivalence
202+
namespace equivalence
203203

204204
def ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F :=
205205
⟨ λ 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
252252
(by obviously) }
253253
end
254254

255-
end category_theory.equivalence
255+
end equivalence
256256

257257
end category_theory

0 commit comments

Comments
 (0)