diff --git a/src/plta/Connectives.lagda b/src/plta/Connectives.lagda
index 978486cf..1ab9e5a4 100644
--- a/src/plta/Connectives.lagda
+++ b/src/plta/Connectives.lagda
@@ -25,11 +25,11 @@ a principle known as *Propositions as Types*.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
-open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
-open plta.Isomorphism.≃-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.Nat.Properties.Simple using (+-suc)
 open import Function using (_∘_)
+open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
+open plta.Isomorphism.≃-Reasoning
 \end{code}
 
 We assume [extensionality][extensionality].
diff --git a/src/plta/Decidable.lagda b/src/plta/Decidable.lagda
index 13831363..ffef6298 100644
--- a/src/plta/Decidable.lagda
+++ b/src/plta/Decidable.lagda
@@ -497,7 +497,8 @@ on which matches; but either is equally valid.
 
 ## Decidability of All
 
-Recall that in Chapter [Lists]({{ site.baseurl }}{% link out/plta/Lists.md %}#All) we defined a predicate `All P` that holds if a given predicate is satisfied by every element of a list.
+Recall that in Chapter [Lists]({{ site.baseurl }}{% link out/plta/Lists.md %}#All)
+we defined a predicate `All P` that holds if a given predicate is satisfied by every element of a list.
 \begin{code}
 data All {A : Set} (P : A → Set) : List A → Set where
   [] : All P []
diff --git a/src/plta/Lists.lagda b/src/plta/Lists.lagda
index cdec1037..10e195aa 100644
--- a/src/plta/Lists.lagda
+++ b/src/plta/Lists.lagda
@@ -23,9 +23,9 @@ open import Data.Nat.Properties using
   (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
 open import Relation.Nullary using (¬_)
 open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
-open import plta.Isomorphism using (_≃_)
 open import Function using (_∘_)
 open import Level using (Level)
+open import plta.Isomorphism using (_≃_)
 \end{code}
 
 We assume [extensionality][extensionality].
diff --git a/src/plta/Negation.lagda b/src/plta/Negation.lagda
index 7dcb04a8..71a2f50e 100644
--- a/src/plta/Negation.lagda
+++ b/src/plta/Negation.lagda
@@ -14,13 +14,13 @@ and classical logic.
 ## Imports
 
 \begin{code}
-open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Data.Nat using (ℕ; zero; suc)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Function using (_∘_)
+open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
 \end{code}
 
 
diff --git a/src/plta/Quantifiers.lagda b/src/plta/Quantifiers.lagda
index 1a44d4db..5f9ba715 100644
--- a/src/plta/Quantifiers.lagda
+++ b/src/plta/Quantifiers.lagda
@@ -16,14 +16,13 @@ This chapter introduces universal and existential quantification.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
-open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
-open plta.Isomorphism.≃-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Data.Nat.Properties.Simple using (+-suc)
 open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
 \end{code}
 
 We assume [extensionality][extensionality].