[Import] Relation.Binary.Indexed ... .Lattice (#2648)

* [Import]

* Update src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda

whitespace

* Update src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda

cognate grouping

* Update src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda

* fix: restore import of `Definitions`, this time with `using` list

* fix: remove redundant `import`

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Co-authored-by: jamesmckinna <j.mckinna@hw.ac.uk>

Author: jmougeot

src/Relation/Binary/Indexed/Homogeneous/Bundles.agda

@@ -13,12 +13,12 @@ module Relation.Binary.Indexed.Homogeneous.Bundles where
 
 open import Level using (suc; _⊔_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Bundles as B using (Setoid; Poset; Preorder)
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Binary.Bundles as B using (Setoid; Preorder; Poset)
 open import Relation.Binary.Indexed.Homogeneous.Core using (IRel; Lift)
 open import Relation.Binary.Indexed.Homogeneous.Structures
   using (IsIndexedEquivalence; IsIndexedDecEquivalence; IsIndexedPreorder
         ; IsIndexedPartialOrder)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 -- Indexed structures are laid out in a similar manner as to those
 -- in Relation.Binary. The main difference is each structure also

src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda

@@ -10,9 +10,11 @@ module Relation.Binary.Indexed.Homogeneous.Construct.At where
 
 open import Level using (Level)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder)
+open import Relation.Binary.Indexed.Homogeneous
+  using (IRel; IsIndexedEquivalence; IsIndexedDecEquivalence; IsIndexedPreorder
+        ; IndexedSetoid; IndexedDecSetoid; IndexedPreorder)
 open import Relation.Binary.Structures
   using (IsEquivalence; IsDecEquivalence; IsPreorder)
-open import Relation.Binary.Indexed.Homogeneous using (IRel; IsIndexedEquivalence; IsIndexedDecEquivalence; IsIndexedPreorder; IndexedSetoid; IndexedDecSetoid; IndexedPreorder)
 
 private
   variable

src/Relation/Binary/Indexed/Homogeneous/Definitions.agda

@@ -14,12 +14,11 @@ module Relation.Binary.Indexed.Homogeneous.Definitions where
 open import Data.Product.Base using (_×_)
 open import Level using (Level)
 open import Relation.Binary.Core using (_⇒_)
-open import Relation.Binary.Indexed.Homogeneous.Core using (IRel)
 import Relation.Binary.Definitions as B
   using (Reflexive; Symmetric; Transitive; Antisymmetric; Decidable)
+open import Relation.Binary.Indexed.Homogeneous.Core using (IRel)
 open import Relation.Unary.Indexed using (IPred)
 
-
 private
   variable
     i a ℓ ℓ₁ ℓ₂ : Level

src/Relation/Binary/Indexed/Homogeneous/Structures.agda

@@ -22,9 +22,13 @@ open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Core using (_⇒_)
 import Relation.Binary.Definitions as B
+  using (Reflexive; Symmetric; Transitive; Antisymmetric
+        ;_Respectsˡ_; _Respectsʳ_; _Respects₂_)
 import Relation.Binary.Structures as B using (IsEquivalence; IsPreorder; IsPartialOrder)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.Indexed.Homogeneous.Definitions
+import Relation.Binary.Structures as B
+  using (IsEquivalence; IsPreorder; IsPartialOrder)
 
 ------------------------------------------------------------------------
 -- Equivalences

src/Relation/Binary/Lattice/Bundles.agda

@@ -11,7 +11,7 @@
 
 module Relation.Binary.Lattice.Bundles where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Level using (suc; _⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Poset; Setoid)

src/Relation/Binary/Lattice/Definitions.agda

@@ -11,11 +11,11 @@
 
 module Relation.Binary.Lattice.Definitions where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (_×_; _,_)
 open import Function.Base using (flip)
-open import Relation.Binary.Core using (Rel)
 open import Level using (Level)
+open import Relation.Binary.Core using (Rel)
 
 private
   variable

src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda

@@ -11,14 +11,16 @@ open import Relation.Binary.Lattice
 module Relation.Binary.Lattice.Properties.BoundedJoinSemilattice
   {c ℓ₁ ℓ₂} (J : BoundedJoinSemilattice c ℓ₁ ℓ₂) where
 
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_; flip)
+
 open BoundedJoinSemilattice J
 
 open import Algebra.Definitions _≈_
-open import Data.Product.Base using (_,_)
-open import Function.Base using (_∘_; flip)
+  using (LeftIdentity; RightIdentity; Identity)
 open import Relation.Binary.Properties.Poset poset
-open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice
-  using (∨-comm)
+  using (≥-isPartialOrder)
+
 
 -- Bottom is an identity of the meet operation.
 

src/Relation/Binary/Lattice/Properties/BoundedLattice.agda

@@ -11,14 +11,16 @@ open import Relation.Binary.Lattice
 module Relation.Binary.Lattice.Properties.BoundedLattice
   {c ℓ₁ ℓ₂} (L : BoundedLattice c ℓ₁ ℓ₂) where
 
-open BoundedLattice L
-
-open import Algebra.Definitions _≈_
 open import Data.Product.Base using (_,_)
 open import Relation.Binary.Bundles using (Setoid)
+
+open BoundedLattice L
+
+open import Algebra.Definitions _≈_ using (Zero; RightZero; LeftZero)
 open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice
+  using (y≤x⇒x∧y≈y; ∧-comm)
 open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice
-
+  using (x≤y⇒x∨y≈y; ∨-comm )
 open Setoid setoid renaming (trans to ≈-trans)
 
 ∧-zeroʳ : RightZero ⊥ _∧_

src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda

@@ -7,15 +7,19 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Lattice
+  using (BoundedMeetSemilattice; IsBoundedJoinSemilattice; BoundedJoinSemilattice)
 
 module Relation.Binary.Lattice.Properties.BoundedMeetSemilattice
   {c ℓ₁ ℓ₂} (M : BoundedMeetSemilattice c ℓ₁ ℓ₂) where
 
+open import Function.Base using (_∘_; flip)
+
 open BoundedMeetSemilattice M
+  using (⊤; _∧_; isBoundedMeetSemilattice; _≈_; poset; _≤_; infimum; maximum)
 
 open import Algebra.Definitions _≈_
-open import Function.Base using (_∘_; flip)
-open import Relation.Binary.Properties.Poset poset
+  using (LeftIdentity; RightIdentity; Identity)
+open import Relation.Binary.Properties.Poset poset using (≥-isPartialOrder)
 import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as J
 
 -- The dual construction is a bounded join semilattice.
@@ -37,3 +41,4 @@ dualBoundedJoinSemilattice = record
 
 open J dualBoundedJoinSemilattice
   hiding (dualIsBoundedMeetSemilattice; dualBoundedMeetSemilattice) public
+

src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda

@@ -11,15 +11,21 @@ open import Relation.Binary.Lattice
 module Relation.Binary.Lattice.Properties.DistributiveLattice
   {c ℓ₁ ℓ₂} (L : DistributiveLattice c ℓ₁ ℓ₂) where
 
+open import Data.Product.Base using (_,_)
+open import Relation.Binary.Bundles using (Setoid)
+
 open DistributiveLattice L hiding (refl)
 
 open import Algebra.Definitions _≈_
-open import Data.Product.Base using (_,_)
-open import Relation.Binary.Bundles using (Setoid)
+  using (Zero; RightZero; LeftZero
+        ; _DistributesOverʳ_; _DistributesOverˡ_; _DistributesOver_)
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Relation.Binary.Lattice.Properties.Lattice lattice
+  using (∧-absorbs-∨; ∨-absorbs-∧ )
 open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice
+  using (∧-comm; ∧-cong)
 open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice
+  using (∨-comm; ∨-cong; ∨-assoc)
 
 open Setoid setoid
 
@@ -52,3 +58,4 @@ open Setoid setoid
 
 ∨-distrib-∧ : _∨_ DistributesOver _∧_
 ∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧
+