DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Try to generalize universe levels where possible

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-19 12:36:46 -08:00
parent aafcb2683d
commit 486b552b59
2 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Lattice/IterProd.agda
View File

@ -1,5 +1,9 @@
open import Lattice 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} module Lattice.IterProd {a} {A B : Set a}
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)

7
Lattice/Prod.agda
View File

@ -1,11 +1,12 @@
open import Lattice open import Lattice
module Lattice.Prod {a} {A B : Set a} module Lattice.Prod {a b} {A : Set a} {B : Set b}
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
(_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
open import Data.Nat using (ℕ; _≤_; _+_; suc) open import Data.Nat using (ℕ; _≤_; _+_; suc)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
@ -35,7 +36,7 @@ open IsLattice lB using () renaming
; ≺-cong to ≺₂-cong ; ≺-cong to ≺₂-cong
) )
_≈_ : A × B → A × B → Set a _≈_ : A × B → A × B → Set (a ⊔ℓ b)
(a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂) (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
≈-equiv : IsEquivalence (A × B) _≈_ ≈-equiv : IsEquivalence (A × B) _≈_