-
Notifications
You must be signed in to change notification settings - Fork 134
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.
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
Dl sheaves properly ordered #788
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just two tiny comments, then I'd be happy to merge
module _ (x y : L .fst)where | ||
hom-∨₁ : DLCat [ x , x ∨l y ] | ||
hom-∨₁ = ∨≤RCancel _ _ | ||
-- TODO: isn't the fixity of the operators a bit weird? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's not clear to me what this comment is about?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I gave meet and join the same fixity as both distribute over each other
hom-∨₂ = ∨≤LCancel _ _ | ||
|
||
hom-∧₁ : DLCat [ x ∧l y , x ] | ||
hom-∧₁ = (≤m→≤j _ _ (∧≤RCancel _ _)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No need for parenthesis in definition
hom-∧₁ = (≤m→≤j _ _ (∧≤RCancel _ _)) | ||
|
||
hom-∧₂ : DLCat [ x ∧l y , y ] | ||
hom-∧₂ = (≤m→≤j _ _ (∧≤LCancel _ _)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No need for parenthesis in definition
This PR contains the correct definition of sheaf on a basis of a distributive lattice. It doesn't contain any particularly interesting results yet (i.e. lifting to a sheaf on the whole lattice) but I thought I'll put it in the library before we start applying the new naming conventions everywhere.