update makePseudolatticeFromPoset and instances built using it

Author: LorenzoMolena

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

@@ -65,11 +65,11 @@ module _
   (P : Poset ℓ ℓ') (_∧_ _∨_ : ⟨ P ⟩ → ⟨ P ⟩ → ⟨ P ⟩) where
   open PosetStr (str P) renaming (_≤_ to infix 8 _≤_)
   module _
-    (π₁ : ∀ {a b x} → x ≤ a ∧ b → x ≤ a)
-    (π₂ : ∀ {a b x} → x ≤ a ∧ b → x ≤ b)
+    (π₁ : ∀ {a b}   → a ∧ b ≤ a)
+    (π₂ : ∀ {a b}   → a ∧ b ≤ b)
     (ϕ  : ∀ {a b x} → x ≤ a → x ≤ b → x ≤ a ∧ b)
-    (ι₁ : ∀ {a b x} → a ∨ b ≤ x → a ≤ x)
-    (ι₂ : ∀ {a b x} → a ∨ b ≤ x → b ≤ x)
+    (ι₁ : ∀ {a b}   → a ≤ a ∨ b)
+    (ι₂ : ∀ {a b}   → b ≤ a ∨ b)
     (ψ  : ∀ {a b x} → a ≤ x → b ≤ x → a ∨ b ≤ x) where
 
     makePseudolatticeFromPoset : Pseudolattice ℓ ℓ'
@@ -82,11 +82,11 @@ module _
       isPL .IsPseudolattice.isPseudolattice .fst a b .snd x = propBiimpl→Equiv
         (is-prop-valued _ _)
         (isProp× (is-prop-valued _ _) (is-prop-valued _ _))
-        (λ x≤a∧b → π₁ x≤a∧b , π₂ x≤a∧b)
+        (λ x≤a∧b → is-trans _ _ _ x≤a∧b π₁ , is-trans _ _ _ x≤a∧b π₂)
         (uncurry ϕ)
       isPL .IsPseudolattice.isPseudolattice .snd a b .fst = a ∨ b
       isPL .IsPseudolattice.isPseudolattice .snd a b .snd x = propBiimpl→Equiv
         (is-prop-valued _ _)
         (isProp× (is-prop-valued _ _) (is-prop-valued _ _))
-        (λ a∨b≤x → ι₁ a∨b≤x , ι₂ a∨b≤x)
+        (λ a∨b≤x → is-trans _ _ _ ι₁ a∨b≤x , is-trans _ _ _ ι₂ a∨b≤x)
         (uncurry ψ)

Cubical/Relation/Binary/Order/Pseudolattice/Instances/Int.agda

@@ -12,9 +12,9 @@ open PseudolatticeStr
 
 ℤ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
 ℤ≤Pseudolattice = makePseudolatticeFromPoset ℤ≤Poset min max
-  (λ       x≤min → isTrans≤ x≤min min≤)
-  (λ {a b} x≤min → isTrans≤ x≤min (subst (_≤ℤ b) (minComm b a) min≤))
+  min≤
+  (λ {a b} → subst (_≤ℤ b) (minComm b a) min≤)
   (λ {a b} x≤a x≤b → subst (_≤ℤ min a b) (minIdem _) (≤MonotoneMin x≤a x≤b))
-  (λ       max≤x → isTrans≤ ≤max max≤x)
-  (λ {a b} max≤x → isTrans≤ (subst (b ≤ℤ_) (maxComm b a) ≤max) max≤x)
+  ≤max
+  (λ {a b} → subst (b ≤ℤ_) (maxComm b a) ≤max)
   (λ {a b} a≤x b≤x → subst (max a b ≤ℤ_) (maxIdem _) (≤MonotoneMax a≤x b≤x))

Cubical/Relation/Binary/Order/Pseudolattice/Instances/Nat.agda

@@ -29,9 +29,9 @@ private
 
 ℕ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
 ℕ≤Pseudolattice = makePseudolatticeFromPoset ℕ≤Poset min max
-  (λ       x≤min → ≤-trans x≤min min-≤-left)
-  (λ {a b} x≤min → ≤-trans x≤min (min-≤-right {a} {b}))
+  min-≤-left
+  (λ {a b} → min-≤-right {a} {b})
   minGLB
-  (λ       max≤x → ≤-trans left-≤-max max≤x)
-  (λ {a b} max≤x → ≤-trans (right-≤-max {b} {a}) max≤x)
+  left-≤-max
+  (λ {a b} → right-≤-max {b} {a})
   maxLUB