chore(category_theory/groupoid): remove unnecessary imports (#7600)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/core.lean

@@ -3,8 +3,9 @@ Copyright (c) 2019 Scott Morrison All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.groupoid
 import control.equiv_functor
+import category_theory.groupoid
+import category_theory.whiskering
 import category_theory.types
 
 /-!

src/category_theory/epi_mono.lean

@@ -10,13 +10,26 @@ since they are used by some lemmas for `iso`, which is used everywhere.
 -/
 import category_theory.adjunction.basic
 import category_theory.opposites
+import category_theory.groupoid
 
 universes v₁ v₂ u₁ u₂
 
 namespace category_theory
 
 variables {C : Type u₁} [category.{v₁} C]
 
+instance unop_mono_of_epi {A B : Cᵒᵖ} (f : A ⟶ B) [epi f] : mono f.unop :=
+⟨λ Z g h eq, quiver.hom.op_inj ((cancel_epi f).1 (quiver.hom.unop_inj eq))⟩
+
+instance unop_epi_of_mono {A B : Cᵒᵖ} (f : A ⟶ B) [mono f] : epi f.unop :=
+⟨λ Z g h eq, quiver.hom.op_inj ((cancel_mono f).1 (quiver.hom.unop_inj eq))⟩
+
+instance op_mono_of_epi {A B : C} (f : A ⟶ B) [epi f] : mono f.op :=
+⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_epi f).1 (quiver.hom.op_inj eq))⟩
+
+instance op_epi_of_mono {A B : C} (f : A ⟶ B) [mono f] : epi f.op :=
+⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_mono f).1 (quiver.hom.op_inj eq))⟩
+
 section
 variables {D : Type u₂} [category.{v₂} D]
 
@@ -141,17 +154,19 @@ lemma is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section
   : is_iso f :=
 ⟨⟨section_ f, ⟨(cancel_epi_id $ section_ f).mp (by simp), by simp⟩⟩⟩
 
-instance unop_mono_of_epi {A B : Cᵒᵖ} (f : A ⟶ B) [epi f] : mono f.unop :=
-⟨λ Z g h eq, quiver.hom.op_inj ((cancel_epi f).1 (quiver.hom.unop_inj eq))⟩
-
-instance unop_epi_of_mono {A B : Cᵒᵖ} (f : A ⟶ B) [mono f] : epi f.unop :=
-⟨λ Z g h eq, quiver.hom.op_inj ((cancel_mono f).1 (quiver.hom.unop_inj eq))⟩
-
-instance op_mono_of_epi {A B : C} (f : A ⟶ B) [epi f] : mono f.op :=
-⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_epi f).1 (quiver.hom.op_inj eq))⟩
-
-instance op_epi_of_mono {A B : C} (f : A ⟶ B) [mono f] : epi f.op :=
-⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_mono f).1 (quiver.hom.op_inj eq))⟩
+/-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/
+-- FIXME this has unnecessarily become noncomputable!
+noncomputable
+def groupoid.of_trunc_split_mono
+  (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (split_mono f)) :
+  groupoid.{v₁} C :=
+begin
+  apply groupoid.of_is_iso,
+  intros X Y f,
+  trunc_cases all_split_mono f,
+  trunc_cases all_split_mono (retraction f),
+  apply is_iso.of_mono_retraction,
+end
 
 section
 variables {D : Type u₂} [category.{v₂} D]

src/category_theory/groupoid.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Reid Barton All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Scott Morrison, David Wärn
 -/
-import category_theory.epi_mono
+import category_theory.full_subcategory
 
 namespace category_theory
 
@@ -59,20 +59,6 @@ noncomputable
 def groupoid.of_is_iso (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), is_iso f) : groupoid.{v} C :=
 { inv := λ X Y f, inv f }
 
-/-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/
--- FIXME this has unnecessarily become noncomputable!
-noncomputable
-def groupoid.of_trunc_split_mono
-  (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (split_mono f)) :
-  groupoid.{v} C :=
-begin
-  apply groupoid.of_is_iso,
-  intros X Y f,
-  trunc_cases all_split_mono f,
-  trunc_cases all_split_mono (retraction f),
-  apply is_iso.of_mono_retraction,
-end
-
 end
 
 instance induced_category.groupoid {C : Type u} (D : Type u₂) [groupoid.{v} D] (F : C → D) :