move(category_theory/category/default): rename to `category_theory.ba…

…sic` (#9412)
leanprover-community · Sep 30, 2021 · 6e6fe1f · 6e6fe1f
1 parent 4091f72
commit 6e6fe1f
Show file tree

Hide file tree

Showing 10 changed files with 7 additions and 10 deletions.
diff --git a/src/category_theory/category/Kleisli.lean b/src/category_theory/category/Kleisli.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import category_theory.category
+import category_theory.category.basic
 
 /-!
 # The Kleisli construction on the Type category

diff --git a/src/category_theory/category/Rel.lean b/src/category_theory/category/Rel.lean
@@ -3,7 +3,7 @@ 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.category
+import category_theory.category.basic
 
 /-!
 The category of types with binary relations as morphisms.

diff --git a/src/category_theory/category/default.lean → src/category_theory/category/basic.lean b/src/category_theory/category/default.lean → src/category_theory/category/basic.lean
diff --git a/src/category_theory/category/preorder.lean b/src/category_theory/category/preorder.lean
@@ -5,8 +5,6 @@ Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
 -/
 
 import category_theory.category.Cat
-import category_theory.category.default
-import category_theory.opposites
 import order.category.Preorder
 
 /-!

diff --git a/src/category_theory/category/ulift.lean b/src/category_theory/category/ulift.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Adam Topaz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz
 -/
-import category_theory.category
+import category_theory.category.basic
 import category_theory.equivalence
 import category_theory.filtered
 

diff --git a/src/category_theory/concrete_category/bundled.lean b/src/category_theory/concrete_category/bundled.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather
 -/
-import category_theory.category
+import category_theory.category.basic
 
 /-!
 # Bundled types

diff --git a/src/control/equiv_functor.lean b/src/control/equiv_functor.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.category
+import category_theory.category.basic
 import data.equiv.functor
 
 /-!

diff --git a/src/control/fold.lean b/src/control/fold.lean
@@ -7,7 +7,6 @@ import algebra.free_monoid
 import algebra.opposites
 import control.traversable.instances
 import control.traversable.lemmas
-import category_theory.category
 import category_theory.endomorphism
 import category_theory.types
 import category_theory.category.Kleisli

diff --git a/src/tactic/reassoc_axiom.lean b/src/tactic/reassoc_axiom.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import category_theory.category
+import category_theory.category.basic
 
 /-!
 # Tools to reformulate category-theoretic axioms in a more associativity-friendly way

diff --git a/src/tactic/slice.lean b/src/tactic/slice.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.category
+import category_theory.category.basic
 
 open category_theory