fix: qualified module name

Author: jamesmckinna

src/Algebra/Consequences/Propositional.agda

@@ -22,12 +22,12 @@ open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Unary using (Pred)
 
 open import Algebra.Definitions {A = A} _≡_
-import Algebra.Consequences.Setoid (setoid A) as Base
+import Algebra.Consequences.Setoid (setoid A) as SetoidConsequences
 
 ------------------------------------------------------------------------
 -- Re-export all proofs that don't require congruence or substitutivity
 
-open Base public
+open SetoidConsequences public
   hiding
   ( comm∧assoc⇒middleFour
   ; identity∧middleFour⇒assoc
@@ -63,12 +63,12 @@ module _ {_∙_ _⁻¹ ε} where
   assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ →
                               RightInverse ε _⁻¹ _∙_ →
                               ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹)
-  assoc∧id∧invʳ⇒invˡ-unique = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _)
+  assoc∧id∧invʳ⇒invˡ-unique = SetoidConsequences.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _)
 
   assoc∧id∧invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
                               LeftInverse ε _⁻¹ _∙_ →
                               ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹)
-  assoc∧id∧invˡ⇒invʳ-unique = Base.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _)
+  assoc∧id∧invˡ⇒invʳ-unique = SetoidConsequences.assoc∧id∧invˡ⇒invʳ-unique (cong₂ _)
 
 ------------------------------------------------------------------------
 -- Ring-like structures
@@ -79,27 +79,27 @@ module _ {_+_ _*_ -_ 0#} where
                                 RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                 LeftZero 0# _*_
   assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ =
-    Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)
+    SetoidConsequences.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)
 
   assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
                                 RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                 RightZero 0# _*_
   assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ =
-    Base.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)
+    SetoidConsequences.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)
 
 ------------------------------------------------------------------------
 -- Bisemigroup-like structures
 
 module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
 
   comm∧distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
-  comm∧distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm
+  comm∧distrˡ⇒distrʳ = SetoidConsequences.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm
 
   comm∧distrʳ⇒distrˡ : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOverˡ _◦_
-  comm∧distrʳ⇒distrˡ = Base.comm∧distrʳ⇒distrˡ (cong₂ _) ∙-comm
+  comm∧distrʳ⇒distrˡ = SetoidConsequences.comm∧distrʳ⇒distrˡ (cong₂ _) ∙-comm
 
   comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z)))
-  comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm
+  comm⇒sym[distribˡ] = SetoidConsequences.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm
 
 module _ {_∙_ _◦_ : Op₂ A}
          (∙-assoc : Associative _∙_)
@@ -108,7 +108,7 @@ module _ {_∙_ _◦_ : Op₂ A}
 
   binomial-expansion : ∀ w x y z →
              ((w ∙ x) ◦ (y ∙ z)) ≡ ((((w ◦ y) ∙ (w ◦ z)) ∙ (x ◦ y)) ∙ (x ◦ z))
-  binomial-expansion = Base.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib
+  binomial-expansion = SetoidConsequences.binomial-expansion {_∙_} {_◦_} (cong₂ _) ∙-assoc distrib
 
 ------------------------------------------------------------------------
 -- Middle-Four Exchange
@@ -117,17 +117,17 @@ module _ {_∙_ : Op₂ A} where
 
   comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
                           _∙_ MiddleFourExchange _∙_
-  comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _∙_)
+  comm∧assoc⇒middleFour = SetoidConsequences.comm∧assoc⇒middleFour (cong₂ _∙_)
 
   identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
                               _∙_ MiddleFourExchange _∙_ →
                               Associative _∙_
-  identity∧middleFour⇒assoc = Base.identity∧middleFour⇒assoc (cong₂ _∙_)
+  identity∧middleFour⇒assoc = SetoidConsequences.identity∧middleFour⇒assoc (cong₂ _∙_)
 
   identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
                              _∙_ MiddleFourExchange _+_ →
                              Commutative _∙_
-  identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _∙_)
+  identity∧middleFour⇒comm = SetoidConsequences.identity∧middleFour⇒comm (cong₂ _∙_)
 
 ------------------------------------------------------------------------
 -- Without Loss of Generality
@@ -136,13 +136,13 @@ module _ {p} {P : Pred A p} where
 
   subst∧comm⇒sym : ∀ {f} (f-comm : Commutative f) →
                    Symmetric (λ a b → P (f a b))
-  subst∧comm⇒sym = Base.subst∧comm⇒sym {P = P} subst
+  subst∧comm⇒sym = SetoidConsequences.subst∧comm⇒sym {P = P} subst
 
   wlog : ∀ {f} (f-comm : Commutative f) →
          ∀ {r} {_R_ : Rel _ r} → Total _R_ →
          (∀ a b → a R b → P (f a b)) →
          ∀ a b → P (f a b)
-  wlog = Base.wlog {P = P} subst
+  wlog = SetoidConsequences.wlog {P = P} subst
 
 
 ------------------------------------------------------------------------