format

Author: malarbol

src/finite-probability-theory/positive-distributions-on-finite-types.lagda.md

@@ -14,15 +14,15 @@ open import foundation.function-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
-open import ring-theory.large-rings
-open import ring-theory.rings
-
 open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.large-ring-of-real-numbers
 open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
 
+open import ring-theory.large-rings
+open import ring-theory.rings
+
 open import univalent-combinatorics.finite-types
 ```
 

src/finite-probability-theory/probability-distributions-on-finite-types.lagda.md

@@ -18,15 +18,15 @@ open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
-open import ring-theory.large-rings
-open import ring-theory.rings
-
 open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.large-ring-of-real-numbers
 open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
 
+open import ring-theory.large-rings
+open import ring-theory.rings
+
 open import univalent-combinatorics.finite-types
 ```
 

src/real-numbers/apartness-real-numbers.lagda.md

@@ -8,9 +8,9 @@ module real-numbers.apartness-real-numbers where
 
 ```agda
 open import foundation.apartness-relations
-open import foundation.coproduct-types
 open import foundation.binary-relations
 open import foundation.binary-transport
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.empty-types
@@ -34,7 +34,6 @@ open import metric-spaces.apartness-located-metric-spaces
 open import real-numbers.absolute-value-real-numbers
 open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
-open import real-numbers.rational-real-numbers
 open import real-numbers.difference-real-numbers
 open import real-numbers.distance-real-numbers
 open import real-numbers.inequality-real-numbers