-
Notifications
You must be signed in to change notification settings - Fork 136
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
Upper natural numbers #602
Conversation
…ded elements are preserved by the arithmetic operations
Also promote the rendered version in README w/ some adjectives stolen from the stdlib
# Conflicts: # Cubical/Algebra/CommMonoid/Base.agda # Cubical/Data/Nat/Order.agda
This reverts commit db795f0.
Ohno. That wasn't obsolete... I guess I should wake up first. |
Just in case there are any doubts: This PR still wants to be reviewed by @mortberg |
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.
Lots of minor comments. Sorry for forgetting to finish the review :-)
Cubical/Functions/Embedding.agda
Outdated
@@ -425,3 +425,17 @@ module EmbeddingIdentityPrinciple {B : Type ℓ} {ℓ₁} (f g : Embedding B ℓ | |||
f ≡ g | |||
■ | |||
open EmbeddingIdentityPrinciple renaming (f≃g to _≃Emb_) using (EmbeddingIP) public |
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.
Why open public?
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.
As far as I know, this is not code I wrote. Good question though.
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.
There is another instance of this in the file. Should I just change both?
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.
Yes, I guess that would be good
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.
Apart from the thing about the public imports I think this is ready to be merged! So please just fix that and check if the CI is still happy, then let's merge!
Should be good to merge now! (travelling...) |
This PR constructs the upper natural numbers. They complete the naturals in some sense. For example, every collection of upper naturals constructively has a minimal element. The goal of this PR is to construct arithmetic operations on the upper natural numbers