remove a whole bunch of redundant imports

the1lab · Sep 18, 2023 · b4a93c5 · b4a93c5
1 parent 5e5bebf
commit b4a93c5
Show file tree

Hide file tree

Showing 126 changed files with 37 additions and 256 deletions.
diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Path.Groupoid
 open import 1Lab.HLevel
 open import 1Lab.Path
 open import 1Lab.Type

diff --git a/src/1Lab/Equiv/Embedding.lagda.md b/src/1Lab/Equiv/Embedding.lagda.md
@@ -10,10 +10,8 @@ description: |
 open import 1Lab.Equiv.Fibrewise
 open import 1Lab.HLevel.Retracts
 open import 1Lab.HLevel.Universe
-open import 1Lab.Path.Groupoid
 open import 1Lab.Type.Sigma
 open import 1Lab.Univalence
-open import 1Lab.Type.Pi
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path

diff --git a/src/1Lab/Equiv/HalfAdjoint.lagda.md b/src/1Lab/Equiv/HalfAdjoint.lagda.md
@@ -11,7 +11,6 @@ description: |
 open import 1Lab.Reflection.Marker
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Path.Groupoid
-open import 1Lab.Equiv.Biinv
 open import 1Lab.Type.Sigma
 open import 1Lab.Univalence
 open import 1Lab.HLevel

diff --git a/src/1Lab/Path/IdentitySystem.lagda.md b/src/1Lab/Path/IdentitySystem.lagda.md
@@ -3,7 +3,6 @@
 open import 1Lab.Equiv.Embedding
 open import 1Lab.Equiv.Fibrewise
 open import 1Lab.HLevel.Retracts
-open import 1Lab.Path.Groupoid
 open import 1Lab.Type.Sigma
 open import 1Lab.Univalence
 open import 1Lab.Type.Pi

diff --git a/src/1Lab/Path/IdentitySystem/Strict.lagda.md b/src/1Lab/Path/IdentitySystem/Strict.lagda.md
@@ -3,11 +3,8 @@
 open import 1Lab.Path.IdentitySystem
 open import 1Lab.HLevel.Retracts
 open import 1Lab.HLevel
-open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
-
-open import Data.Dec.Base
 ```
 -->
 

diff --git a/src/1Lab/Reflection.lagda.md b/src/1Lab/Reflection.lagda.md
@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Type.Sigma
-open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type hiding (absurd)
 

diff --git a/src/1Lab/Reflection/Marker.agda b/src/1Lab/Reflection/Marker.agda
@@ -3,7 +3,6 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Maybe.Base
-open import Data.List.Base
 
 open import Prim.Data.Nat
 

diff --git a/src/1Lab/Reflection/Variables.agda b/src/1Lab/Reflection/Variables.agda
@@ -1,9 +1,7 @@
 open import 1Lab.Reflection hiding (reverse)
 open import 1Lab.Type
 
-open import Data.List.Base hiding (reverse)
 open import Data.Fin.Base
-open import Data.Nat.Base
 
 module 1Lab.Reflection.Variables where
 

diff --git a/src/1Lab/Univalence.lagda.md b/src/1Lab/Univalence.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Path.Groupoid
 open import 1Lab.Type.Sigma
 open import 1Lab.HLevel
 open import 1Lab.Equiv

diff --git a/src/1Lab/Univalence/SIP.lagda.md b/src/1Lab/Univalence/SIP.lagda.md
@@ -8,7 +8,6 @@ description: |
 
 <!--
 ```agda
-open import 1Lab.Path.Groupoid
 open import 1Lab.Type.Sigma
 open import 1Lab.Univalence
 open import 1Lab.Type.Pi

diff --git a/src/Algebra/Group/Ab/Abelianisation.lagda.md b/src/Algebra/Group/Ab/Abelianisation.lagda.md
@@ -4,7 +4,6 @@ open import Algebra.Group.Cat.Base
 open import Algebra.Group.Ab
 open import Algebra.Group
 
-open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Adjoint
 open import Cat.Prelude
 ```

diff --git a/src/Algebra/Group/Ab/Free.lagda.md b/src/Algebra/Group/Ab/Free.lagda.md
@@ -6,7 +6,6 @@ open import Algebra.Group.Free
 open import Algebra.Group.Ab
 open import Algebra.Group
 
-open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Adjoint.Compose
 open import Cat.Functor.Adjoint
 open import Cat.Prelude

diff --git a/src/Algebra/Group/Concrete.lagda.md b/src/Algebra/Group/Concrete.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import 1Lab.Path.Reasoning
-open import 1Lab.Univalence
 
 open import Algebra.Group.Cat.Base
 open import Algebra.Group.Homotopy
@@ -16,7 +15,6 @@ open import Data.Int
 
 open import Homotopy.Connectedness
 open import Homotopy.Space.Circle
-open import Homotopy.Base
 
 open is-group-hom
 open Precategory

diff --git a/src/Algebra/Monoid/Category.lagda.md b/src/Algebra/Monoid/Category.lagda.md
@@ -7,7 +7,6 @@ open import Algebra.Magma
 open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Adjoint.Monadic
 open import Cat.Functor.Equivalence
-open import Cat.Instances.Delooping
 open import Cat.Functor.Properties
 open import Cat.Functor.Adjoint
 open import Cat.Prelude

diff --git a/src/Algebra/Ring/Ideal.lagda.md b/src/Algebra/Ring/Ideal.lagda.md
@@ -8,11 +8,7 @@ open import Algebra.Prelude
 open import Algebra.Group
 open import Algebra.Ring
 
-open import Cat.Functor.FullSubcategory
-
 open import Data.Power
-
-open import Meta.Bind
 ```
 -->
 

diff --git a/src/Algebra/Ring/Module/Action.lagda.md b/src/Algebra/Ring/Module/Action.lagda.md
@@ -7,7 +7,6 @@ open import Algebra.Group
 open import Algebra.Ring
 
 open import Cat.Displayed.Univalence.Thin
-open import Cat.Abelian.Instances.Ab
 open import Cat.Abelian.Base
 open import Cat.Abelian.Endo
 open import Cat.Prelude hiding (_+_)

diff --git a/src/Cat/Abelian/Base.lagda.md b/src/Cat/Abelian/Base.lagda.md
@@ -1,13 +1,11 @@
 <!--
 ```agda
 open import Algebra.Group.Ab.Tensor
-open import Algebra.Magma.Unital
 open import Algebra.Group.Ab
 open import Algebra.Prelude
 open import Algebra.Monoid
 open import Algebra.Group
 
-open import Cat.Displayed.Univalence.Thin
 open import Cat.Diagram.Equaliser.Kernel
 
 import Algebra.Group.Cat.Base as Grp

diff --git a/src/Cat/Abelian/Instances/Ab.lagda.md b/src/Cat/Abelian/Instances/Ab.lagda.md
@@ -3,19 +3,11 @@
 open import Algebra.Group.Cat.FinitelyComplete
 open import Algebra.Group.Cat.Base
 open import Algebra.Group.Subgroup
-open import Algebra.Group.Ab.Free
 open import Algebra.Group.Ab.Sum
 open import Algebra.Group.Ab
-open import Algebra.Group
 
-open import Cat.Functor.Adjoint.Continuous
-open import Cat.Diagram.Equaliser.Kernel
-open import Cat.Functor.FullSubcategory
-open import Cat.Diagram.Coequaliser
 open import Cat.Diagram.Equaliser
-open import Cat.Diagram.Terminal
 open import Cat.Diagram.Product
-open import Cat.Functor.Adjoint
 open import Cat.Abelian.Base
 open import Cat.Prelude
 ```
@@ -30,9 +22,7 @@ module Cat.Abelian.Instances.Ab {ℓ} where
 open is-additive.Coequaliser
 open is-additive.Terminal
 open is-pre-abelian
-open Ab-category
 open is-additive
-open make-group
 ```
 -->
 

diff --git a/src/Cat/Allegory/Base.lagda.md b/src/Cat/Allegory/Base.lagda.md
@@ -1,8 +1,6 @@
 <!--
 ```agda
 open import Cat.Prelude
-
-import Cat.Reasoning as Cr
 ```
 -->
 

diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md
@@ -1,10 +1,8 @@
 <!--
 ```agda
 open import 1Lab.Reflection.Record
-open import 1Lab.Equiv.Fibrewise
 open import 1Lab.HLevel.Retracts
 open import 1Lab.HLevel.Universe
-open import 1Lab.Univalence
 open import 1Lab.Rewrite
 open import 1Lab.HLevel
 open import 1Lab.Equiv

diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md
@@ -4,7 +4,6 @@ open import Cat.Functor.Naturality
 open import Cat.Instances.Product
 open import Cat.Functor.Compose renaming (_◆_ to _◇_)
 open import Cat.Functor.Base
-open import Cat.Functor.Hom
 open import Cat.Prelude
 
 import Cat.Functor.Bifunctor as Bi

diff --git a/src/Cat/Bi/Diagram/Adjunction.lagda.md b/src/Cat/Bi/Diagram/Adjunction.lagda.md
@@ -2,9 +2,6 @@
 ```agda
 open import Cat.Bi.Base
 open import Cat.Prelude
-
-import Cat.Diagram.Monad as Cat
-import Cat.Reasoning as Cr
 ```
 -->
 

diff --git a/src/Cat/Bi/Instances/Relations.lagda.md b/src/Cat/Bi/Instances/Relations.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 {-# OPTIONS --lossy-unification -vtc.def:20 #-}
 open import Cat.Diagram.Pullback.Properties
-open import Cat.Diagram.Product.Solver
 open import Cat.Morphism.Factorisation
 open import Cat.Morphism.StrongEpi
 open import Cat.Instances.Functor

diff --git a/src/Cat/Diagram/Coend/Sets.lagda.md b/src/Cat/Diagram/Coend/Sets.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import Cat.Instances.Functor
 open import Cat.Instances.Product
-open import Cat.Instances.Sets
 open import Cat.Diagram.Coend
 open import Cat.Prelude
 

diff --git a/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md b/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import Cat.Diagram.Coequaliser
 open import Cat.Diagram.Pullback
-open import Cat.Diagram.Initial
 open import Cat.Prelude
 
 import Cat.Reasoning

diff --git a/src/Cat/Diagram/Colimit/Cocone.lagda.md b/src/Cat/Diagram/Colimit/Cocone.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Cat.Diagram.Colimit.Base
-open import Cat.Instances.Functor
 open import Cat.Diagram.Initial
 open import Cat.Prelude
 
@@ -36,8 +35,8 @@ commutes".
 ```agda
 module _ {J : Precategory o ℓ} {C : Precategory o′ ℓ′} (F : Functor J C) where
   private
-    import Cat.Reasoning J as J
-    import Cat.Reasoning C as C
+    module C = Cat.Reasoning C
+    module J = Precategory J
     module F = Functor F
 ```
 -->

diff --git a/src/Cat/Diagram/Colimit/Coproduct.lagda.md b/src/Cat/Diagram/Colimit/Coproduct.lagda.md
@@ -12,8 +12,6 @@ open import Cat.Diagram.Colimit.Base
 open import Cat.Instances.Discrete
 open import Cat.Functor.Kan.Base
 open import Cat.Prelude
-
-open import Data.Bool
 ```
 -->
 

diff --git a/src/Cat/Diagram/Colimit/Representable.lagda.md b/src/Cat/Diagram/Colimit/Representable.lagda.md
@@ -2,9 +2,7 @@
 ```agda
 open import Cat.Functor.Hom.Representable
 open import Cat.Instances.Shape.Terminal
-open import Cat.Instances.Sets.Complete
 open import Cat.Diagram.Colimit.Base
-open import Cat.Diagram.Limit.Base
 open import Cat.Instances.Functor
 open import Cat.Functor.Kan.Base
 open import Cat.Functor.Compose

diff --git a/src/Cat/Diagram/Coproduct/Indexed.lagda.md b/src/Cat/Diagram/Coproduct/Indexed.lagda.md
@@ -1,9 +1,7 @@
 <!--
 ```agda
 open import Cat.Instances.Shape.Terminal
-open import Cat.Instances.Discrete
 open import Cat.Diagram.Pullback
-open import Cat.Functor.Kan.Base
 open import Cat.Diagram.Initial
 open import Cat.Univalent
 open import Cat.Prelude

diff --git a/src/Cat/Diagram/Duals.lagda.md b/src/Cat/Diagram/Duals.lagda.md
@@ -1,10 +1,6 @@
 <!--
 ```agda
-open import Cat.Instances.Functor.Duality
-open import Cat.Instances.Functor
 open import Cat.Prelude
-
-import Cat.Reasoning
 ```
 -->
 
@@ -14,7 +10,7 @@ module Cat.Diagram.Duals {o h} (C : Precategory o h) where
 
 <!--
 ```agda
-import Cat.Reasoning C as C
+private module C = Precategory C
 ```
 -->
 

diff --git a/src/Cat/Diagram/Image.lagda.md b/src/Cat/Diagram/Image.lagda.md
@@ -5,7 +5,6 @@ open import Cat.Diagram.Initial
 open import Cat.Functor.Adjoint
 open import Cat.Instances.Comma
 open import Cat.Instances.Slice
-open import Cat.Functor.Base
 open import Cat.Prelude
 
 import Cat.Reasoning

diff --git a/src/Cat/Diagram/Initial.lagda.md b/src/Cat/Diagram/Initial.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import Cat.Univalent
 open import Cat.Prelude
 ```
 -->

diff --git a/src/Cat/Diagram/Limit/Base.lagda.md b/src/Cat/Diagram/Limit/Base.lagda.md
@@ -7,7 +7,6 @@ open import Cat.Functor.Naturality
 open import Cat.Diagram.Equaliser
 open import Cat.Functor.Coherence
 open import Cat.Functor.Kan.Base
-open import Cat.Instances.Lift
 open import Cat.Functor.Base
 open import Cat.Prelude
 

diff --git a/src/Cat/Diagram/Limit/Cone.lagda.md b/src/Cat/Diagram/Limit/Cone.lagda.md
@@ -7,7 +7,6 @@ open import Cat.Diagram.Terminal
 open import Cat.Functor.Kan.Base
 open import Cat.Prelude
 
-import Cat.Functor.Reasoning as Func
 import Cat.Reasoning
 ```
 -->

diff --git a/src/Cat/Diagram/Limit/Equaliser.lagda.md b/src/Cat/Diagram/Limit/Equaliser.lagda.md
@@ -4,11 +4,8 @@ open import Cat.Instances.Shape.Parallel
 open import Cat.Instances.Shape.Terminal
 open import Cat.Diagram.Limit.Base
 open import Cat.Diagram.Equaliser
-open import Cat.Instances.Functor
 open import Cat.Functor.Kan.Base
 open import Cat.Prelude
-
-open import Data.Bool
 ```
 -->
 

diff --git a/src/Cat/Diagram/Limit/Finite.lagda.md b/src/Cat/Diagram/Limit/Finite.lagda.md
@@ -21,7 +21,6 @@ open import Cat.Finite
 
 open import Data.Fin.Finite
 open import Data.Bool
-open import Data.Sum
 
 import Cat.Reasoning as Cat
 

diff --git a/src/Cat/Diagram/Limit/Pullback.lagda.md b/src/Cat/Diagram/Limit/Pullback.lagda.md
@@ -3,12 +3,9 @@
 open import Cat.Instances.Shape.Cospan
 open import Cat.Diagram.Limit.Base
 open import Cat.Diagram.Limit.Cone
-open import Cat.Instances.Functor
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Terminal
 open import Cat.Prelude
-
-open import Data.Bool
 ```
 -->
 

diff --git a/src/Cat/Diagram/Limit/Terminal.lagda.md b/src/Cat/Diagram/Limit/Terminal.lagda.md
@@ -20,7 +20,7 @@ module Cat.Diagram.Limit.Terminal {o h} (C : Precategory o h) where
 
 <!--
 ```agda
-open import Cat.Reasoning C
+open Precategory C
 
 open Terminal
 open Functor