Conversation
mortberg
left a comment
mortberg
left a comment
There was a problem hiding this comment.
A few small comments to fix and then we can merge
| isIdemRing R = ∀ (r : ⟨ R ⟩) → (str R) .CommRingStr._·_ r r ≡ r | ||
|
|
||
| idemCommRing→BR : {ℓ : Level} (R : CommRing ℓ) → isIdemRing R → BooleanRing ℓ | ||
| idemCommRing→BR R idem = ⟨ R ⟩ , |
There was a problem hiding this comment.
Can you please use copattern-matching instead? (C-c C-c is your friend)
| BoolBRStr ._+_ = _⊕_ | ||
| BoolBRStr ._·_ = _and_ | ||
| BoolBRStr .-_ x = x | ||
| BoolBRStr .isBooleanRing = record |
| BoolBR = Bool , BoolBRStr | ||
|
|
||
| BoolCR : CommRing ℓ-zero | ||
| BoolCR = BooleanRing→CommRing BoolBR |
There was a problem hiding this comment.
Shouldn't this go in https://github.com/agda/cubical/tree/master/Cubical/Algebra/CommRing/Instances ?
| } | ||
|
|
||
| BoolBR : BooleanRing ℓ-zero | ||
| BoolBR = Bool , BoolBRStr |
There was a problem hiding this comment.
Maybe have a specific BooleanRing.Instances folder and put this and BoolBRStr in a dedicated file there? (Then you can remove the anonymous module as well and just open BooleanStr (which should maybe be called BooleanRingStr?))
mortberg
left a comment
mortberg
left a comment
There was a problem hiding this comment.
One tiny comment and then I'll merge
| BooleanStr→CommRingStr : { A : Type ℓ } → BooleanStr A → CommRingStr A | ||
| BooleanStr→CommRingStr x = record { isCommRing = IsBooleanRing.isCommRing (BooleanStr.isBooleanRing x) } | ||
| BooleanRingStr→CommRingStr : { A : Type ℓ } → BooleanRingStr A → CommRingStr A | ||
| BooleanRingStr→CommRingStr x = record { isCommRing = IsBooleanRing.isCommRing (BooleanRingStr.isBooleanRing x) } |
There was a problem hiding this comment.
Oops, I had missed this use of record. Can you please change it just for consistency with the rest of the library?
There was a problem hiding this comment.
Of course! I think you only missed it because it comes from an earlier PR (#1146), and was only changed now because of the name change.
There was a problem hiding this comment.
I guess you can put it in a header at the top of the file if you want?
There was a problem hiding this comment.
Thanks! He wrote these parts in order to write about presentable Boolean algebras. I hope to soon make a PR on presentable Boolean algebras, and will give the credits in a file where these parts come together. That feels more manageable then putting headers in each part.
There was a problem hiding this comment.
Ok, great. Then I'll merge!
2 participants
Replaces #1234