add ≤→∧≡Left and ≥→∧≡Right into the Properties module. Add isPropIsPseudolattice into the the Base file

Author: LorenzoMolena

Cubical/Relation/Binary/Order/Pseudolattice/Base.agda

@@ -1,11 +1,17 @@
 module Cubical.Relation.Binary.Order.Pseudolattice.Base where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.SIP
 
+open import Cubical.Reflection.RecordEquiv
+
 open import Cubical.Relation.Binary.Base
-open import Cubical.Relation.Binary.Order.Poset renaming (isPseudolattice to pseudolattice)
-open import Cubical.Relation.Binary.Order.StrictOrder
+open import Cubical.Relation.Binary.Order.Poset renaming (
+  isPseudolattice to pseudolattice ;
+  isPropIsPseudolattice to is-prop-is-pseudolattice)
 
 open BinaryRelation
 
@@ -31,6 +37,9 @@ record IsPseudolattice {L : Type ℓ} (_≤_ : L → L → Type ℓ') : Type (
   infixl 7 _∧l_
   infixl 6 _∨l_
 
+
+unquoteDecl IsPseudolatticeIsoΣ = declareRecordIsoΣ IsPseudolatticeIsoΣ (quote IsPseudolattice)
+
 record PseudolatticeStr (ℓ' : Level) (L : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   constructor pseudolatticestr
 
@@ -42,6 +51,9 @@ record PseudolatticeStr (ℓ' : Level) (L : Type ℓ) : Type (ℓ-suc (ℓ-max 
 
   open IsPseudolattice is-pseudolattice public
 
+
+unquoteDecl PseudolatticeStrIsoΣ = declareRecordIsoΣ PseudolatticeStrIsoΣ (quote PseudolatticeStr)
+
 Pseudolattice : ∀ ℓ ℓ' → Type (ℓ-suc (ℓ-max ℓ ℓ'))
 Pseudolattice ℓ ℓ' = TypeWithStr ℓ (PseudolatticeStr ℓ')
 
@@ -59,3 +71,9 @@ makeIsPseudolattice {_≤_ = _≤_} is-setL is-prop-valued is-refl is-trans is-a
     PS : IsPseudolattice _≤_
     PS .IsPseudolattice.isPoset = isposet is-setL is-prop-valued is-refl is-trans is-antisym
     PS .IsPseudolattice.isPseudolattice = is-meet-semipseudolattice , is-join-semipseudolattice
+
+isPropIsPseudolattice : {L : Type ℓ} (_≤_ : L → L → Type ℓ') → isProp (IsPseudolattice _≤_)
+isPropIsPseudolattice {L = L} _≤_ = isOfHLevelRetractFromIso 1
+  IsPseudolatticeIsoΣ $ isPropΣ
+  (isPropIsPoset _≤_) λ isPoset →
+  is-prop-is-pseudolattice (poset L _≤_ isPoset)

Cubical/Relation/Binary/Order/Pseudolattice/Properties.agda

@@ -49,7 +49,7 @@ module MeetProperties (L≤ : Pseudolattice ℓ ℓ') where
   ∧≤R = equivFun isMeet∧ (is-refl _) .snd
 
   ∧GLB : ∀ {a b x} → x ≤ a → x ≤ b → x ≤ a ∧l b
-  ∧GLB {a} {b} {x} = curry (invEq isMeet∧)
+  ∧GLB = curry (invEq isMeet∧)
 
   isMeet→≡∧ : ∀ m
               → (∀ {x} → x ≤ m → x ≤ a)
@@ -76,7 +76,13 @@ module MeetProperties (L≤ : Pseudolattice ℓ ℓ') where
   ≤≃∧ = order≃meet isPoset _ _ _ λ _ → isMeet∧
 
   ≤→∧ : a ≤ b → a ≡ a ∧l b
-  ≤→∧ {a} {b} = equivFun ≤≃∧
+  ≤→∧ = equivFun ≤≃∧
+
+  ≤→∧≡Left : a ≤ b → a ∧l b ≡ a
+  ≤→∧≡Left = sym ∘ ≤→∧
+
+  ≥→∧≡Right : b ≤ a → a ∧l b ≡ b
+  ≥→∧≡Right = sym ∘ (_∙ ∧Comm) ∘ ≤→∧
 
   Pseudolattice→Semigroup∧ : Semigroup ℓ
   Pseudolattice→Semigroup∧ .fst = L
@@ -88,6 +94,7 @@ open MeetProperties public
 
 module _ (L≤ : Pseudolattice ℓ ℓ') where
   open MeetProperties (DualPseudolattice L≤) public renaming (
-      isMeet∧ to isJoin∨ ; ∧≤L to L≤∨ ; ∧≤R to R≤∨ ; ∧GLB to ∨LUB
-    ; isMeet→≡∧ to isJoin→≡∨ ; ∧Comm to ∨Comm ; ∧Idem to ∨Idem ; ∧Assoc to ∨Assoc
-    ; ≤≃∧ to ≤≃∨ ; ≤→∧ to ≤→∨ ; Pseudolattice→Semigroup∧ to Pseudolattice→Semigroup∨)
+      isMeet∧ to isJoin∨ ; ∧≤L to L≤∨ ; ∧≤R to R≤∨ ; isMeet→≡∧ to isJoin→≡∨
+    ; ∧Comm to ∨Comm ; ∧Idem to ∨Idem ; ∧Assoc to ∨Assoc
+    ; ≤≃∧ to ≤≃∨ ; ≤→∧ to ≤→∨ ; ≤→∧≡Left to ≥→∨≡Left ; ≥→∧≡Right to ≤→∨≡Right
+    ; ∧GLB to ∨LUB ; Pseudolattice→Semigroup∧ to Pseudolattice→Semigroup∨)