feat: port CategoryTheory.GlueData (#3099)

Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Mar 26, 2023 · 8f18946 · 8f18946
1 parent d010c13
commit 8f18946
Show file tree

Hide file tree

Showing 2 changed files with 422 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -351,6 +351,7 @@ import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.InvIsos
 import Mathlib.CategoryTheory.Functor.ReflectsIso
+import Mathlib.CategoryTheory.GlueData
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Groupoid.Basic
 import Mathlib.CategoryTheory.Groupoid.VertexGroup