about to define the core of a category

leanprover-community · Mar 18, 2019 · 86df660 · 86df660
1 parent a7cc111
commit 86df660
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/src/category_theory/core.lean b/src/category_theory/core.lean
@@ -0,0 +1,15 @@
+/-
+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 category_theory.equivalence
+
+namespace category_theory
+
+universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+
+
+end category_theory