Apartness & Construct (#2597)

Co-authored-by: Jacques Carette <[email protected]>

Author: jmougeot

Diff for: 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 for: 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)