chore: sort imports

the1lab · Nov 5, 2023 · bc0e9cc · bc0e9cc
1 parent 6b6a5c2
commit bc0e9cc
Show file tree

Hide file tree

Showing 6 changed files with 18 additions and 17 deletions.
diff --git a/src/Cat/Diagram/Exponential.lagda.md b/src/Cat/Diagram/Exponential.lagda.md
@@ -4,9 +4,9 @@ open import Cat.Functor.Adjoint.Hom
 open import Cat.Instances.Product
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Terminal
-open import Cat.Instances.Slice
-open import Cat.Functor.Adjoint
 open import Cat.Diagram.Product
+open import Cat.Functor.Adjoint
+open import Cat.Instances.Slice
 open import Cat.Prelude
 
 import Cat.Functor.Bifunctor as Bifunctor

diff --git a/src/Cat/Displayed/Doctrine/Frame.lagda.md b/src/Cat/Displayed/Doctrine/Frame.lagda.md
@@ -1,30 +1,31 @@
 <!--
 ```agda
-open import Cat.Displayed.Doctrine
-open import Cat.Diagram.Product
-open import Cat.Diagram.Terminal
+open import Cat.Instances.Sets.Complete
 open import Cat.Displayed.Cocartesian
 open import Cat.Displayed.Cartesian
+open import Cat.Displayed.Doctrine
+open import Cat.Diagram.Pullback
+open import Cat.Diagram.Terminal
+open import Cat.Diagram.Product
 open import Cat.Displayed.Fibre
 open import Cat.Displayed.Base
-open import Cat.Diagram.Pullback
 open import Cat.Prelude
 
-open import Cat.Instances.Sets.Complete
 open import Order.Frame
 
-import Order.Frame.Reasoning as Frm
 import Cat.Reasoning as Cat
 
+import Order.Frame.Reasoning as Frm
+
 open Regular-hyperdoctrine
-open Displayed
-open Cartesian-fibration
-open Cartesian-lift
-open is-cartesian
 open Cocartesian-fibration
+open Cartesian-fibration
 open Cocartesian-lift
+open Cartesian-lift
 open is-cocartesian
+open is-cartesian
 open is-product
+open Displayed
 open Terminal
 open Product
 ```

diff --git a/src/Cat/Displayed/Doctrine/Logic.lagda.md b/src/Cat/Displayed/Doctrine/Logic.lagda.md
@@ -2,15 +2,16 @@
 ```agda
 open import Cat.Diagram.Limit.Finite
 open import Cat.Displayed.Doctrine
-open import Cat.Diagram.Product
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Terminal
+open import Cat.Diagram.Product
 open import Cat.Displayed.Base
 open import Cat.Prelude
 
 import Cat.Displayed.Reasoning as Disp
-import Order.Reasoning
 import Cat.Reasoning as Cat
+
+import Order.Reasoning
 ```
 -->
 

diff --git a/src/Cat/Displayed/InternalSum.lagda.md b/src/Cat/Displayed/InternalSum.lagda.md
@@ -6,7 +6,6 @@ open import Cat.Displayed.Adjoint
 open import Cat.Displayed.Functor
 open import Cat.Displayed.Base
 open import Cat.Prelude
-
 ```
 -->
 

diff --git a/src/Cat/Instances/Slice.lagda.md b/src/Cat/Instances/Slice.lagda.md
@@ -1,8 +1,8 @@
 <!--
 ```agda
 open import Cat.Diagram.Limit.Finite
-open import Cat.Instances.Discrete
 open import Cat.Functor.Properties
+open import Cat.Instances.Discrete
 open import Cat.Diagram.Pullback
 open import Cat.Diagram.Terminal
 open import Cat.Diagram.Product

diff --git a/src/Cat/Instances/Slice/Twice.lagda.md b/src/Cat/Instances/Slice/Twice.lagda.md
@@ -1,7 +1,7 @@
 <!--
 ```agda
-open import Cat.Instances.Slice
 open import Cat.Functor.Adjoint
+open import Cat.Instances.Slice
 open import Cat.Prelude
 
 import Cat.Reasoning
-Original file line number
+Diff line change
@@ Expand Up / @@ -6,7 +6,6 @@ open import Cat.Displayed.Adjoint @@
     open import Cat.Displayed.Functor
     open import Cat.Displayed.Base
     open import Cat.Prelude
     ```
     -->
@@ Expand Down @@