From 486b552b59cfcfb3cbe76365951782f57049c2b2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 19 Feb 2024 12:36:46 -0800 Subject: [PATCH] Try to generalize universe levels where possible Signed-off-by: Danila Fedorin --- Lattice/IterProd.agda | 4 ++++ Lattice/Prod.agda | 7 ++++--- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda index 00cbe43..d1fa771 100644 --- a/Lattice/IterProd.agda +++ b/Lattice/IterProd.agda @@ -1,5 +1,9 @@ open import Lattice +-- Due to universe levels, it becomes relatively annoying to handle the case +-- where the levels of A and B are not the same. For the time being, constrain +-- them to be the same. + module Lattice.IterProd {a} {A B : Set a} (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda index 0663eb5..fe9b9d4 100644 --- a/Lattice/Prod.agda +++ b/Lattice/Prod.agda @@ -1,11 +1,12 @@ open import Lattice -module Lattice.Prod {a} {A B : Set a} - (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) +module Lattice.Prod {a b} {A : Set a} {B : Set b} + (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b) (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where +open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) open import Data.Nat using (ℕ; _≤_; _+_; suc) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Empty using (⊥-elim) @@ -35,7 +36,7 @@ open IsLattice lB using () renaming ; ≺-cong to ≺₂-cong ) -_≈_ : A × B → A × B → Set a +_≈_ : A × B → A × B → Set (a ⊔ℓ b) (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂) ≈-equiv : IsEquivalence (A × B) _≈_