diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
index 3c86822ae..75f6cceb1 100644
--- 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
index c64055ad4..12e2a3bbe 100644
--- 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
index 164b17e7e..43239d9b0 100644
--- 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
index 6c7bdb669..345575762 100644
--- 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
index dd58bc097..860d34072 100644
--- 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
index edd62a037..d74a7a7fb 100644
--- 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
index 4133cc79a..a5f173b14 100644
--- 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
index 6df19d576..afe31d41a 100644
--- 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
index 48b886535..0950d9826 100644
--- 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
index 850b8dcbe..1243b3a6a 100644
--- 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
index f104486de..595342eef 100644
--- 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
index c216119a4..e12a53606 100644
--- 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
index 2e11956d3..5f91b2345 100644
--- 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
index 274dba9a7..c5673ba9d 100644
--- 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
index 59e0b4991..6eb6901ca 100644
--- 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
index ba123f963..8dbbca38f 100644
--- 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
index 09f2f7d23..4564016b9 100644
--- 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
index 9f8a238a2..957239d9f 100644
--- 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
index 7452d042a..e9b616062 100644
--- 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
index 9ecd85d31..0170e8779 100644
--- 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
index a4c509518..41302b582 100644
--- 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
index af9e99d9b..3b0c0d463 100644
--- 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
index f1494588a..154566e70 100644
--- 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
index 5165eec9e..fa5e89d36 100644
--- 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
index 92ee94d0d..8de39f2cc 100644
--- 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
index 69e032a79..12a7f959c 100644
--- 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
index f438a98c5..0d9a58a9d 100644
--- 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
index c428d16d1..4605068b7 100644
--- 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
index a3a5f44e7..11a26adbf 100644
--- 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
index d7d4d4621..7c0a7e69a 100644
--- 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
index 3cfaa575b..01741ef13 100644
--- 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
index d01cbbd97..839263964 100644
--- 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
index 9852a7220..ab17873ce 100644
--- 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
index 0dc8ac0ef..fe26ac8ff 100644
--- 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
index 329b953d8..739e5570d 100644
--- 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
index df4e8c578..8e6f2942f 100644
--- 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
index 9a29b24c6..9b9afec6b 100644
--- 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
index e34567032..2779e5e1e 100644
--- 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
diff --git a/src/Cat/Diagram/Monad/Codensity.lagda.md b/src/Cat/Diagram/Monad/Codensity.lagda.md
index 55c377cc8..2f64abb8c 100644
--- a/src/Cat/Diagram/Monad/Codensity.lagda.md
+++ b/src/Cat/Diagram/Monad/Codensity.lagda.md
@@ -3,7 +3,6 @@
 open import Cat.Instances.Functor
 open import Cat.Functor.Kan.Base
 open import Cat.Diagram.Monad
-open import Cat.Functor.Base
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Func
diff --git a/src/Cat/Diagram/Product/Finite.lagda.md b/src/Cat/Diagram/Product/Finite.lagda.md
index 6e61f8916..a35d09e56 100644
--- a/src/Cat/Diagram/Product/Finite.lagda.md
+++ b/src/Cat/Diagram/Product/Finite.lagda.md
@@ -1,8 +1,6 @@
 <!--
 ```agda
 open import Cat.Diagram.Product.Indexed
-open import Cat.Diagram.Limit.Base
-open import Cat.Diagram.Equaliser
 open import Cat.Diagram.Terminal
 open import Cat.Diagram.Product
 open import Cat.Prelude
diff --git a/src/Cat/Diagram/Product/Indexed.lagda.md b/src/Cat/Diagram/Product/Indexed.lagda.md
index ff9e91b17..a8f0400e0 100644
--- a/src/Cat/Diagram/Product/Indexed.lagda.md
+++ b/src/Cat/Diagram/Product/Indexed.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Cat.Instances.Shape.Terminal
-open import Cat.Functor.Kan.Base
 open import Cat.Univalent
 open import Cat.Prelude
 ```
diff --git a/src/Cat/Diagram/Pullback.lagda.md b/src/Cat/Diagram/Pullback.lagda.md
index 6eb2a11bd..c3d0cbd56 100644
--- a/src/Cat/Diagram/Pullback.lagda.md
+++ b/src/Cat/Diagram/Pullback.lagda.md
@@ -12,7 +12,7 @@ module Cat.Diagram.Pullback {ℓ ℓ′} (C : Precategory ℓ ℓ′) where
 
 <!--
 ```agda
-open import Cat.Reasoning C
+open Precategory C
 private variable
   P′ X Y Z : Ob
   h p₁' p₂' : Hom X Y
diff --git a/src/Cat/Diagram/Pushout.lagda.md b/src/Cat/Diagram/Pushout.lagda.md
index b19366ff0..297d8b72b 100644
--- a/src/Cat/Diagram/Pushout.lagda.md
+++ b/src/Cat/Diagram/Pushout.lagda.md
@@ -13,7 +13,7 @@ module Cat.Diagram.Pushout {o ℓ} (C : Precategory o ℓ) where
 
 <!--
 ```agda
-open import Cat.Reasoning C
+open Precategory C
 private variable
   Q X Y Z : Ob
   h i₁′ i₂′ : Hom X Y
diff --git a/src/Cat/Diagram/Zero.lagda.md b/src/Cat/Diagram/Zero.lagda.md
index 4c5eedea3..bc17b0369 100644
--- a/src/Cat/Diagram/Zero.lagda.md
+++ b/src/Cat/Diagram/Zero.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import Cat.Univalent
 open import Cat.Prelude
 ```
 -->
diff --git a/src/Cat/Displayed/Cartesian/Discrete.lagda.md b/src/Cat/Displayed/Cartesian/Discrete.lagda.md
index 8a6dab78e..6ce93592f 100644
--- a/src/Cat/Displayed/Cartesian/Discrete.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Discrete.lagda.md
@@ -14,9 +14,7 @@ open import Cat.Displayed.Base
 open import Cat.Displayed.Path
 open import Cat.Prelude
 
-import Cat.Displayed.Reasoning
 import Cat.Displayed.Morphism
-import Cat.Reasoning
 ```
 -->
 
@@ -62,10 +60,10 @@ maps $x' \to_f y'$.
 ```agda
 module _ {o ℓ o′ ℓ′} {B : Precategory o ℓ} (E : Displayed B o′ ℓ′) where
   private
-    module B = Cat.Reasoning B
+    module B = Precategory B
     module E = Displayed E
     open Cat.Displayed.Morphism E
-    open Cat.Displayed.Reasoning E
+    open Displayed E
 ```
 
 -->
diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
index d9151536e..ec7590bda 100644
--- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
@@ -1,13 +1,11 @@
 <!--
 ```agda
 {-# OPTIONS --lossy-unification #-}
-open import Cat.Bi.Instances.Discrete
 open import Cat.Displayed.Cartesian
 open import Cat.Instances.Discrete
 open import Cat.Instances.Functor
 open import Cat.Displayed.Fibre
 open import Cat.Displayed.Base
-open import Cat.Bi.Base
 open import Cat.Prelude
 
 import Cat.Displayed.Fibre.Reasoning
@@ -228,7 +226,7 @@ base-change-square-ni {σ = σ} {δ = δ} {γ = γ} {τ = τ} p =
   to-natural-iso ni where
 
   open make-natural-iso
-  ni : make-natural-iso _ _ 
+  ni : make-natural-iso _ _
   ni .eta = base-change-square p
   ni .inv = base-change-square (sym p)
   ni .eta∘inv x = from-pathp $ base-change-square-inv p x
diff --git a/src/Cat/Displayed/Cartesian/Street.lagda.md b/src/Cat/Displayed/Cartesian/Street.lagda.md
index a6b05ac96..e1861ad4c 100644
--- a/src/Cat/Displayed/Cartesian/Street.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Street.lagda.md
@@ -1,8 +1,6 @@
 <!--
 ```agda
-open import Cat.Displayed.Cartesian
 open import Cat.Displayed.Fibre
-open import Cat.Displayed.Total
 open import Cat.Displayed.Base
 open import Cat.Prelude
 
@@ -17,9 +15,6 @@ module Cat.Displayed.Cartesian.Street where
 
 <!--
 ```agda
-open Cartesian-fibration
-open Cartesian-lift
-open is-cartesian
 open Displayed
 ```
 -->
@@ -41,7 +36,7 @@ module _ {o ℓ o′ ℓ′} {E : Precategory o ℓ} {B : Precategory o′ ℓ
   private
     module E = Cat.Reasoning E
     module B = Cat.Reasoning B
-    module P = Cat.Functor.Reasoning P
+    module P = Functor P
   open B.HLevel-instance
   open E.HLevel-instance
 ```
diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
index a9d0e96ff..b57bdf9c3 100644
--- a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
+++ b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
@@ -1,13 +1,11 @@
 <!--
 ```agda
 open import Cat.Displayed.Cocartesian
-open import Cat.Instances.Functor
 open import Cat.Displayed.Fibre
 open import Cat.Displayed.Base
 open import Cat.Prelude
 
 import Cat.Displayed.Reasoning
-import Cat.Reasoning
 ```
 -->
 
@@ -21,7 +19,7 @@ module Cat.Displayed.Cocartesian.Indexing
 
 <!--
 ```agda
-open Cat.Reasoning ℬ
+open Precategory ℬ
 open Displayed ℰ
 open Cat.Displayed.Reasoning ℰ
 open Cocartesian-fibration opfibration
diff --git a/src/Cat/Displayed/Comprehension/Coproduct/Strong.lagda.md b/src/Cat/Displayed/Comprehension/Coproduct/Strong.lagda.md
index ea3ad29e4..8f7a019a9 100644
--- a/src/Cat/Displayed/Comprehension/Coproduct/Strong.lagda.md
+++ b/src/Cat/Displayed/Comprehension/Coproduct/Strong.lagda.md
@@ -1,16 +1,12 @@
 <!--
 ```agda
 open import Cat.Displayed.Comprehension.Coproduct
-open import Cat.Displayed.Cartesian.Indexing
 open import Cat.Displayed.Comprehension
-open import Cat.Displayed.Cocartesian
 open import Cat.Displayed.Cartesian
 open import Cat.Morphism.Orthogonal
-open import Cat.Displayed.Fibre
 open import Cat.Displayed.Base
 open import Cat.Prelude
 
-import Cat.Displayed.Reasoning
 import Cat.Reasoning
 ```
 -->
diff --git a/src/Cat/Displayed/Fibre.lagda.md b/src/Cat/Displayed/Fibre.lagda.md
index a4e9fd073..f19fe1aa6 100644
--- a/src/Cat/Displayed/Fibre.lagda.md
+++ b/src/Cat/Displayed/Fibre.lagda.md
@@ -5,7 +5,6 @@ open import Cat.Prelude
 
 import Cat.Displayed.Reasoning as Dr
 import Cat.Displayed.Solver as Ds
-import Cat.Reasoning as Cr
 ```
 -->
 
@@ -15,10 +14,10 @@ module Cat.Displayed.Fibre
   (E : Displayed B o′ ℓ′)
   where
 
+open Precategory B
 open Displayed E
 open Ds
 open Dr E
-open Cr B
 ```
 
 ## Fibre categories {defines="fibre-category fibre-categories"}
diff --git a/src/Cat/Displayed/Instances/Diagrams.lagda.md b/src/Cat/Displayed/Instances/Diagrams.lagda.md
index c8e103e7d..9d7c83a09 100644
--- a/src/Cat/Displayed/Instances/Diagrams.lagda.md
+++ b/src/Cat/Displayed/Instances/Diagrams.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import Cat.Displayed.Cartesian.Indexing
 open import Cat.Displayed.Instances.Pullback
 open import Cat.Displayed.Instances.Lifting
 open import Cat.Displayed.Cartesian
@@ -12,7 +11,6 @@ open import Cat.Displayed.Base
 open import Cat.Prelude
 
 import Cat.Displayed.Reasoning
-import Cat.Reasoning
 ```
 -->
 
@@ -23,7 +21,7 @@ module Cat.Displayed.Instances.Diagrams
   (E : Displayed B o' ℓ')
   where
 
-open Cat.Reasoning B
+open Precategory B
 open Displayed E
 open Cat.Displayed.Reasoning E
 open Functor
diff --git a/src/Cat/Displayed/Instances/Elements.lagda.md b/src/Cat/Displayed/Instances/Elements.lagda.md
index 6d667677a..ae812e633 100644
--- a/src/Cat/Displayed/Instances/Elements.lagda.md
+++ b/src/Cat/Displayed/Instances/Elements.lagda.md
@@ -16,7 +16,7 @@ module Cat.Displayed.Instances.Elements {o ℓ s} (B : Precategory o ℓ)
 
 <!--
 ```agda
-open import Cat.Reasoning B
+open Precategory B
 open Functor
 
 private
diff --git a/src/Cat/Displayed/Instances/Family.lagda.md b/src/Cat/Displayed/Instances/Family.lagda.md
index dfb558cf2..d837b69c0 100644
--- a/src/Cat/Displayed/Instances/Family.lagda.md
+++ b/src/Cat/Displayed/Instances/Family.lagda.md
@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Path.IdentitySystem.Strict
-
 open import Cat.Displayed.GenericObject
 open import Cat.Displayed.Cartesian
 open import Cat.Functor.Equivalence
@@ -10,7 +8,6 @@ open import Cat.Instances.Discrete
 open import Cat.Instances.Functor
 open import Cat.Displayed.Fibre
 open import Cat.Displayed.Base
-open import Cat.Univalent
 open import Cat.Skeletal
 open import Cat.Prelude
 open import Cat.Strict
diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md
index 20ec1880b..30acc0b23 100644
--- a/src/Cat/Displayed/Instances/Lifting.lagda.md
+++ b/src/Cat/Displayed/Instances/Lifting.lagda.md
@@ -9,7 +9,6 @@ open import Cat.Displayed.Base
 open import Cat.Prelude
 
 import Cat.Displayed.Reasoning
-import Cat.Functor.Reasoning
 import Cat.Reasoning
 ```
 -->
@@ -361,8 +360,8 @@ When $\cE$ is a fibration, then so is the displayed category of liftings.
     : (fib : Cartesian-fibration E)
     → Cartesian-fibration Liftings
   Liftings-fibration fib .Cartesian-fibration.has-lift {F} {G} α G' = cart-lift where
-    module F = Cat.Functor.Reasoning F
-    module G = Cat.Functor.Reasoning G
+    module F = Functor F
+    module G = Functor G
     open Cartesian-fibration fib
     open Lifting
     open _=[_]=>l_
diff --git a/src/Cat/Displayed/InternalSum.lagda.md b/src/Cat/Displayed/InternalSum.lagda.md
index aa0db0e77..cebe2460d 100644
--- a/src/Cat/Displayed/InternalSum.lagda.md
+++ b/src/Cat/Displayed/InternalSum.lagda.md
@@ -1,14 +1,12 @@
 <!--
 ```agda
 open import Cat.Displayed.Instances.DisplayedFamilies
-open import Cat.Instances.Shape.Interval using (Arr)
-open import Cat.Displayed.Composition
-open import Cat.Displayed.Cartesian
+open import Cat.Displayed.Instances.Slice
 open import Cat.Displayed.Adjoint
 open import Cat.Displayed.Functor
-open import Cat.Instances.Slice
 open import Cat.Displayed.Base
 open import Cat.Prelude
+
 ```
 -->
 
@@ -20,9 +18,6 @@ module Cat.Displayed.InternalSum
 <!--
 ```agda
 open Precategory B
-
-open import Cat.Displayed.Instances.Slice B
-open import Cat.Displayed.Total
 ```
 -->
 
diff --git a/src/Cat/Displayed/Path.lagda.md b/src/Cat/Displayed/Path.lagda.md
index c499a1022..5af5213b3 100644
--- a/src/Cat/Displayed/Path.lagda.md
+++ b/src/Cat/Displayed/Path.lagda.md
@@ -3,7 +3,6 @@
 open import Cat.Functor.Equivalence.Path
 open import Cat.Functor.Equivalence
 open import Cat.Displayed.Functor
-open import Cat.Displayed.Total
 open import Cat.Displayed.Base
 open import Cat.Prelude
 ```
diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md
index cbbaae298..329d9b0d3 100644
--- a/src/Cat/Displayed/Reasoning.lagda.md
+++ b/src/Cat/Displayed/Reasoning.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import Cat.Instances.Functor
 open import Cat.Displayed.Base
 open import Cat.Prelude
 
diff --git a/src/Cat/Displayed/Solver.agda b/src/Cat/Displayed/Solver.agda
index 15cbb9874..55f673dd7 100644
--- a/src/Cat/Displayed/Solver.agda
+++ b/src/Cat/Displayed/Solver.agda
@@ -10,6 +10,7 @@ open import 1Lab.Prelude hiding (id; _∘_)
 
 open import Cat.Base
 open import Cat.Displayed.Base
+
 import Cat.Solver
 
 import Cat.Displayed.Reasoning as Dr
diff --git a/src/Cat/Displayed/Univalence.lagda.md b/src/Cat/Displayed/Univalence.lagda.md
index ecfbee92b..e6dcd47e9 100644
--- a/src/Cat/Displayed/Univalence.lagda.md
+++ b/src/Cat/Displayed/Univalence.lagda.md
@@ -3,7 +3,6 @@
 open import Cat.Displayed.Fibre
 open import Cat.Displayed.Total
 open import Cat.Displayed.Base
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Displayed.Reasoning
@@ -25,11 +24,9 @@ module Cat.Displayed.Univalence
 private
   module B = Cat.Reasoning B
   module ∫E = Cat.Reasoning (∫ E)
-  module E = Cat.Displayed.Reasoning E
 open Cat.Displayed.Morphism E
 open Displayed E
 open Total-hom
-open E
 ```
 -->
 
diff --git a/src/Cat/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md
index 6e6a08085..f455a4c81 100644
--- a/src/Cat/Displayed/Univalence/Thin.lagda.md
+++ b/src/Cat/Displayed/Univalence/Thin.lagda.md
@@ -5,11 +5,9 @@ open import 1Lab.Equiv.Embedding
 
 open import Cat.Displayed.Univalence
 open import Cat.Functor.Properties
-open import Cat.Displayed.Fibre
 open import Cat.Displayed.Total
 open import Cat.Displayed.Base
 open import Cat.Instances.Sets
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Displayed.Morphism
diff --git a/src/Cat/Functor/Adjoint/Continuous.lagda.md b/src/Cat/Functor/Adjoint/Continuous.lagda.md
index 75d837b44..f072049db 100644
--- a/src/Cat/Functor/Adjoint/Continuous.lagda.md
+++ b/src/Cat/Functor/Adjoint/Continuous.lagda.md
@@ -8,19 +8,12 @@ open import Cat.Diagram.Colimit.Base
 open import Cat.Diagram.Limit.Finite
 open import Cat.Functor.Adjoint.Kan
 open import Cat.Diagram.Limit.Base
-open import Cat.Instances.Functor
 open import Cat.Diagram.Terminal
 open import Cat.Functor.Kan.Base
-open import Cat.Diagram.Initial
 open import Cat.Functor.Adjoint
-open import Cat.Diagram.Duals
-open import Cat.Functor.Base
 open import Cat.Prelude
 
-open import Data.Bool
-
 import Cat.Functor.Reasoning as Func
-import Cat.Reasoning as Cat
 ```
 -->
 
@@ -38,8 +31,8 @@ module _
   private
     module L = Func L
     module R = Func R
-    module C = Cat C
-    module D = Cat D
+    module C = Precategory C
+    module D = Precategory D
     module adj = _⊣_ L⊣R
     open _=>_
 ```
diff --git a/src/Cat/Functor/Adjoint/Kan.lagda.md b/src/Cat/Functor/Adjoint/Kan.lagda.md
index 1bacbf56e..ef8f41b20 100644
--- a/src/Cat/Functor/Adjoint/Kan.lagda.md
+++ b/src/Cat/Functor/Adjoint/Kan.lagda.md
@@ -5,7 +5,6 @@ open import Cat.Functor.Coherence
 open import Cat.Instances.Functor
 open import Cat.Functor.Kan.Base
 open import Cat.Functor.Adjoint
-open import Cat.Functor.Base
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Fr
diff --git a/src/Cat/Functor/Adjoint/Mate.lagda.md b/src/Cat/Functor/Adjoint/Mate.lagda.md
index b76efbd0e..783cbcdf2 100644
--- a/src/Cat/Functor/Adjoint/Mate.lagda.md
+++ b/src/Cat/Functor/Adjoint/Mate.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import Cat.Instances.Functor
 open import Cat.Functor.Adjoint
 open import Cat.Prelude
 
diff --git a/src/Cat/Functor/Adjoint/Unique.lagda.md b/src/Cat/Functor/Adjoint/Unique.lagda.md
index 0a665cd91..f31e6740b 100644
--- a/src/Cat/Functor/Adjoint/Unique.lagda.md
+++ b/src/Cat/Functor/Adjoint/Unique.lagda.md
@@ -5,7 +5,6 @@ open import Cat.Functor.Naturality
 open import Cat.Functor.Univalence
 open import Cat.Functor.Adjoint
 open import Cat.Functor.Base
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Fr
diff --git a/src/Cat/Functor/Closed.lagda.md b/src/Cat/Functor/Closed.lagda.md
index be67bdeb3..884a0dad5 100644
--- a/src/Cat/Functor/Closed.lagda.md
+++ b/src/Cat/Functor/Closed.lagda.md
@@ -1,12 +1,9 @@
 <!--
 ```agda
-open import 1Lab.Path.Cartesian
-
 open import Cat.Instances.Product
 open import Cat.Functor.Base
 open import Cat.Prelude
 
-import Cat.Functor.Reasoning as Fr
 import Cat.Reasoning
 
 open Precategory
diff --git a/src/Cat/Functor/Conservative.lagda.md b/src/Cat/Functor/Conservative.lagda.md
index 865d73dc1..158d01c42 100644
--- a/src/Cat/Functor/Conservative.lagda.md
+++ b/src/Cat/Functor/Conservative.lagda.md
@@ -1,8 +1,6 @@
 <!--
 ```agda
 open import Cat.Diagram.Limit.Base
-open import Cat.Diagram.Terminal
-open import Cat.Functor.Base
 open import Cat.Morphism
 open import Cat.Prelude hiding (J)
 
diff --git a/src/Cat/Functor/Dense.lagda.md b/src/Cat/Functor/Dense.lagda.md
index c7b1c694c..a0d881b59 100644
--- a/src/Cat/Functor/Dense.lagda.md
+++ b/src/Cat/Functor/Dense.lagda.md
@@ -8,7 +8,6 @@ open import Cat.Instances.Comma
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Fr
-import Cat.Reasoning as Cr
 ```
 -->
 
@@ -45,8 +44,8 @@ module
   open _=>_
 
   private
-    module C = Cr C
-    module D = Cr D
+    module C = Precategory C
+    module D = Precategory D
     module F = Fr F
 ```
 -->
diff --git a/src/Cat/Functor/Equivalence.lagda.md b/src/Cat/Functor/Equivalence.lagda.md
index 1d98ecb80..bd379bb8a 100644
--- a/src/Cat/Functor/Equivalence.lagda.md
+++ b/src/Cat/Functor/Equivalence.lagda.md
@@ -4,7 +4,6 @@ open import Cat.Functor.Naturality
 open import Cat.Functor.Properties
 open import Cat.Functor.Adjoint
 open import Cat.Functor.Base
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Fr
diff --git a/src/Cat/Functor/Equivalence/Complete.lagda.md b/src/Cat/Functor/Equivalence/Complete.lagda.md
index 7114ee7e6..db0659334 100644
--- a/src/Cat/Functor/Equivalence/Complete.lagda.md
+++ b/src/Cat/Functor/Equivalence/Complete.lagda.md
@@ -4,7 +4,6 @@ open import Cat.Functor.Adjoint.Continuous
 open import Cat.Functor.Equivalence
 open import Cat.Diagram.Limit.Base
 open import Cat.Instances.Functor
-open import Cat.Functor.Base
 open import Cat.Prelude
 ```
 -->
diff --git a/src/Cat/Functor/Equivalence/Path.lagda.md b/src/Cat/Functor/Equivalence/Path.lagda.md
index 52ae30b7c..53a6b1817 100644
--- a/src/Cat/Functor/Equivalence/Path.lagda.md
+++ b/src/Cat/Functor/Equivalence/Path.lagda.md
@@ -3,9 +3,6 @@
 open import Cat.Functor.Adjoint.Unique
 open import Cat.Functor.Equivalence
 open import Cat.Instances.Functor
-open import Cat.Functor.Adjoint
-open import Cat.Functor.Base
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Fr
@@ -261,7 +258,7 @@ module
     open is-equivalence eqv
     module C = Cat.Reasoning C
     module D = Cat.Reasoning D
-    module F = Fr F
+    module F = Functor F
   open _=>_
 
 ```
diff --git a/src/Cat/Functor/FullSubcategory.lagda.md b/src/Cat/Functor/FullSubcategory.lagda.md
index def893b43..455c4fa65 100644
--- a/src/Cat/Functor/FullSubcategory.lagda.md
+++ b/src/Cat/Functor/FullSubcategory.lagda.md
@@ -1,8 +1,6 @@
 <!--
 ```agda
 open import Cat.Functor.Properties
-open import Cat.Functor.Base
-open import Cat.Univalent
 open import Cat.Prelude
 ```
 -->
diff --git a/src/Cat/Functor/Hom.lagda.md b/src/Cat/Functor/Hom.lagda.md
index 473e77334..28917269e 100644
--- a/src/Cat/Functor/Hom.lagda.md
+++ b/src/Cat/Functor/Hom.lagda.md
@@ -2,8 +2,6 @@
 ```agda
 open import Cat.Functor.Properties
 open import Cat.Instances.Product
-open import Cat.Diagram.Initial
-open import Cat.Functor.Compose
 open import Cat.Functor.Closed
 open import Cat.Functor.Base
 open import Cat.Prelude
diff --git a/src/Cat/Functor/Hom/Cocompletion.lagda.md b/src/Cat/Functor/Hom/Cocompletion.lagda.md
index d89b1a4c8..98551863a 100644
--- a/src/Cat/Functor/Hom/Cocompletion.lagda.md
+++ b/src/Cat/Functor/Hom/Cocompletion.lagda.md
@@ -6,9 +6,6 @@ open import Cat.Instances.Functor
 open import Cat.Functor.Kan.Base
 open import Cat.Functor.Hom
 open import Cat.Prelude
-
-import Cat.Functor.Reasoning as Func
-import Cat.Reasoning
 ```
 -->
 
@@ -23,11 +20,10 @@ module
 <!--
 ```agda
 private
-  module C = Cat.Reasoning C
-  module D = Cat.Reasoning D
+  module C = Precategory C
+  module D = Precategory D
 open import Cat.Morphism Cat[ C , D ] using (_≅_)
 
-open Func
 open _=>_
 ```
 -->
diff --git a/src/Cat/Functor/Hom/Displayed.lagda.md b/src/Cat/Functor/Hom/Displayed.lagda.md
index 0150361cb..255994b21 100644
--- a/src/Cat/Functor/Hom/Displayed.lagda.md
+++ b/src/Cat/Functor/Hom/Displayed.lagda.md
@@ -3,7 +3,6 @@
 open import Cat.Instances.Product
 open import Cat.Displayed.Solver
 open import Cat.Displayed.Fibre
-open import Cat.Displayed.Total
 open import Cat.Displayed.Base
 open import Cat.Prelude
 
diff --git a/src/Cat/Functor/Hom/Representable.lagda.md b/src/Cat/Functor/Hom/Representable.lagda.md
index afe84fa0b..e6d2b5fae 100644
--- a/src/Cat/Functor/Hom/Representable.lagda.md
+++ b/src/Cat/Functor/Hom/Representable.lagda.md
@@ -4,13 +4,11 @@
 open import Cat.Univalent.Instances.Opposite
 open import Cat.Diagram.Colimit.Base
 open import Cat.Diagram.Limit.Base
-open import Cat.Functor.Kan.Unique
 open import Cat.Functor.Properties
 open import Cat.Instances.Elements
 open import Cat.Instances.Functor
 open import Cat.Diagram.Terminal
 open import Cat.Morphism.Duality
-open import Cat.Instances.Sets
 open import Cat.Functor.Hom
 open import Cat.Prelude
 
diff --git a/src/Cat/Functor/Kan/Base.lagda.md b/src/Cat/Functor/Kan/Base.lagda.md
index 44b1228b9..c60693d06 100644
--- a/src/Cat/Functor/Kan/Base.lagda.md
+++ b/src/Cat/Functor/Kan/Base.lagda.md
@@ -3,7 +3,6 @@
 open import Cat.Instances.Shape.Terminal
 open import Cat.Functor.Coherence
 open import Cat.Instances.Functor
-open import Cat.Functor.Compose
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Func
diff --git a/src/Cat/Functor/Properties.lagda.md b/src/Cat/Functor/Properties.lagda.md
index 0b3ea98a2..80eccff9d 100644
--- a/src/Cat/Functor/Properties.lagda.md
+++ b/src/Cat/Functor/Properties.lagda.md
@@ -208,8 +208,6 @@ module _ {C : Precategory o h} {D : Precategory o₁ h₁} where
     open _≅_ public
     open Inverses public
 
-  open import Cat.Univalent
-
   is-ff→F-map-iso-is-equiv
     : {F : Functor C D} → is-fully-faithful F
     → ∀ {X Y} → is-equiv (F-map-iso {x = X} {Y} F)
diff --git a/src/Cat/Functor/WideSubcategory.lagda.md b/src/Cat/Functor/WideSubcategory.lagda.md
index 2d217bb6a..dc7a28e92 100644
--- a/src/Cat/Functor/WideSubcategory.lagda.md
+++ b/src/Cat/Functor/WideSubcategory.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Cat.Functor.Properties
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Reasoning
diff --git a/src/Cat/Gaunt.lagda.md b/src/Cat/Gaunt.lagda.md
index 29b8f85c4..90c7605e0 100644
--- a/src/Cat/Gaunt.lagda.md
+++ b/src/Cat/Gaunt.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import 1Lab.Path.IdentitySystem.Strict
 
-open import Cat.Univalent
 open import Cat.Skeletal
 open import Cat.Prelude
 open import Cat.Strict
diff --git a/src/Cat/Instances/Comma.lagda.md b/src/Cat/Instances/Comma.lagda.md
index 6b7d82614..1b344769f 100644
--- a/src/Cat/Instances/Comma.lagda.md
+++ b/src/Cat/Instances/Comma.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Cat.Instances.Shape.Terminal
-open import Cat.Instances.Functor
 open import Cat.Prelude
 ```
 -->
diff --git a/src/Cat/Instances/Comma/Univalent.lagda.md b/src/Cat/Instances/Comma/Univalent.lagda.md
index e67547b3a..d8d51e0b1 100644
--- a/src/Cat/Instances/Comma/Univalent.lagda.md
+++ b/src/Cat/Instances/Comma/Univalent.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import Cat.Instances.Comma
 open import Cat.Functor.Base
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Func
diff --git a/src/Cat/Instances/Core.lagda.md b/src/Cat/Instances/Core.lagda.md
index c81cd460f..87ebb137a 100644
--- a/src/Cat/Instances/Core.lagda.md
+++ b/src/Cat/Instances/Core.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import Cat.Functor.WideSubcategory
 open import Cat.Instances.Functor
-open import Cat.Functor.Base
 open import Cat.Groupoid
 open import Cat.Prelude
 
diff --git a/src/Cat/Instances/Delooping.lagda.md b/src/Cat/Instances/Delooping.lagda.md
index e7c5c4b51..31aa892e4 100644
--- a/src/Cat/Instances/Delooping.lagda.md
+++ b/src/Cat/Instances/Delooping.lagda.md
@@ -3,8 +3,6 @@
 open import Algebra.Monoid
 
 open import Cat.Prelude
-
-open import Data.List
 ```
 -->
 
diff --git a/src/Cat/Instances/Discrete.lagda.md b/src/Cat/Instances/Discrete.lagda.md
index 0e3ecb423..209a79bab 100644
--- a/src/Cat/Instances/Discrete.lagda.md
+++ b/src/Cat/Instances/Discrete.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import Cat.Univalent
 open import Cat.Prelude
 
 open import Data.Dec
diff --git a/src/Cat/Instances/Elements.lagda.md b/src/Cat/Instances/Elements.lagda.md
index af8bf222b..4a9370568 100644
--- a/src/Cat/Instances/Elements.lagda.md
+++ b/src/Cat/Instances/Elements.lagda.md
@@ -11,7 +11,7 @@ module Cat.Instances.Elements {o ℓ s} (C : Precategory o ℓ)
 
 <!--
 ```agda
-open import Cat.Reasoning C
+open Precategory C
 open Functor
 
 private
diff --git a/src/Cat/Instances/FinSet.lagda.md b/src/Cat/Instances/FinSet.lagda.md
index 4c131f702..08d37f787 100644
--- a/src/Cat/Instances/FinSet.lagda.md
+++ b/src/Cat/Instances/FinSet.lagda.md
@@ -3,8 +3,6 @@
 open import Cat.Prelude
 
 open import Data.Fin
-
-import Cat.Reasoning as Cat
 ```
 -->
 
diff --git a/src/Cat/Instances/Functor.lagda.md b/src/Cat/Instances/Functor.lagda.md
index 6d425c2ca..eb13b3f66 100644
--- a/src/Cat/Instances/Functor.lagda.md
+++ b/src/Cat/Instances/Functor.lagda.md
@@ -1,12 +1,8 @@
 <!--
 ```agda
-open import 1Lab.Path.Cartesian
-
 open import Cat.Instances.Product
-open import Cat.Univalent using (is-category)
 open import Cat.Prelude
 
-import Cat.Functor.Reasoning as Fr
 import Cat.Reasoning
 
 open Precategory
diff --git a/src/Cat/Instances/Functor/Duality.lagda.md b/src/Cat/Instances/Functor/Duality.lagda.md
index 40871d5b0..364fde17d 100644
--- a/src/Cat/Instances/Functor/Duality.lagda.md
+++ b/src/Cat/Instances/Functor/Duality.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import Cat.Functor.Equivalence
 open import Cat.Instances.Functor
-open import Cat.Functor.Base
 open import Cat.Prelude
 
 import Cat.Reasoning
diff --git a/src/Cat/Instances/InternalFunctor/Compose.lagda.md b/src/Cat/Instances/InternalFunctor/Compose.lagda.md
index 6de4c6f9e..53a81a090 100644
--- a/src/Cat/Instances/InternalFunctor/Compose.lagda.md
+++ b/src/Cat/Instances/InternalFunctor/Compose.lagda.md
@@ -6,7 +6,6 @@ open import Cat.Prelude
 import Cat.Instances.InternalFunctor
 import Cat.Internal.Reasoning
 import Cat.Internal.Base as Internal
-import Cat.Reasoning
 ```
 -->
 
@@ -29,7 +28,7 @@ composition of internal natural transformations.
 <!--
 ```agda
 module _ {o ℓ} {C : Precategory o ℓ} {𝔸 𝔹 ℂ : Internal.Internal-cat C} where
-  open Cat.Reasoning C
+  open Precategory C
   open Internal C
   open Internal-functor
   open _=>i_
@@ -95,7 +94,7 @@ With that out of the way, we can prove the main result.
 <!--
 ```agda
 module _ {o ℓ} {C : Precategory o ℓ} (𝔸 𝔹 ℂ : Internal.Internal-cat C) where
-  open Cat.Reasoning C
+  open Precategory C
   open Internal C
   open Cat.Instances.InternalFunctor C
   open Functor
diff --git a/src/Cat/Instances/OFE/Complete.lagda.md b/src/Cat/Instances/OFE/Complete.lagda.md
index fef981e4c..4bcbd8b4d 100644
--- a/src/Cat/Instances/OFE/Complete.lagda.md
+++ b/src/Cat/Instances/OFE/Complete.lagda.md
@@ -1,11 +1,8 @@
 <!--
 ```agda
-open import Cat.Displayed.Univalence.Thin
-open import Cat.Displayed.Total
 open import Cat.Instances.OFE
 open import Cat.Prelude
 
-open import Data.Nat.Properties
 open import Data.Nat.Order
 open import Data.Nat.Base
 ```
diff --git a/src/Cat/Instances/OFE/Discrete.lagda.md b/src/Cat/Instances/OFE/Discrete.lagda.md
index 53f175a87..b513e249e 100644
--- a/src/Cat/Instances/OFE/Discrete.lagda.md
+++ b/src/Cat/Instances/OFE/Discrete.lagda.md
@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import Cat.Displayed.Univalence.Thin
-open import Cat.Displayed.Total
 open import Cat.Instances.OFE
 open import Cat.Prelude
 ```
diff --git a/src/Cat/Instances/Poly.lagda.md b/src/Cat/Instances/Poly.lagda.md
index 27f31dc1b..0f11abf4d 100644
--- a/src/Cat/Instances/Poly.lagda.md
+++ b/src/Cat/Instances/Poly.lagda.md
@@ -6,10 +6,7 @@ open import Cat.Univalent.Instances.Opposite
 open import Cat.Displayed.Instances.Family
 open import Cat.Displayed.Univalence
 open import Cat.Instances.Discrete
-open import Cat.Instances.Functor
-open import Cat.Displayed.Fibre
 open import Cat.Displayed.Total
-open import Cat.Displayed.Base
 open import Cat.Instances.Sets
 open import Cat.Prelude
 
diff --git a/src/Cat/Instances/Product.lagda.md b/src/Cat/Instances/Product.lagda.md
index ff9ada4f5..c3418c3cc 100644
--- a/src/Cat/Instances/Product.lagda.md
+++ b/src/Cat/Instances/Product.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Cat.Functor.Base
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Reasoning
diff --git a/src/Cat/Instances/Sets/Complete.lagda.md b/src/Cat/Instances/Sets/Complete.lagda.md
index d4db7bc50..1a2507324 100644
--- a/src/Cat/Instances/Sets/Complete.lagda.md
+++ b/src/Cat/Instances/Sets/Complete.lagda.md
@@ -75,11 +75,11 @@ module _ {ℓ} where
   open import Cat.Diagram.Equaliser (Sets ℓ)
   open import Cat.Diagram.Pullback (Sets ℓ)
   open import Cat.Diagram.Product (Sets ℓ)
-  open import Cat.Reasoning (Sets ℓ)
+  open Precategory (Sets ℓ)
 
   private variable
     A B : Set ℓ
-    f g : Hom A B
+    f g : ⌞ A ⌟ → ⌞ B ⌟
 
   open Terminal
   open is-product
diff --git a/src/Cat/Instances/Shape/Isomorphism.lagda.md b/src/Cat/Instances/Shape/Isomorphism.lagda.md
index 19eddde6d..38f456cf0 100644
--- a/src/Cat/Instances/Shape/Isomorphism.lagda.md
+++ b/src/Cat/Instances/Shape/Isomorphism.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Cat.Instances.Functor
-open import Cat.Functor.Base
 open import Cat.Prelude
 
 open import Data.Bool
diff --git a/src/Cat/Instances/Slice.lagda.md b/src/Cat/Instances/Slice.lagda.md
index e837762c2..999b8ac6d 100644
--- a/src/Cat/Instances/Slice.lagda.md
+++ b/src/Cat/Instances/Slice.lagda.md
@@ -9,7 +9,6 @@ open import Cat.Instances.Functor
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Terminal
 open import Cat.Diagram.Product
-open import Cat.Univalent
 open import Cat.Prelude
 
 open import Data.Sum
diff --git a/src/Cat/Instances/StrictCat/Cohesive.lagda.md b/src/Cat/Instances/StrictCat/Cohesive.lagda.md
index 5d52d663a..8934ebb07 100644
--- a/src/Cat/Instances/StrictCat/Cohesive.lagda.md
+++ b/src/Cat/Instances/StrictCat/Cohesive.lagda.md
@@ -5,7 +5,6 @@ open import Cat.Instances.Discrete hiding (Disc)
 open import Cat.Instances.Functor
 open import Cat.Instances.Product
 open import Cat.Functor.Adjoint
-open import Cat.Univalent
 open import Cat.Prelude
 ```
 -->
diff --git a/src/Cat/Internal/Morphism.lagda.md b/src/Cat/Internal/Morphism.lagda.md
index 848cd55d0..202fc5357 100644
--- a/src/Cat/Internal/Morphism.lagda.md
+++ b/src/Cat/Internal/Morphism.lagda.md
@@ -5,7 +5,6 @@ open import Cat.Prelude
 
 import Cat.Internal.Reasoning
 import Cat.Internal.Base
-import Cat.Reasoning
 ```
 -->
 
@@ -18,7 +17,7 @@ module Cat.Internal.Morphism
 
 <!--
 ```agda
-open Cat.Reasoning C
+open Precategory C
 open Cat.Internal.Base C
 open Cat.Internal.Reasoning ℂ
 
diff --git a/src/Cat/Internal/Sets.lagda.md b/src/Cat/Internal/Sets.lagda.md
index 0b1fd6b51..fe80d9849 100644
--- a/src/Cat/Internal/Sets.lagda.md
+++ b/src/Cat/Internal/Sets.lagda.md
@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import Cat.Instances.StrictCat
-open import Cat.Instances.Sets
 open import Cat.Internal.Base
 open import Cat.Prelude
 
diff --git a/src/Cat/Monoidal/Instances/Cartesian.lagda.md b/src/Cat/Monoidal/Instances/Cartesian.lagda.md
index 209619e16..7bb8094d2 100644
--- a/src/Cat/Monoidal/Instances/Cartesian.lagda.md
+++ b/src/Cat/Monoidal/Instances/Cartesian.lagda.md
@@ -6,7 +6,6 @@ open import Cat.Diagram.Terminal
 open import Cat.Monoidal.Base
 open import Cat.Prelude
 
-import Cat.Functor.Bifunctor as Bifunctor
 import Cat.Diagram.Product
 import Cat.Reasoning as Cr
 ```
diff --git a/src/Cat/Morphism/Factorisation.lagda.md b/src/Cat/Morphism/Factorisation.lagda.md
index f9c33f869..b0577fa34 100644
--- a/src/Cat/Morphism/Factorisation.lagda.md
+++ b/src/Cat/Morphism/Factorisation.lagda.md
@@ -1,9 +1,6 @@
 <!--
 ```agda
-open import Cat.Functor.FullSubcategory
 open import Cat.Morphism.Orthogonal
-open import Cat.Diagram.Terminal
-open import Cat.Functor.Adjoint
 open import Cat.Prelude
 
 open import Data.Power
diff --git a/src/Cat/Morphism/StrongEpi.lagda.md b/src/Cat/Morphism/StrongEpi.lagda.md
index 0773003f3..7a946f76e 100644
--- a/src/Cat/Morphism/StrongEpi.lagda.md
+++ b/src/Cat/Morphism/StrongEpi.lagda.md
@@ -3,7 +3,6 @@
 open import Cat.Diagram.Coequaliser.RegularEpi
 open import Cat.Diagram.Pullback.Properties
 open import Cat.Functor.FullSubcategory
-open import Cat.Morphism.Factorisation
 open import Cat.Diagram.Limit.Finite
 open import Cat.Morphism.Orthogonal
 open import Cat.Diagram.Equaliser
diff --git a/src/Cat/Regular.lagda.md b/src/Cat/Regular.lagda.md
index 2d20e4b0e..b0f8132fb 100644
--- a/src/Cat/Regular.lagda.md
+++ b/src/Cat/Regular.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Cat.Diagram.Coequaliser.RegularEpi
-open import Cat.Diagram.Pullback.Properties
 open import Cat.Morphism.Factorisation
 open import Cat.Diagram.Limit.Finite
 open import Cat.Diagram.Coequaliser
@@ -10,9 +9,6 @@ open import Cat.Diagram.Pullback
 open import Cat.Diagram.Product
 open import Cat.Prelude
 
-open import Data.Power
-
-import Cat.Functor.Bifunctor as Bifunctor
 import Cat.Reasoning as Cr
 ```
 -->
diff --git a/src/Cat/Regular/Image.lagda.md b/src/Cat/Regular/Image.lagda.md
index a21ef3dc4..f8a9e7a1d 100644
--- a/src/Cat/Regular/Image.lagda.md
+++ b/src/Cat/Regular/Image.lagda.md
@@ -1,14 +1,12 @@
 <!--
 ```agda
 -- {-# OPTIONS --lossy-unification #-}
-open import Cat.Diagram.Pullback.Properties
 open import Cat.Functor.FullSubcategory
 open import Cat.Morphism.Factorisation
 open import Cat.Morphism.StrongEpi
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Product
 open import Cat.Instances.Slice
-open import Cat.Diagram.Image
 open import Cat.Prelude
 open import Cat.Regular
 
diff --git a/src/Cat/Regular/Slice.lagda.md b/src/Cat/Regular/Slice.lagda.md
index 3df6366ca..ad50f6f24 100644
--- a/src/Cat/Regular/Slice.lagda.md
+++ b/src/Cat/Regular/Slice.lagda.md
@@ -9,9 +9,6 @@ open import Cat.Instances.Slice
 open import Cat.Prelude
 open import Cat.Regular
 
-open import Data.Power
-
-import Cat.Functor.Bifunctor as Bifunctor
 import Cat.Reasoning as Cr
 ```
 -->
diff --git a/src/Cat/Restriction/Base.lagda.md b/src/Cat/Restriction/Base.lagda.md
index 315d253a0..57b572b6b 100644
--- a/src/Cat/Restriction/Base.lagda.md
+++ b/src/Cat/Restriction/Base.lagda.md
@@ -1,8 +1,6 @@
 <!--
 ```agda
 open import Cat.Prelude
-
-import Cat.Reasoning
 ```
 -->
 
@@ -53,7 +51,7 @@ record Restriction-category
   {o ℓ} (C : Precategory o ℓ)
   : Type (o ⊔ ℓ) where
   no-eta-equality
-  open Cat.Reasoning C
+  open Precategory C
   field
     _↓ : ∀ {x y} → Hom x y → Hom x x
 
diff --git a/src/Cat/Solver.lagda.md b/src/Cat/Solver.lagda.md
index e9bc725fa..5dcfdf5ed 100644
--- a/src/Cat/Solver.lagda.md
+++ b/src/Cat/Solver.lagda.md
@@ -6,7 +6,6 @@ open import 1Lab.Prelude hiding (id ; _∘_)
 
 open import Cat.Base
 
-open import Data.Bool
 open import Data.List
 ```
 -->
diff --git a/src/Cat/Strict.lagda.md b/src/Cat/Strict.lagda.md
index 55047dde3..f83c23650 100644
--- a/src/Cat/Strict.lagda.md
+++ b/src/Cat/Strict.lagda.md
@@ -1,8 +1,6 @@
 <!--
 ```agda
 open import Cat.Prelude
-
-import Cat.Reasoning
 ```
 -->
 
diff --git a/src/Cat/Strict/Reasoning.lagda.md b/src/Cat/Strict/Reasoning.lagda.md
index a7c41e92b..6b4bb9912 100644
--- a/src/Cat/Strict/Reasoning.lagda.md
+++ b/src/Cat/Strict/Reasoning.lagda.md
@@ -1,14 +1,12 @@
 ```agda
 open import Cat.Prelude
 
-import Cat.Reasoning
-
 module Cat.Strict.Reasoning
   {o ℓ} (C : Precategory o ℓ)
   (ob-set : is-set (Precategory.Ob C))
   where
 
-open Cat.Reasoning C
+open Precategory C
 ```
 
 # Reasoning with strict categories
diff --git a/src/Cat/Univalent.lagda.md b/src/Cat/Univalent.lagda.md
index 70a3fe7b9..74dbdbfc0 100644
--- a/src/Cat/Univalent.lagda.md
+++ b/src/Cat/Univalent.lagda.md
@@ -2,7 +2,6 @@
 ```
 open import 1Lab.Prelude hiding (_∘_ ; id)
 
-open import Cat.Solver
 open import Cat.Base
 
 import Cat.Reasoning
diff --git a/src/Cat/Univalent/Instances/Opposite.lagda.md b/src/Cat/Univalent/Instances/Opposite.lagda.md
index 605c48c88..e196c3a57 100644
--- a/src/Cat/Univalent/Instances/Opposite.lagda.md
+++ b/src/Cat/Univalent/Instances/Opposite.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import Cat.Univalent
 open import Cat.Prelude
 
 import Cat.Reasoning
diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md
index 731e362a5..cd1b4a968 100644
--- a/src/Data/Fin/Base.lagda.md
+++ b/src/Data/Fin/Base.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import 1Lab.Path.IdentitySystem
 open import 1Lab.HLevel.Retracts
-open import 1Lab.Type.Sigma
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
diff --git a/src/Data/Fin/Closure.lagda.md b/src/Data/Fin/Closure.lagda.md
index 04a4bd0d9..549473692 100644
--- a/src/Data/Fin/Closure.lagda.md
+++ b/src/Data/Fin/Closure.lagda.md
@@ -4,8 +4,6 @@ open import 1Lab.Prelude
 
 open import Data.Fin.Base
 open import Data.Sum
-
-open import Prim.Data.Maybe
 ```
 -->
 
@@ -48,7 +46,7 @@ Finite-one-is-contr .paths fzero = refl
 ```
 
 The successor operation on indices corresponds to taking coproducts with
-the unit set, which is concisely phrased using the `Maybe` type:
+the unit set.
 
 ```agda
 Finite-successor : Fin (suc n) ≃ (⊤ ⊎ Fin n)
diff --git a/src/Data/Fin/Finite.lagda.md b/src/Data/Fin/Finite.lagda.md
index 43b182379..5e3cdab74 100644
--- a/src/Data/Fin/Finite.lagda.md
+++ b/src/Data/Fin/Finite.lagda.md
@@ -10,8 +10,6 @@ open import Data.Fin.Base
 open import Data.Nat.Base
 open import Data.Dec
 open import Data.Sum
-
-open import Meta.Bind
 ```
 -->
 
diff --git a/src/Data/List.lagda.md b/src/Data/List.lagda.md
index f8d8c4f71..ccd0cfbff 100644
--- a/src/Data/List.lagda.md
+++ b/src/Data/List.lagda.md
@@ -8,7 +8,6 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Nat.Base
-open import Data.Bool
 ```
 -->
 
diff --git a/src/Data/Nat/Properties.lagda.md b/src/Data/Nat/Properties.lagda.md
index 845d7cbc8..ac2ba0675 100644
--- a/src/Data/Nat/Properties.lagda.md
+++ b/src/Data/Nat/Properties.lagda.md
@@ -6,7 +6,6 @@ open import 1Lab.Type
 open import Data.Nat.Order
 open import Data.Dec.Base
 open import Data.Nat.Base
-open import Data.Sum
 ```
 -->
 
diff --git a/src/Data/Nat/Solver.lagda.md b/src/Data/Nat/Solver.lagda.md
index f64be599b..59f6927d5 100644
--- a/src/Data/Nat/Solver.lagda.md
+++ b/src/Data/Nat/Solver.lagda.md
@@ -7,8 +7,6 @@ open import 1Lab.Type
 
 open import Data.Nat.Properties
 open import Data.Fin.Base
-open import Data.Nat.Base
-open import Data.Bool
 open import Data.List
 ```
 -->
diff --git a/src/Data/Wellfounded/Base.lagda.md b/src/Data/Wellfounded/Base.lagda.md
index f82e8f575..353a7a5ad 100644
--- a/src/Data/Wellfounded/Base.lagda.md
+++ b/src/Data/Wellfounded/Base.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import 1Lab.HLevel
 open import 1Lab.Path
 open import 1Lab.Type
 ```
diff --git a/src/Homotopy/Connectedness.lagda.md b/src/Homotopy/Connectedness.lagda.md
index c5dbb98b4..840bcef9e 100644
--- a/src/Homotopy/Connectedness.lagda.md
+++ b/src/Homotopy/Connectedness.lagda.md
@@ -14,9 +14,7 @@ open import Algebra.Group.Homotopy
 
 open import Data.Set.Truncation
 
-open import Homotopy.Space.Suspension
 open import Homotopy.Space.Circle
-open import Homotopy.Space.Sphere
 open import Homotopy.Base
 ```
 -->
diff --git a/src/Homotopy/Space/Sinfty.lagda.md b/src/Homotopy/Space/Sinfty.lagda.md
index 617ba4680..039204071 100644
--- a/src/Homotopy/Space/Sinfty.lagda.md
+++ b/src/Homotopy/Space/Sinfty.lagda.md
@@ -1,8 +1,6 @@
 <!--
 ```
 open import 1Lab.Prelude
-
-open import Homotopy.Space.Circle
 ```
 -->
 
diff --git a/src/Order/Instances/Lower.lagda.md b/src/Order/Instances/Lower.lagda.md
index 3c5193577..1bcca758d 100644
--- a/src/Order/Instances/Lower.lagda.md
+++ b/src/Order/Instances/Lower.lagda.md
@@ -2,7 +2,6 @@
 ```agda
 open import Cat.Prelude
 
-open import Order.Instances.Pointwise.Diagrams
 open import Order.Instances.Pointwise
 open import Order.Instances.Props
 open import Order.Diagram.Glb
diff --git a/src/Order/Instances/Subobjects.lagda.md b/src/Order/Instances/Subobjects.lagda.md
index 270709676..fe801b7ef 100644
--- a/src/Order/Instances/Subobjects.lagda.md
+++ b/src/Order/Instances/Subobjects.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-open import Cat.Univalent
 open import Cat.Prelude
 
 open import Order.Base
diff --git a/src/Order/Semilattice/Free.lagda.md b/src/Order/Semilattice/Free.lagda.md
index dde73ccf1..8454fa0c4 100644
--- a/src/Order/Semilattice/Free.lagda.md
+++ b/src/Order/Semilattice/Free.lagda.md
@@ -6,9 +6,7 @@ open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Adjoint
 open import Cat.Prelude
 
-open import Data.Nat.Properties
 open import Data.Fin.Closure
-open import Data.Nat.Order
 open import Data.Fin.Base
 open import Data.Sum.Base
 
@@ -234,7 +232,7 @@ using surjectivity of the first map.
 ```agda
     ε : Σ Nat (λ n → Σ (Fin n → Σ ∣ A ∣ λ x → x ∈ P) λ f → ∀ x → ∥ fibre f x ∥)
       → Glb B.po fam
-    ε (card , g , surj) = glb 
+    ε (card , g , surj) = glb
       where
         module h = is-glb (B.⋂-is-glb (λ x → fam (g x)))
         glb : Glb B.po fam
@@ -248,7 +246,7 @@ using surjectivity of the first map.
         glb .Glb.has-glb .is-glb.greatest lb′ lb′<subset =
           h.greatest lb′ λ i → lb′<subset (g i)
 
-    ε′ : Glb B.po fam 
+    ε′ : Glb B.po fam
     ε′ = ∥-∥-rec (Glb-is-prop B.po) ε P-fin
 
 open is-glb
diff --git a/src/Prim/Data/Float.lagda.md b/src/Prim/Data/Float.lagda.md
index 55b28163f..cb403072e 100644
--- a/src/Prim/Data/Float.lagda.md
+++ b/src/Prim/Data/Float.lagda.md
@@ -3,7 +3,6 @@
 open import 1Lab.Type
 
 open import Data.Int.Inductive
-open import Data.Bool
 
 open import Prim.Data.String
 open import Prim.Data.Maybe
diff --git a/src/Prim/Data/String.lagda.md b/src/Prim/Data/String.lagda.md
index f328d9259..183fec77d 100644
--- a/src/Prim/Data/String.lagda.md
+++ b/src/Prim/Data/String.lagda.md
@@ -5,7 +5,6 @@ open import 1Lab.Type
 open import Data.List.Base
 
 open import Prim.Data.Maybe
-open import Prim.Literals
 ```
 -->
 
diff --git a/src/Prim/HCompU.lagda.md b/src/Prim/HCompU.lagda.md
index 5d42ba496..5594f3f7b 100644
--- a/src/Prim/HCompU.lagda.md
+++ b/src/Prim/HCompU.lagda.md
@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Type.Sigma
-open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type