Properties of `Pseudolattice`#1272

Open

LorenzoMolena wants to merge 6 commits intoagda:masterfrom

LorenzoMolena:pseudolattice-properties

Commits on Nov 12, 2025

add fixity for `_≤_` in `PseudolatticeStr`, add `Properties` file
LorenzoMolena
committed

Commits on Nov 13, 2025

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

Commits on Nov 14, 2025

add equivalences of Pseudolattices and other basic properties, following similar modules
LorenzoMolena
committed
remove implicit universe levels in the type of `PseudolatticeEquiv`
LorenzoMolena
committed

Commits on Dec 13, 2025

remove global public export of `MeetProperties` and `JoinProperties` ; add module `PseudolatticeTheory` which export them
LorenzoMolena
committed

Commits on Dec 14, 2025

add export of `Pseudolattice.Property` in `Pseudolattice`
LorenzoMolena
committed