you know it

the1lab · Oct 3, 2024 · bd76381 · bd76381
1 parent 2682d25
commit bd76381
Showing 1 changed file with 4 additions and 5 deletions.
diff --git a/src/Talks/Topos2024.lagda.md b/src/Talks/Topos2024.lagda.md
@@ -15,19 +15,18 @@ Amélia Liao
 open import 1Lab.Path.Reasoning
 open import 1Lab.Prelude hiding (funext ; sym ; subst ; Extensional ; ext ; uncurry ; id ; _∘_ ; _==_ ; _*_ ; _+_)
 
+open import Algebra.Group.Concrete.Abelian
 open import Algebra.Group.Ab.Tensor
 open import Algebra.Group.Cat.Base hiding (Displayed)
 open import Algebra.Group.Ab
 open import Algebra.Monoid using (Monoid-on)
 open import Algebra.Group
 
-open import Data.Nat.Base hiding (_==_ ; _*_ ; _+_)
-open import Data.Int.Base
-open import Data.Sum
-
 open import Cat.Base
 
-open import Algebra.Group.Concrete.Abelian
+open import Data.Int.Base
+open import Data.Nat.Base hiding (_==_ ; _*_ ; _+_)
+open import Data.Sum
 
 open import Homotopy.Space.Circle