Skip to content

Properties of Pseudolattice #1272

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
LorenzoMolena wants to merge 6 commits into
base: master
Choose a base branch
from
+235 −3
Open

Properties of Pseudolattice #1272

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
bb72c98
add fixity for `_≤_` in `PseudolatticeStr`, add `Properties` file
LorenzoMolena Nov 12, 2025
1abebbf
add `≤→∧≡Left` and `≥→∧≡Right` into the `Properties` module. Add `isP…
LorenzoMolena Nov 13, 2025
f32b9c8
add equivalences of Pseudolattices and other basic properties, follow…
LorenzoMolena Nov 14, 2025
9ffd711
remove implicit universe levels in the type of `PseudolatticeEquiv`
LorenzoMolena Nov 14, 2025
4a2eba9
remove global public export of `MeetProperties` and `JoinProperties` …
LorenzoMolena Dec 13, 2025
5b03cc3
add export of `Pseudolattice.Property` in `Pseudolattice`
LorenzoMolena Dec 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cubical/Relation/Binary/Order/Pseudolattice.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
module Cubical.Relation.Binary.Order.Pseudolattice where

open import Cubical.Relation.Binary.Order.Pseudolattice.Base public
open import Cubical.Relation.Binary.Order.Pseudolattice.Properties public
101 changes: 98 additions & 3 deletions Cubical/Relation/Binary/Order/Pseudolattice/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,17 +1,29 @@
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.Reflection.StrictEquiv

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

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

private
variable
ℓ ℓ' : Level
ℓ ℓ' ℓ₀ ℓ₀' ℓ₁ ℓ₁' : Level

record IsPseudolattice {L : Type ℓ} (_≤_ : L → L → Type ℓ') : Type (ℓ-max ℓ ℓ') where
constructor ispseudolattice
Expand All @@ -31,15 +43,23 @@ 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

field
_≤_ : L → L → Type ℓ'
is-pseudolattice : IsPseudolattice _≤_

infix 5 _≤_

open IsPseudolattice is-pseudolattice public


unquoteDecl PseudolatticeStrIsoΣ = declareRecordIsoΣ PseudolatticeStrIsoΣ (quote PseudolatticeStr)

Pseudolattice : ∀ ℓ ℓ' → Type (ℓ-suc (ℓ-max ℓ ℓ'))
Pseudolattice ℓ ℓ' = TypeWithStr ℓ (PseudolatticeStr ℓ')

Expand All @@ -57,3 +77,78 @@ 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


record IsPseudolatticeEquiv {A : Type ℓ₀} {B : Type ℓ₁}
(M : PseudolatticeStr ℓ₀' A) (e : A ≃ B) (N : PseudolatticeStr ℓ₁' B)
: Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁')
where
constructor
ispseudolatticeequiv
-- Shorter qualified names
private
module M = PseudolatticeStr M
module N = PseudolatticeStr N

field
pres≤ : (x y : A) → x M.≤ y ≃ equivFun e x N.≤ equivFun e y


PseudolatticeEquiv : (M : Pseudolattice ℓ₀ ℓ₀') (N : Pseudolattice ℓ₁ ℓ₁')
→ Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') (ℓ-max ℓ₁ ℓ₁'))
PseudolatticeEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsPseudolatticeEquiv (M .snd) e (N .snd)

isPropIsPseudolattice : {L : Type ℓ} (_≤_ : L → L → Type ℓ') → isProp (IsPseudolattice _≤_)
isPropIsPseudolattice {L = L} _≤_ = isOfHLevelRetractFromIso 1
IsPseudolatticeIsoΣ $ isPropΣ
(isPropIsPoset _≤_) λ isPoset →
is-prop-is-pseudolattice (poset L _≤_ isPoset)

𝒮ᴰ-Pseudolattice : DUARel (𝒮-Univ ℓ) (PseudolatticeStr ℓ') (ℓ-max ℓ ℓ')
𝒮ᴰ-Pseudolattice =
𝒮ᴰ-Record (𝒮-Univ _) IsPseudolatticeEquiv
(fields:
data[ _≤_ ∣ autoDUARel _ _ ∣ pres≤ ]
prop[ is-pseudolattice ∣ (λ _ _ → isPropIsPseudolattice _) ])
where
open PseudolatticeStr
open IsPseudolattice
open IsPseudolatticeEquiv

PseudolatticePath : (M N : Pseudolattice ℓ ℓ') → PseudolatticeEquiv M N ≃ (M ≡ N)
PseudolatticePath = ∫ 𝒮ᴰ-Pseudolattice .UARel.ua

-- an easier way of establishing an equivalence of pseudolattices
module _ {P : Pseudolattice ℓ₀ ℓ₀'} {S : Pseudolattice ℓ₁ ℓ₁'} (e : ⟨ P ⟩ ≃ ⟨ S ⟩) where
private
module P = PseudolatticeStr (P .snd)
module S = PseudolatticeStr (S .snd)

module _ (isMon : ∀ x y → x P.≤ y → equivFun e x S.≤ equivFun e y)
(isMonInv : ∀ x y → x S.≤ y → invEq e x P.≤ invEq e y) where
open IsPseudolatticeEquiv
open IsPseudolattice

makeIsPseudolatticeEquiv : IsPseudolatticeEquiv (P .snd) e (S .snd)
pres≤ makeIsPseudolatticeEquiv x y = propBiimpl→Equiv
(P.is-pseudolattice .is-prop-valued _ _)
(S.is-pseudolattice .is-prop-valued _ _)
(isMon _ _) (isMonInv' _ _)
where
isMonInv' : ∀ x y → equivFun e x S.≤ equivFun e y → x P.≤ y
isMonInv' x y ex≤ey = transport (λ i → retEq e x i P.≤ retEq e y i) (isMonInv _ _ ex≤ey)


module PseudolatticeReasoning (P' : Pseudolattice ℓ ℓ') where
private P = fst P'
open PseudolatticeStr (snd P')
open IsPseudolattice

_≤⟨_⟩_ : (x : P) {y z : P} → x ≤ y → y ≤ z → x ≤ z
x ≤⟨ p ⟩ q = is-pseudolattice .is-trans x _ _ p q

_◾ : (x : P) → x ≤ x
x ◾ = is-pseudolattice .is-refl x

infixr 0 _≤⟨_⟩_
infix 1 _◾
136 changes: 136 additions & 0 deletions Cubical/Relation/Binary/Order/Pseudolattice/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,136 @@
module Cubical.Relation.Binary.Order.Pseudolattice.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Binary.Order.Proset
open import Cubical.Relation.Binary.Order.Poset renaming (isPseudolattice to pseudolattice)
open import Cubical.Relation.Binary.Order.Quoset

open import Cubical.Relation.Binary.Order.Pseudolattice.Base

open import Cubical.Relation.Nullary

open import Cubical.Algebra.Semigroup

private
variable
ℓ ℓ' ℓ'' : Level

module _
{A : Type ℓ}
{R : Rel A A ℓ'}
where

open BinaryRelation
open IsPseudolattice

isPseudolattice→isPoset : IsPseudolattice R → IsPoset R
isPseudolattice→isPoset = isPoset

isPseudolattice→isProset : IsPseudolattice R → IsProset R
isPseudolattice→isProset = isPoset→isProset ∘ isPoset

isPseudolatticeDecidable→Discrete : IsPseudolattice R → isDecidable R → Discrete A
isPseudolatticeDecidable→Discrete = isPosetDecidable→Discrete ∘ isPoset

isPseudolattice→isQuosetIrreflKernel : IsPseudolattice R → IsQuoset (IrreflKernel R)
isPseudolattice→isQuosetIrreflKernel = isPoset→isQuosetIrreflKernel ∘ isPoset

isPseudolatticeDecidable→isQuosetDecidable : IsPseudolattice R → isDecidable R → isDecidable (IrreflKernel R)
isPseudolatticeDecidable→isQuosetDecidable = isPosetDecidable→isQuosetDecidable ∘ isPoset

isPseudolatticeDual : IsPseudolattice R → IsPseudolattice (Dual R)
isPseudolatticeDual pl .isPoset = isPosetDual (isPoset pl)
isPseudolatticeDual pl .isPseudolattice .fst = pl .isPseudolattice .snd
isPseudolatticeDual pl .isPseudolattice .snd = pl .isPseudolattice .fst

Pseudolattice→Proset : Pseudolattice ℓ ℓ' → Proset ℓ ℓ'
Pseudolattice→Proset (_ , pl) = proset _ _ (isPoset→isProset isPoset)
where open PseudolatticeStr pl

Pseudolattice→Poset : Pseudolattice ℓ ℓ' → Poset ℓ ℓ'
Pseudolattice→Poset (_ , pl) = poset _ _ isPoset
where open PseudolatticeStr pl

Pseudolattice→Quoset : Pseudolattice ℓ ℓ' → Quoset ℓ (ℓ-max ℓ ℓ')
Pseudolattice→Quoset (_ , pl) = quoset _ _ (isPoset→isQuosetIrreflKernel isPoset)
where open PseudolatticeStr pl

DualPseudolattice : Pseudolattice ℓ ℓ' → Pseudolattice ℓ ℓ'
DualPseudolattice (_ , pl) = _ , pseudolatticestr _ (isPseudolatticeDual is-pseudolattice)
where open PseudolatticeStr pl

module MeetProperties (L≤ : Pseudolattice ℓ ℓ') where
private
L = L≤ .fst
open PseudolatticeStr (L≤ .snd)
variable
a b c x : L

isMeet∧ : ∀ {a b x} → x ≤ (a ∧l b) ≃ (x ≤ a) × (x ≤ b)
isMeet∧ {a} {b} {x} = isPseudolattice .fst a b .snd x

∧≤L : (a ∧l b) ≤ a
∧≤L = equivFun isMeet∧ (is-refl _) .fst

∧≤R : (a ∧l b) ≤ b
∧≤R = equivFun isMeet∧ (is-refl _) .snd

∧GLB : ∀ {a b x} → x ≤ a → x ≤ b → x ≤ a ∧l b
∧GLB = curry (invEq isMeet∧)

isMeet→≡∧ : ∀ m
→ (∀ {x} → x ≤ m → x ≤ a)
→ (∀ {x} → x ≤ m → x ≤ b)
→ (∀ {x} → x ≤ a → x ≤ b → x ≤ m)
→ a ∧l b ≡ m
isMeet→≡∧ {a = a} {b = b} m l r u =
fst $ PathPΣ $ MeetUnique isPoset a b (isPseudolattice .fst a b) $
m , λ x → propBiimpl→Equiv (is-prop-valued _ _)
(isProp× (is-prop-valued _ _) (is-prop-valued _ _))
(λ x≤m → l x≤m , r x≤m)
(uncurry u)

∧Idem : a ∧l a ≡ a
∧Idem = meetIdemp isPoset (isPseudolattice .fst) _

∧Comm : a ∧l b ≡ b ∧l a
∧Comm = meetComm isPoset (isPseudolattice .fst) _ _

∧Assoc : a ∧l (b ∧l c) ≡ (a ∧l b) ∧l c
∧Assoc = meetAssoc isPoset (isPseudolattice .fst) _ _ _

≤≃∧ : (a ≤ b) ≃ (a ≡ a ∧l b)
≤≃∧ = order≃meet isPoset _ _ _ λ _ → isMeet∧

≤→∧ : a ≤ b → a ≡ a ∧l b
≤→∧ = 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
Pseudolattice→Semigroup∧ .snd .SemigroupStr._·_ = _∧l_
Pseudolattice→Semigroup∧ .snd .SemigroupStr.isSemigroup =
issemigroup is-set (λ _ _ _ → ∧Assoc)

module JoinProperties (L≤ : Pseudolattice ℓ ℓ') where
open MeetProperties (DualPseudolattice L≤) public renaming (
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∨)

module PseudolatticeTheory (L≤ : Pseudolattice ℓ ℓ') where
open MeetProperties L≤ public
open JoinProperties L≤ public