Skip to content

Commit f32b9c8

Browse files
LorenzoMolenaLorenzoMolena
committed
add equivalences of Pseudolattices and other basic properties, following similar modules
1 parent 1abebbf commit f32b9c8

File tree

2 files changed

+127
-15
lines changed

2 files changed

+127
-15
lines changed

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

Lines changed: 77 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,12 @@ open import Cubical.Foundations.HLevels
77
open import Cubical.Foundations.SIP
88

99
open import Cubical.Reflection.RecordEquiv
10+
open import Cubical.Reflection.StrictEquiv
11+
12+
open import Cubical.Displayed.Base
13+
open import Cubical.Displayed.Auto
14+
open import Cubical.Displayed.Record
15+
open import Cubical.Displayed.Universe
1016

1117
open import Cubical.Relation.Binary.Base
1218
open import Cubical.Relation.Binary.Order.Poset renaming (
@@ -17,7 +23,7 @@ open BinaryRelation
1723

1824
private
1925
variable
20-
ℓ ℓ' : Level
26+
ℓ ℓ' ℓ₀ ℓ₀' ℓ₁ ℓ₁' : Level
2127

2228
record IsPseudolattice {L : Type ℓ} (_≤_ : L → L → Type ℓ') : Type (ℓ-max ℓ ℓ') where
2329
constructor ispseudolattice
@@ -72,8 +78,78 @@ makeIsPseudolattice {_≤_ = _≤_} is-setL is-prop-valued is-refl is-trans is-a
7278
PS .IsPseudolattice.isPoset = isposet is-setL is-prop-valued is-refl is-trans is-antisym
7379
PS .IsPseudolattice.isPseudolattice = is-meet-semipseudolattice , is-join-semipseudolattice
7480

81+
82+
record IsPseudolatticeEquiv {A : Type ℓ₀} {B : Type ℓ₁}
83+
(M : PseudolatticeStr ℓ₀' A) (e : A ≃ B) (N : PseudolatticeStr ℓ₁' B)
84+
: Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁')
85+
where
86+
constructor
87+
ispseudolatticeequiv
88+
-- Shorter qualified names
89+
private
90+
module M = PseudolatticeStr M
91+
module N = PseudolatticeStr N
92+
93+
field
94+
pres≤ : (x y : A) → x M.≤ y ≃ equivFun e x N.≤ equivFun e y
95+
96+
97+
PseudolatticeEquiv : ∀ {ℓ₀ ℓ₀' ℓ₁ ℓ₁'}
98+
→ (M : Pseudolattice ℓ₀ ℓ₀') (N : Pseudolattice ℓ₁ ℓ₁')
99+
→ Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') (ℓ-max ℓ₁ ℓ₁'))
100+
PseudolatticeEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsPseudolatticeEquiv (M .snd) e (N .snd)
101+
75102
isPropIsPseudolattice : {L : Type ℓ} (_≤_ : L → L → Type ℓ') → isProp (IsPseudolattice _≤_)
76103
isPropIsPseudolattice {L = L} _≤_ = isOfHLevelRetractFromIso 1
77104
IsPseudolatticeIsoΣ $ isPropΣ
78105
(isPropIsPoset _≤_) λ isPoset →
79106
is-prop-is-pseudolattice (poset L _≤_ isPoset)
107+
108+
𝒮ᴰ-Pseudolattice : DUARel (𝒮-Univ ℓ) (PseudolatticeStr ℓ') (ℓ-max ℓ ℓ')
109+
𝒮ᴰ-Pseudolattice =
110+
𝒮ᴰ-Record (𝒮-Univ _) IsPseudolatticeEquiv
111+
(fields:
112+
data[ _≤_ ∣ autoDUARel _ _ ∣ pres≤ ]
113+
prop[ is-pseudolattice ∣ (λ _ _ → isPropIsPseudolattice _) ])
114+
where
115+
open PseudolatticeStr
116+
open IsPseudolattice
117+
open IsPseudolatticeEquiv
118+
119+
PseudolatticePath : (M N : Pseudolattice ℓ ℓ') → PseudolatticeEquiv M N ≃ (M ≡ N)
120+
PseudolatticePath = ∫ 𝒮ᴰ-Pseudolattice .UARel.ua
121+
122+
-- an easier way of establishing an equivalence of pseudolattices
123+
module _ {P : Pseudolattice ℓ₀ ℓ₀'} {S : Pseudolattice ℓ₁ ℓ₁'} (e : ⟨ P ⟩ ≃ ⟨ S ⟩) where
124+
private
125+
module P = PseudolatticeStr (P .snd)
126+
module S = PseudolatticeStr (S .snd)
127+
128+
module _ (isMon : ∀ x y → x P.≤ y → equivFun e x S.≤ equivFun e y)
129+
(isMonInv : ∀ x y → x S.≤ y → invEq e x P.≤ invEq e y) where
130+
open IsPseudolatticeEquiv
131+
open IsPseudolattice
132+
133+
makeIsPseudolatticeEquiv : IsPseudolatticeEquiv (P .snd) e (S .snd)
134+
pres≤ makeIsPseudolatticeEquiv x y = propBiimpl→Equiv
135+
(P.is-pseudolattice .is-prop-valued _ _)
136+
(S.is-pseudolattice .is-prop-valued _ _)
137+
(isMon _ _) (isMonInv' _ _)
138+
where
139+
isMonInv' : ∀ x y → equivFun e x S.≤ equivFun e y → x P.≤ y
140+
isMonInv' x y ex≤ey = transport (λ i → retEq e x i P.≤ retEq e y i) (isMonInv _ _ ex≤ey)
141+
142+
143+
module PseudolatticeReasoning (P' : Pseudolattice ℓ ℓ') where
144+
private P = fst P'
145+
open PseudolatticeStr (snd P')
146+
open IsPseudolattice
147+
148+
_≤⟨_⟩_ : (x : P) {y z : P} → x ≤ y → y ≤ z → x ≤ z
149+
x ≤⟨ p ⟩ q = is-pseudolattice .is-trans x _ _ p q
150+
151+
_◾ : (x : P) → x ≤ x
152+
x ◾ = is-pseudolattice .is-refl x
153+
154+
infixr 0 _≤⟨_⟩_
155+
infix 1 _◾

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

Lines changed: 50 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8,29 +8,63 @@ open import Cubical.Foundations.HLevels
88
open import Cubical.Data.Sigma
99

1010
open import Cubical.Relation.Binary.Base
11+
open import Cubical.Relation.Binary.Order.Proset
1112
open import Cubical.Relation.Binary.Order.Poset renaming (isPseudolattice to pseudolattice)
13+
open import Cubical.Relation.Binary.Order.Quoset
1214

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

15-
open import Cubical.Algebra.Semigroup
17+
open import Cubical.Relation.Nullary
1618

17-
open BinaryRelation
19+
open import Cubical.Algebra.Semigroup
1820

1921
private
2022
variable
21-
ℓ ℓ' : Level
23+
ℓ ℓ' ℓ'' : Level
2224

23-
DualPseudolattice : Pseudolattice ℓ ℓ' → Pseudolattice ℓ ℓ'
24-
DualPseudolattice L .fst = L .fst
25-
DualPseudolattice L .snd .PseudolatticeStr._≤_ = Dual (L .snd .PseudolatticeStr._≤_)
26-
DualPseudolattice L .snd .PseudolatticeStr.is-pseudolattice = isPL
25+
module _
26+
{A : Type ℓ}
27+
{R : Rel A A ℓ'}
2728
where
28-
open module L≤ = PseudolatticeStr (L .snd)
29-
open IsPseudolattice
30-
isPL : IsPseudolattice _
31-
isPL .isPoset = isPosetDual L≤.isPoset
32-
isPL .isPseudolattice .fst = L≤.isPseudolattice .snd
33-
isPL .isPseudolattice .snd = L≤.isPseudolattice .fst
29+
30+
open BinaryRelation
31+
open IsPseudolattice
32+
33+
isPseudolattice→isPoset : IsPseudolattice R → IsPoset R
34+
isPseudolattice→isPoset = isPoset
35+
36+
isPseudolattice→isProset : IsPseudolattice R → IsProset R
37+
isPseudolattice→isProset = isPoset→isProset ∘ isPoset
38+
39+
isPseudolatticeDecidable→Discrete : IsPseudolattice R → isDecidable R → Discrete A
40+
isPseudolatticeDecidable→Discrete = isPosetDecidable→Discrete ∘ isPoset
41+
42+
isPseudolattice→isQuosetIrreflKernel : IsPseudolattice R → IsQuoset (IrreflKernel R)
43+
isPseudolattice→isQuosetIrreflKernel = isPoset→isQuosetIrreflKernel ∘ isPoset
44+
45+
isPseudolatticeDecidable→isQuosetDecidable : IsPseudolattice R → isDecidable R → isDecidable (IrreflKernel R)
46+
isPseudolatticeDecidable→isQuosetDecidable = isPosetDecidable→isQuosetDecidable ∘ isPoset
47+
48+
isPseudolatticeDual : IsPseudolattice R → IsPseudolattice (Dual R)
49+
isPseudolatticeDual pl .isPoset = isPosetDual (isPoset pl)
50+
isPseudolatticeDual pl .isPseudolattice .fst = pl .isPseudolattice .snd
51+
isPseudolatticeDual pl .isPseudolattice .snd = pl .isPseudolattice .fst
52+
53+
Pseudolattice→Proset : Pseudolattice ℓ ℓ' → Proset ℓ ℓ'
54+
Pseudolattice→Proset (_ , pl) = proset _ _ (isPoset→isProset isPoset)
55+
where open PseudolatticeStr pl
56+
57+
Pseudolattice→Poset : Pseudolattice ℓ ℓ' → Poset ℓ ℓ'
58+
Pseudolattice→Poset (_ , pl) = poset _ _ isPoset
59+
where open PseudolatticeStr pl
60+
61+
Pseudolattice→Quoset : Pseudolattice ℓ ℓ' → Quoset ℓ (ℓ-max ℓ ℓ')
62+
Pseudolattice→Quoset (_ , pl) = quoset _ _ (isPoset→isQuosetIrreflKernel isPoset)
63+
where open PseudolatticeStr pl
64+
65+
DualPseudolattice : Pseudolattice ℓ ℓ' → Pseudolattice ℓ ℓ'
66+
DualPseudolattice (_ , pl) = _ , pseudolatticestr _ (isPseudolatticeDual is-pseudolattice)
67+
where open PseudolatticeStr pl
3468

3569
module MeetProperties (L≤ : Pseudolattice ℓ ℓ') where
3670
private
@@ -92,9 +126,11 @@ module MeetProperties (L≤ : Pseudolattice ℓ ℓ') where
92126

93127
open MeetProperties public
94128

95-
module _ (L≤ : Pseudolattice ℓ ℓ') where
129+
module JoinProperties (L≤ : Pseudolattice ℓ ℓ') where
96130
open MeetProperties (DualPseudolattice L≤) public renaming (
97131
isMeet∧ to isJoin∨ ; ∧≤L to L≤∨ ; ∧≤R to R≤∨ ; isMeet→≡∧ to isJoin→≡∨
98132
; ∧Comm to ∨Comm ; ∧Idem to ∨Idem ; ∧Assoc to ∨Assoc
99133
; ≤≃∧ to ≤≃∨ ; ≤→∧ to ≤→∨ ; ≤→∧≡Left to ≥→∨≡Left ; ≥→∧≡Right to ≤→∨≡Right
100134
; ∧GLB to ∨LUB ; Pseudolattice→Semigroup∧ to Pseudolattice→Semigroup∨)
135+
136+
open JoinProperties public

0 commit comments

Comments
 (0)