We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 745e304 commit 8d8b14bCopy full SHA for 8d8b14b
Mathlib/CategoryTheory/Closed/PowerObjects.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
4
Authors: Klaus Gy
5
-/
6
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
7
-import Mathlib.CategoryTheory.Topos.Classifier
+import Mathlib.CategoryTheory.Subobject.Basic
8
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
9
/-!
10
# Elementary Topos (in Elementary Form)
11
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equalizer.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Andrew Yang
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
-import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
0 commit comments