Lattices and posets #593
Lattices and posets #593
Conversation
| ∨l-rdist-∧l : ∀ x y z → (y ∧l z) ∨l x ≡ (y ∨l x) ∧l (z ∨l x) | ||
| ∨l-rdist-∧l x y z = ∨l-comm _ x ∙∙ ∨l-ldist-∧l _ _ _ ∙∙ cong₂ (_∧l_) (∨l-comm _ _) (∨l-comm _ _) | ||
|
|
||
| makeDistLattice : {L : Type ℓ} (0l 1l : L) (_∨l_ _∧l_ : L → L → L) |
There was a problem hiding this comment.
Wouldn't it be nicer with an anonymous module here with makeIsDistLattice and makeDistLattice so that you don't have to write the long list of parameters twice?
There was a problem hiding this comment.
That's a good idea, I think we should do that for all the structures in the algebra library.
Had to make the arguments 0l 1l _∨l_ _∧l_ implicit in makeDistLattice but I think that's even better anyways
There was a problem hiding this comment.
I also made two versions of makeIsDistLattice.
| open DistLatticeStr (snd L') | ||
|
|
||
| δ : {n : ℕ} (i j : Fin n) → L | ||
| δ i j = if i == j then 1l else 0l |
There was a problem hiding this comment.
Maybe there should be a more general delta operation which takes the zero and one?
There was a problem hiding this comment.
like δ x y i j = if i == j then x else y?
| (makeIsSemilattice is-setL ∧l-assoc ∧l-rid ∧l-lid ∧l-comm ∧l-idem) | ||
| λ x y → ∨l-absorb-∧l x y , ∧l-absorb-∨l x y | ||
|
|
||
| makeLattice : {L : Type ℓ} (0l 1l : L) (_∨l_ _∧l_ : L → L → L) |
There was a problem hiding this comment.
Share parameters with makeIsLattice by using an anonymous module?
| @@ -0,0 +1,191 @@ | |||
| {- | |||
| following Johnstone we define semilattices to be commutative monoids | |||
There was a problem hiding this comment.
Add a ref to the Johnstone book?
| makeIsCommMonoid is-setL assoc rid lid comm | ||
| IsSemilattice.idem (makeIsSemilattice is-setL assoc rid lid comm idem) = idem | ||
|
|
||
| makeSemilattice : {L : Type ℓ} (ε : L) (_·_ : L → L → L) |
There was a problem hiding this comment.
Share parameters with makeIsSemilattice?
| @@ -0,0 +1,326 @@ | |||
| {- | |||
| This an earlier formalization of posets using the old SIP instead of DURGs | |||
There was a problem hiding this comment.
Please add this to Cubical.Experiments.Everything
|
Converted back to draft because I'm really not sure about whether we should have anonymous modules for the |
This PR adds all the algebraic structures needed to define distributive lattices and rewrites the file on Posets.