Merge branch 'agda:master' into master

agda · Nov 9, 2023 · 14ef4ad · 14ef4ad
2 parents b91db4b + 4de6b69
commit 14ef4ad
Show file tree

Hide file tree

Showing 49 changed files with 3,479 additions and 347 deletions.
diff --git a/.github/workflows/ci-nix.yml b/.github/workflows/ci-nix.yml
diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
@@ -42,8 +42,8 @@ on:
 ########################################################################
 
 env:
-  AGDA_BRANCH: v2.6.3
-  GHC_VERSION: 9.2.5
+  AGDA_BRANCH: v2.6.4
+  GHC_VERSION: 9.4.7
   CABAL_VERSION: 3.6.2.0
   CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
   CACHE_PATHS: |
@@ -56,7 +56,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Install cabal
-        uses: haskell/actions/setup@v2
+        uses: haskell-actions/setup@v2
         with:
           ghc-version: ${{ env.GHC_VERSION }}
           cabal-version: ${{ env.CABAL_VERSION }}
@@ -126,7 +126,7 @@ jobs:
             library-${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}-
 
       - name: Put cabal programs in PATH
-        run: echo "~/.cabal/bin" >> $GITHUB_PATH
+        run: echo "~/.cabal/bin" >> "${GITHUB_PATH}"
 
       - name: Test cubical
         run: |

diff --git a/CITATION.cff b/CITATION.cff
@@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below."
 authors:
 - name: "The Agda Community"
 title: "Cubical Agda Library"
-version: 0.5
-date-released: 2023-07-05
+version: 0.6
+date-released: 2023-10-24
 url: "https://github.com/agda/cubical"
diff --git a/Cubical/Algebra/CommRing/Instances/Int.agda b/Cubical/Algebra/CommRing/Instances/Int.agda
@@ -22,4 +22,4 @@ isCommRing (snd ℤCommRing) = isCommRingℤ
     isCommRingℤ : IsCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_
     isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc (λ _ → refl)
                                  -Cancel Int.+Comm Int.·Assoc
-                                 Int.·Rid ·DistR+ Int.·Comm
+                                 Int.·IdR ·DistR+ Int.·Comm
diff --git a/Cubical/Algebra/CommRing/Instances/Rationals.agda b/Cubical/Algebra/CommRing/Instances/Rationals.agda
@@ -9,7 +9,7 @@ module Cubical.Algebra.CommRing.Instances.Rationals where
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.CommRing
-open import Cubical.Data.Rationals
+open import Cubical.Data.Rationals.MoreRationals.QuoQ
   renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)
 
 open CommRingStr

diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda
@@ -43,10 +43,10 @@ module Units (R' : CommRing ℓ) where
   where
   path : r' ≡ r''
   path = r'             ≡⟨ sym (·IdR _) ⟩
-         r' · 1r        ≡⟨ cong (r' ·_) (sym rr''≡1) ⟩
+         r' · 1r        ≡⟨ congR _·_ (sym rr''≡1) ⟩
          r' · (r · r'') ≡⟨ ·Assoc _ _ _ ⟩
-         (r' · r) · r'' ≡⟨ cong (_· r'') (·Comm _ _) ⟩
-         (r · r') · r'' ≡⟨ cong (_· r'') rr'≡1 ⟩
+         (r' · r) · r'' ≡⟨ congL _·_ (·Comm _ _) ⟩
+         (r · r') · r'' ≡⟨ congL _·_ rr'≡1 ⟩
          1r · r''       ≡⟨ ·IdL _ ⟩
          r''            ∎
 
@@ -73,11 +73,11 @@ module Units (R' : CommRing ℓ) where
  RˣMultClosed r r' = (r ⁻¹ · r' ⁻¹) , path
   where
   path : r · r' · (r ⁻¹ · r' ⁻¹) ≡ 1r
-  path = r · r' · (r ⁻¹ · r' ⁻¹) ≡⟨ cong (_· (r ⁻¹ · r' ⁻¹)) (·Comm _ _) ⟩
+  path = r · r' · (r ⁻¹ · r' ⁻¹) ≡⟨ congL _·_ (·Comm _ _) ⟩
          r' · r · (r ⁻¹ · r' ⁻¹) ≡⟨ ·Assoc _ _ _ ⟩
-         r' · r · r ⁻¹ · r' ⁻¹   ≡⟨ cong (_· r' ⁻¹) (sym (·Assoc _ _ _)) ⟩
+         r' · r · r ⁻¹ · r' ⁻¹   ≡⟨ congL _·_ (sym (·Assoc _ _ _)) ⟩
          r' · (r · r ⁻¹) · r' ⁻¹ ≡⟨ cong (λ x → r' · x · r' ⁻¹) (·-rinv _) ⟩
-         r' · 1r · r' ⁻¹         ≡⟨ cong (_· r' ⁻¹) (·IdR _) ⟩
+         r' · 1r · r' ⁻¹         ≡⟨ congL _·_ (·IdR _) ⟩
          r' · r' ⁻¹              ≡⟨ ·-rinv _ ⟩
          1r ∎
 
@@ -99,9 +99,9 @@ module Units (R' : CommRing ℓ) where
  UnitsAreNotZeroDivisors : (r : R) ⦃ _ : r ∈ Rˣ ⦄
                          → ∀ r' → r' · r ≡ 0r → r' ≡ 0r
  UnitsAreNotZeroDivisors r r' p = r'              ≡⟨ sym (·IdR _) ⟩
-                                  r' · 1r         ≡⟨ cong (r' ·_) (sym (·-rinv _)) ⟩
+                                  r' · 1r         ≡⟨ congR _·_ (sym (·-rinv _)) ⟩
                                   r' · (r · r ⁻¹) ≡⟨ ·Assoc _ _ _ ⟩
-                                  r' · r · r ⁻¹   ≡⟨ cong (_· r ⁻¹) p ⟩
+                                  r' · r · r ⁻¹   ≡⟨ congL _·_ p ⟩
                                   0r · r ⁻¹       ≡⟨ 0LeftAnnihilates _ ⟩
                                   0r ∎
 
@@ -139,9 +139,9 @@ module Units (R' : CommRing ℓ) where
           PathPΣ (inverseUniqueness r' (r ⁻¹ , subst (λ x → x · r ⁻¹ ≡ 1r) p (r∈Rˣ .snd)) r'∈Rˣ) .fst
 
  ⁻¹-eq-elim : {r r' r'' : R} ⦃ r∈Rˣ : r ∈ Rˣ ⦄ → r' ≡ r'' · r → r' · r ⁻¹ ≡ r''
- ⁻¹-eq-elim {r = r} {r'' = r''} p = cong (_· r ⁻¹) p
+ ⁻¹-eq-elim {r = r} {r'' = r''} p = congL _·_ p
                                   ∙ sym (·Assoc _ _ _)
-                                  ∙ cong (r'' ·_) (·-rinv _)
+                                  ∙ congR _·_ (·-rinv _)
                                   ∙ ·IdR _
 
 
@@ -220,11 +220,11 @@ module CommRingHomTheory {A' B' : CommRing ℓ} (φ : CommRingHom A' B') where
                → f (r ⁻¹ᵃ) ≡ (f r) ⁻¹ᵇ
  φ[x⁻¹]≡φ[x]⁻¹ r ⦃ r∈Aˣ ⦄ ⦃ φr∈Bˣ ⦄ =
   f (r ⁻¹ᵃ)                         ≡⟨ sym (·B-rid _) ⟩
-  f (r ⁻¹ᵃ) ·B 1b                   ≡⟨ cong (f (r ⁻¹ᵃ) ·B_) (sym (·B-rinv _)) ⟩
+  f (r ⁻¹ᵃ) ·B 1b                   ≡⟨ congR _·B_ (sym (·B-rinv _)) ⟩
   f (r ⁻¹ᵃ) ·B ((f r) ·B (f r) ⁻¹ᵇ) ≡⟨ ·B-assoc _ _ _ ⟩
-  f (r ⁻¹ᵃ) ·B (f r) ·B (f r) ⁻¹ᵇ   ≡⟨ cong (_·B (f r) ⁻¹ᵇ) (sym (pres· _ _)) ⟩
+  f (r ⁻¹ᵃ) ·B (f r) ·B (f r) ⁻¹ᵇ   ≡⟨ congL _·B_ (sym (pres· _ _)) ⟩
   f (r ⁻¹ᵃ ·A r) ·B (f r) ⁻¹ᵇ       ≡⟨ cong (λ x → f x ·B (f r) ⁻¹ᵇ) (·A-linv _) ⟩
-  f 1a ·B (f r) ⁻¹ᵇ                 ≡⟨ cong (_·B (f r) ⁻¹ᵇ) (pres1) ⟩
+  f 1a ·B (f r) ⁻¹ᵇ                 ≡⟨ congL _·B_ pres1 ⟩
   1b ·B (f r) ⁻¹ᵇ                   ≡⟨ ·B-lid _ ⟩
   (f r) ⁻¹ᵇ                         ∎
 
@@ -247,7 +247,7 @@ module Exponentiation (R' : CommRing ℓ) where
 
  ·-of-^-is-^-of-+ : (f : R) (m n : ℕ) → (f ^ m) · (f ^ n) ≡ f ^ (m +ℕ n)
  ·-of-^-is-^-of-+ f zero n = ·IdL _
- ·-of-^-is-^-of-+ f (suc m) n = sym (·Assoc _ _ _) ∙ cong (f ·_) (·-of-^-is-^-of-+ f m n)
+ ·-of-^-is-^-of-+ f (suc m) n = sym (·Assoc _ _ _) ∙ congR _·_ (·-of-^-is-^-of-+ f m n)
 
  ^-ldist-· : (f g : R) (n : ℕ) → (f · g) ^ n ≡ (f ^ n) · (g ^ n)
  ^-ldist-· f g zero = sym (·IdL 1r)
@@ -256,9 +256,9 @@ module Exponentiation (R' : CommRing ℓ) where
   path : f · g · ((f · g) ^ n) ≡ f · (f ^ n) · (g · (g ^ n))
   path = f · g · ((f · g) ^ n)       ≡⟨ cong (f · g ·_) (^-ldist-· f g n) ⟩
          f · g · ((f ^ n) · (g ^ n)) ≡⟨ ·Assoc _ _ _ ⟩
-         f · g · (f ^ n) · (g ^ n)   ≡⟨ cong (_· (g ^ n)) (sym (·Assoc _ _ _)) ⟩
+         f · g · (f ^ n) · (g ^ n)   ≡⟨ congL _·_ (sym (·Assoc _ _ _)) ⟩
          f · (g · (f ^ n)) · (g ^ n) ≡⟨ cong (λ r → (f · r) · (g ^ n)) (·Comm _ _) ⟩
-         f · ((f ^ n) · g) · (g ^ n) ≡⟨ cong (_· (g ^ n)) (·Assoc _ _ _) ⟩
+         f · ((f ^ n) · g) · (g ^ n) ≡⟨ congL _·_ (·Assoc _ _ _) ⟩
          f · (f ^ n) · g · (g ^ n)   ≡⟨ sym (·Assoc _ _ _) ⟩
          f · (f ^ n) · (g · (g ^ n)) ∎
 
@@ -282,17 +282,17 @@ module CommRingTheory (R' : CommRing ℓ) where
  private R = fst R'
 
  ·CommAssocl : (x y z : R) → x · (y · z) ≡ y · (x · z)
- ·CommAssocl x y z = ·Assoc x y z ∙∙ cong (_· z) (·Comm x y) ∙∙ sym (·Assoc y x z)
+ ·CommAssocl x y z = ·Assoc x y z ∙∙ congL _·_ (·Comm x y) ∙∙ sym (·Assoc y x z)
 
  ·CommAssocr : (x y z : R) → x · y · z ≡ x · z · y
- ·CommAssocr x y z = sym (·Assoc x y z) ∙∙ cong (x ·_) (·Comm y z) ∙∙ ·Assoc x z y
+ ·CommAssocr x y z = sym (·Assoc x y z) ∙∙ congR _·_ (·Comm y z) ∙∙ ·Assoc x z y
 
  ·CommAssocr2 : (x y z : R) → x · y · z ≡ z · y · x
- ·CommAssocr2 x y z = ·CommAssocr _ _ _ ∙∙ cong (_· y) (·Comm _ _) ∙∙ ·CommAssocr _ _ _
+ ·CommAssocr2 x y z = ·CommAssocr _ _ _ ∙∙ congL _·_ (·Comm _ _) ∙∙ ·CommAssocr _ _ _
 
  ·CommAssocSwap : (x y z w : R) → (x · y) · (z · w) ≡ (x · z) · (y · w)
  ·CommAssocSwap x y z w =
-   ·Assoc (x · y) z w ∙∙ cong (_· w) (·CommAssocr x y z) ∙∙ sym (·Assoc (x · z) y w)
+   ·Assoc (x · y) z w ∙∙ congL _·_ (·CommAssocr x y z) ∙∙ sym (·Assoc (x · z) y w)
 
 
 

diff --git a/Cubical/Algebra/DistLattice.agda b/Cubical/Algebra/DistLattice.agda
@@ -2,3 +2,4 @@
 module Cubical.Algebra.DistLattice where
 
 open import Cubical.Algebra.DistLattice.Base public
+open import Cubical.Algebra.DistLattice.Properties public
diff --git a/Cubical/Algebra/DistLattice/Properties.agda b/Cubical/Algebra/DistLattice/Properties.agda
@@ -0,0 +1,55 @@
+{-# OPTIONS --safe --lossy-unification #-}
+module Cubical.Algebra.DistLattice.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.HalfAdjoint
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.SIP
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Structures.Axioms
+open import Cubical.Structures.Auto
+open import Cubical.Structures.Macro
+open import Cubical.Algebra.Semigroup
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.CommMonoid
+open import Cubical.Algebra.Semilattice
+open import Cubical.Algebra.Lattice
+open import Cubical.Algebra.DistLattice.Base
+
+open import Cubical.Relation.Binary.Order.Poset
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ where
+  open LatticeHoms
+
+  compDistLatticeHom : (L : DistLattice ℓ) (M : DistLattice ℓ') (N : DistLattice ℓ'')
+                  → DistLatticeHom L M → DistLatticeHom M N → DistLatticeHom L N
+  compDistLatticeHom L M N = compLatticeHom {L = DistLattice→Lattice L} {DistLattice→Lattice M} {DistLattice→Lattice N}
+
+  _∘dl_ : {L : DistLattice ℓ} {M : DistLattice ℓ'} {N : DistLattice ℓ''}
+        → DistLatticeHom M N → DistLatticeHom L M → DistLatticeHom L N
+  g ∘dl f = compDistLatticeHom _ _ _ f g
+
+  compIdDistLatticeHom : {L M : DistLattice ℓ} (f : DistLatticeHom L M)
+                    → compDistLatticeHom _ _ _ (idDistLatticeHom L) f ≡ f
+  compIdDistLatticeHom = compIdLatticeHom
+
+  idCompDistLatticeHom : {L M : DistLattice ℓ} (f : DistLatticeHom L M)
+                    → compDistLatticeHom _ _ _ f (idDistLatticeHom M) ≡ f
+  idCompDistLatticeHom = idCompLatticeHom
+
+  compAssocDistLatticeHom : {L M N U : DistLattice ℓ}
+                         (f : DistLatticeHom L M) (g : DistLatticeHom M N) (h : DistLatticeHom N U)
+                       → compDistLatticeHom _ _ _ (compDistLatticeHom _ _ _ f g) h
+                       ≡ compDistLatticeHom _ _ _ f (compDistLatticeHom _ _ _ g h)
+  compAssocDistLatticeHom = compAssocLatticeHom
diff --git a/Cubical/Algebra/Field/Instances/Rationals.agda b/Cubical/Algebra/Field/Instances/Rationals.agda
@@ -19,7 +19,7 @@ open import Cubical.Data.Int.MoreInts.QuoInt
            ; ·-zeroˡ to ·ℤ-zeroˡ
            ; ·-identityʳ to ·ℤ-identityʳ)
 open import Cubical.HITs.SetQuotients as SetQuot
-open import Cubical.Data.Rationals
+open import Cubical.Data.Rationals.MoreRationals.QuoQ
   using    (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)
 
 open import Cubical.Algebra.Field

diff --git a/Cubical/Algebra/Group/Properties.agda b/Cubical/Algebra/Group/Properties.agda
@@ -32,15 +32,15 @@ module GroupTheory (G : Group ℓ) where
   abstract
     ·CancelL : (a : ⟨ G ⟩) {b c : ⟨ G ⟩} → a · b ≡ a · c → b ≡ c
     ·CancelL a {b} {c} p =
-       b               ≡⟨ sym (·IdL b) ∙ cong (_· b) (sym (·InvL a)) ∙ sym (·Assoc _ _ _) ⟩
-      inv a · (a · b)  ≡⟨ cong (inv a ·_) p ⟩
-      inv a · (a · c)  ≡⟨ ·Assoc _ _ _ ∙ cong (_· c) (·InvL a) ∙ ·IdL c ⟩
+       b               ≡⟨ sym (·IdL b) ∙ congL _·_ (sym (·InvL a)) ∙ sym (·Assoc _ _ _) ⟩
+      inv a · (a · b)  ≡⟨ congR _·_ p ⟩
+      inv a · (a · c)  ≡⟨ ·Assoc _ _ _ ∙ congL _·_ (·InvL a) ∙ ·IdL c ⟩
       c ∎
 
     ·CancelR : {a b : ⟨ G ⟩} (c : ⟨ G ⟩) → a · c ≡ b · c → a ≡ b
     ·CancelR {a} {b} c p =
-      a                ≡⟨ sym (·IdR a) ∙ cong (a ·_) (sym (·InvR c)) ∙ ·Assoc _ _ _ ⟩
-      (a · c) · inv c  ≡⟨ cong (_· inv c) p ⟩
+      a                ≡⟨ sym (·IdR a) ∙ congR _·_ (sym (·InvR c)) ∙ ·Assoc _ _ _ ⟩
+      (a · c) · inv c  ≡⟨ congL _·_ p ⟩
       (b · c) · inv c  ≡⟨ sym (·Assoc _ _ _) ∙ cong (b ·_) (·InvR c) ∙ ·IdR b ⟩
       b ∎
 
@@ -65,22 +65,18 @@ module GroupTheory (G : Group ℓ) where
     idFromIdempotency : (x : ⟨ G ⟩) → x ≡ x · x → x ≡ 1g
     idFromIdempotency x p =
       x                 ≡⟨ sym (·IdR x) ⟩
-      x · 1g            ≡⟨ cong (λ u → x · u) (sym (·InvR _)) ⟩
+      x · 1g            ≡⟨ congR _·_ (sym (·InvR _)) ⟩
       x · (x · inv x)   ≡⟨ ·Assoc _ _ _ ⟩
-      (x · x) · (inv x) ≡⟨ cong (λ u → u · (inv x)) (sym p) ⟩
+      (x · x) · (inv x) ≡⟨ congL _·_ (sym p) ⟩
       x · (inv x)       ≡⟨ ·InvR _ ⟩
       1g              ∎
 
-
     invDistr : (a b : ⟨ G ⟩) → inv (a · b) ≡ inv b · inv a
     invDistr a b = sym (invUniqueR γ) where
       γ : (a · b) · (inv b · inv a) ≡ 1g
-      γ = (a · b) · (inv b · inv a)
-            ≡⟨ sym (·Assoc _ _ _) ⟩
-          a · b · (inv b) · (inv a)
-            ≡⟨ cong (a ·_) (·Assoc _ _ _ ∙ cong (_· (inv a)) (·InvR b)) ⟩
-          a · (1g · inv a)
-            ≡⟨ cong (a ·_) (·IdL (inv a)) ∙ ·InvR a ⟩
+      γ = (a · b) · (inv b · inv a) ≡⟨ sym (·Assoc _ _ _) ⟩
+          a · b · (inv b) · (inv a) ≡⟨ congR _·_ (·Assoc _ _ _ ∙ congL _·_ (·InvR b)) ⟩
+          a · (1g · inv a)          ≡⟨ congR _·_ (·IdL (inv a)) ∙ ·InvR a ⟩
           1g ∎
 
 congIdLeft≡congIdRight : (_·G_ : G → G → G) (-G_ : G → G)
@@ -89,10 +85,10 @@ congIdLeft≡congIdRight : (_·G_ : G → G → G) (-G_ : G → G)
             (lUnitG : (x : G) → 0G ·G x ≡ x)
           → (r≡l : rUnitG 0G ≡ lUnitG 0G)
           → (p : 0G ≡ 0G) →
-            cong (0G ·G_) p ≡ cong (_·G 0G) p
+            congR _·G_ p ≡ congL _·G_ p
 congIdLeft≡congIdRight _·G_ -G_ 0G rUnitG lUnitG r≡l p =
-            rUnit (cong (0G ·G_) p)
+            rUnit (congR _·G_ p)
          ∙∙ ((λ i → (λ j → lUnitG 0G (i ∧ j)) ∙∙ cong (λ x → lUnitG x i) p ∙∙ λ j → lUnitG 0G (i ∧ ~ j))
          ∙∙ cong₂ (λ x y → x ∙∙ p ∙∙ y) (sym r≡l) (cong sym (sym r≡l))
          ∙∙ λ i → (λ j → rUnitG 0G (~ i ∧ j)) ∙∙ cong (λ x → rUnitG x (~ i)) p ∙∙ λ j → rUnitG 0G (~ i ∧ ~ j))
-         ∙∙ sym (rUnit (cong (_·G 0G) p))
+         ∙∙ sym (rUnit (congL _·G_ p))
diff --git a/Cubical/Algebra/Group/ZAction.agda b/Cubical/Algebra/Group/ZAction.agda
@@ -12,9 +12,9 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Powerset
 
 open import Cubical.Data.Sigma
-open import Cubical.Data.Int
+open import Cubical.Data.Int as ℤ
   renaming
-    (_·_ to _*_ ; _+_ to _+ℤ_ ; _-_ to _-ℤ_ ; pos·pos to pos·) hiding (·Assoc)
+    (_·_ to _*_ ; _+_ to _+ℤ_ ; _-_ to _-ℤ_ ; pos·pos to pos·) hiding (·Assoc; ·IdL; ·IdR)
 open import Cubical.Data.Nat renaming (_·_ to _·ℕ_ ; _+_ to _+ℕ_)
 open import Cubical.Data.Nat.Mod
 open import Cubical.Data.Nat.Order
@@ -410,7 +410,7 @@ characℤ≅ℤ e =
     (λ p → inr (Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                   (Σ≡Prop (λ _ → isPropIsEquiv _)
                     (funExt λ x →
-                      cong (fst (fst e)) (sym (·Rid x))
+                      cong (fst (fst e)) (sym (ℤ.·IdR x))
                       ∙ GroupHomℤ→ℤPres· ((fst (fst e)) , (snd e)) x 1
                       ∙ cong (x *_) p
                       ∙ ·Comm x -1 ))))

diff --git a/Cubical/Algebra/Lattice/Base.agda b/Cubical/Algebra/Lattice/Base.agda
@@ -194,6 +194,19 @@ isPropIsLatticeHom R f S = isOfHLevelRetractFromIso 1 IsLatticeHomIsoΣ
   open LatticeStr S
 
 
+isSetLatticeHom : (A : Lattice ℓ) (B : Lattice ℓ') → isSet (LatticeHom A B)
+isSetLatticeHom A B = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f → isPropIsLatticeHom (snd A) f (snd B))
+  where
+  open LatticeStr (str B) using (is-set)
+
+isSetLatticeEquiv : (A : Lattice ℓ) (B : Lattice ℓ') → isSet (LatticeEquiv A B)
+isSetLatticeEquiv A B = isSetΣSndProp (isOfHLevel≃ 2 A.is-set B.is-set)
+                                      (λ e → isPropIsLatticeHom (snd A) (fst e) (snd B))
+  where
+  module A = LatticeStr (str A)
+  module B = LatticeStr (str B)
+
+
 𝒮ᴰ-Lattice : DUARel (𝒮-Univ ℓ) LatticeStr ℓ
 𝒮ᴰ-Lattice =
   𝒮ᴰ-Record (𝒮-Univ _) IsLatticeEquiv
Original file line number	Diff line number	Diff line change
Expand Up		@@ -2,3 +2,4 @@
		module Cubical.Algebra.DistLattice where

		open import Cubical.Algebra.DistLattice.Base public
		open import Cubical.Algebra.DistLattice.Properties public