Merge pull request #65 from JacquesCarette/galc2

Fix issues from PR #61
ualib · Jul 12, 2021 · 51a8c61 · 51a8c61
2 parents 149064b + 52602a2
commit 51a8c61
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 16 deletions.
diff --git a/UniversalAlgebra/GaloisConnections/Basic.lagda b/UniversalAlgebra/GaloisConnections/Basic.lagda
@@ -31,9 +31,9 @@ open import Relation.Unary          using    ( _⊆_ ;  _∈_ ; Pred   )
 
 
 
-module _ {α β ρ₁ ρ₂ ρ₃ ρ₄ : Level}
-         (A : Poset α ρ₁ ρ₂)
-         (B : Poset β ρ₃ ρ₄)
+module _ {α β ℓᵃ ρᵃ ℓᵇ ρᵇ : Level}
+         (A : Poset α ℓᵃ ρᵃ)
+         (B : Poset β ℓᵇ ρᵇ)
          where
 
  open Poset
@@ -42,14 +42,14 @@ module _ {α β ρ₁ ρ₂ ρ₃ ρ₄ : Level}
   _≤A_ = _≤_ A
   _≤B_ = _≤_ B
 
- record Galois : Type (lsuc (α ⊔ β ⊔ ρ₂ ⊔ ρ₄))  where
+ record Galois : Type (lsuc (α ⊔ β ⊔ ρᵃ ⊔ ρᵇ))  where
   field
    F : Carrier A → Carrier B
    G : Carrier B → Carrier A
    GF≥id : ∀ a →  a ≤A G (F a)
    FG≥id : ∀ b →  b ≤B F (G b)
 
- record Residuation : Type (lsuc (α ⊔ β ⊔ ρ₂ ⊔ ρ₄))  where
+ record Residuation : Type (lsuc (α ⊔ β ⊔ ρᵃ ⊔ ρᵇ))  where
   field
    f     : Carrier A → Carrier B
    fhom  : f Preserves _≤A_ ⟶ _≤B_
@@ -61,31 +61,31 @@ module _ {α β ρ₁ ρ₂ ρ₃ ρ₄ : Level}
 module _ {α β : Level}{𝒜 : Type α}{ℬ : Type β} where
 
  -- For A ⊆ 𝒜, define A ⃗ R = {b : b ∈ ℬ,  ∀ a ∈ A → R a b }
- _⃗_ : ∀ {ρ₁ ρ₂} → Pred 𝒜 ρ₁ → REL 𝒜 ℬ ρ₂ → Pred ℬ (α ⊔ ρ₁ ⊔ ρ₂)
+ _⃗_ : ∀ {ρᵃ ρᵇ} → Pred 𝒜 ρᵃ → REL 𝒜 ℬ ρᵇ → Pred ℬ (α ⊔ ρᵃ ⊔ ρᵇ)
  A ⃗ R = λ b → A ⊆ (λ a → R a b)
 
  -- For B ⊆ ℬ, define R ⃖ B = {a : a ∈ 𝒜,  ∀ b ∈ B → R a b }
- _⃖_ : ∀ {ρ₁ ρ₂} → REL 𝒜 ℬ ρ₁ → Pred ℬ ρ₂ → Pred 𝒜 (β ⊔ ρ₁ ⊔ ρ₂)
+ _⃖_ : ∀ {ρᵃ ρᵇ} → REL 𝒜 ℬ ρᵃ → Pred ℬ ρᵇ → Pred 𝒜 (β ⊔ ρᵃ ⊔ ρᵇ)
  R ⃖ B = λ a → B ⊆ R a
 
- ←→≥id : ∀ {ρ₁ ρ₂} {A : Pred 𝒜 ρ₁} {R : REL 𝒜 ℬ ρ₂} → A ⊆ R ⃖ (A ⃗ R)
+ ←→≥id : ∀ {ρᵃ ρʳ} {A : Pred 𝒜 ρᵃ} {R : REL 𝒜 ℬ ρʳ} → A ⊆ R ⃖ (A ⃗ R)
  ←→≥id p b = b p
 
- →←≥id : ∀ {ρ₁ ρ₂} {B : Pred ℬ ρ₁} {R : REL 𝒜 ℬ ρ₂}  → B ⊆ (R ⃖ B) ⃗ R
+ →←≥id : ∀ {ρᵇ ρʳ} {B : Pred ℬ ρᵇ} {R : REL 𝒜 ℬ ρʳ}  → B ⊆ (R ⃖ B) ⃗ R
  →←≥id p a = a p
 
- →←→⊆→ : ∀ {ρ₁ ρ₂} {A : Pred 𝒜 ρ₁}{R : REL 𝒜 ℬ ρ₂} → (R ⃖ (A ⃗ R)) ⃗ R ⊆ A ⃗ R
+ →←→⊆→ : ∀ {ρᵃ ρʳ} {A : Pred 𝒜 ρᵃ}{R : REL 𝒜 ℬ ρʳ} → (R ⃖ (A ⃗ R)) ⃗ R ⊆ A ⃗ R
  →←→⊆→ p a = p (λ z → z a)
 
- ←→←⊆← : ∀ {ρ₁ ρ₂} {B : Pred ℬ ρ₁}{R : REL 𝒜 ℬ ρ₂}  → R ⃖ ((R ⃖ B) ⃗ R) ⊆ R ⃖ B
+ ←→←⊆← : ∀ {ρᵇ ρʳ} {B : Pred ℬ ρᵇ}{R : REL 𝒜 ℬ ρʳ}  → R ⃖ ((R ⃖ B) ⃗ R) ⊆ R ⃖ B
  ←→←⊆← p b = p (λ z → z b)
 
  -- Definition of "closed" with respect to the closure operator λ A → R ⃖ (A ⃗ R)
- ←→Closed : ∀ {ρ₁ ρ₂} {A : Pred 𝒜 ρ₁} {R : REL 𝒜 ℬ ρ₂} → Type _
+ ←→Closed : ∀ {ρᵃ ρʳ} {A : Pred 𝒜 ρᵃ} {R : REL 𝒜 ℬ ρʳ} → Type _
  ←→Closed {A = A}{R} = R ⃖ (A ⃗ R) ⊆ A
 
  -- Definition of "closed" with respect to the closure operator λ B → (R ⃖ B) ⃗ R
- →←Closed : ∀ {ρ₁ ρ₂} {B : Pred ℬ ρ₁}{R : REL 𝒜 ℬ ρ₂} → Type _
+ →←Closed : ∀ {ρᵇ ρʳ} {B : Pred ℬ ρᵇ}{R : REL 𝒜 ℬ ρʳ} → Type _
  →←Closed {B = B}{R} = (R ⃖ B) ⃗ R ⊆ B
 
 \end{code}

diff --git a/UniversalAlgebra/agda-algebras-everything.lagda b/UniversalAlgebra/agda-algebras-everything.lagda
@@ -64,10 +64,9 @@ open import GaloisConnections.Properties    using    ( _≐_ ; ≐-iseqv ; Poset
 
 open import ClosureSystems.Definitions      using    ( Extensive ; OrderPreserving ; Idempotent )
 
-open import ClosureSystems.Basic            using    ( ⊥ ; ⊤ ; ∅ ; 𝒞𝓁 ; ClOp )
+open import ClosureSystems.Basic            using    ( ∅ ; 𝒞𝓁 ; ClOp )
 
-open import ClosureSystems.Properties       using    ( ≦rfl ; ≦trans ; ≦antisym ; clop→law⇒
-                                                     ; clop→law⇐ ; clop←law )
+open import ClosureSystems.Properties       using    ( clop→law⇒ ; clop→law⇐ ; clop←law )
 
 
 -- ALGEBRAS ------------------------------------------------------------------------------------------