diff --git a/src/Algebra/Apartness/Bundles.agda b/src/Algebra/Apartness/Bundles.agda
index 9a55794051..ba9c715ff4 100644
--- a/src/Algebra/Apartness/Bundles.agda
+++ b/src/Algebra/Apartness/Bundles.agda
@@ -13,7 +13,7 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (ApartnessRelation)
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Bundles using (CommutativeRing)
-open import Algebra.Apartness.Structures
+open import Algebra.Apartness.Structures using (IsHeytingCommutativeRing; IsHeytingField)
 
 record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 -_
diff --git a/src/Algebra/Construct/Add/Identity.agda b/src/Algebra/Construct/Add/Identity.agda
index a22e6785fd..db0d029ea7 100644
--- a/src/Algebra/Construct/Add/Identity.agda
+++ b/src/Algebra/Construct/Add/Identity.agda
@@ -14,9 +14,9 @@ open import Algebra.Core using (Op₂)
 open import Algebra.Definitions
   using (Congruent₂; Associative; LeftIdentity; RightIdentity; Identity)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
-open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
 open import Data.Product.Base using (_,_)
 open import Level using (Level; _⊔_)
+open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive)
 open import Relation.Binary.Structures using (IsEquivalence)