search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Well-orderings and Ordinals #1072

Closed LuuBluum closed 6 months ago

LuuBluum commented 9 months ago

Defines well-ordered sets, their various properties, as well as a definition of ordinals and some ordinal arithmetic (namely, successor, addition, and multiplication; exponentiation will have to wait).

felixwellen commented 9 months ago

Please rebase/merge master

LuuBluum commented 7 months ago

Sorry for the long wait (it does help if PRs are shorter) and thanks for contributing! Apart from some details which I commented on, I do not know how your PR relates to the literature. @iblech kindly pointed me to this article (not the only one on the topic): https://arxiv.org/pdf/2301.10696.pdf which also comes with an agda formalization and an equivalent definition of ordinal. You should add pointers to the literature and comment on the relation of your formalization and others (e.g. if it is independet/inspired/partially copied).

Oh, to explain that, this is identical to the formalization done in the HoTT book, outside of the bit at the end for ordinal suprema which I did cite my source. Looks like I forgot to mention that at the top of the file; I can rectify that without issue.

felixwellen commented 7 months ago

Good - that would be great!

felixwellen commented 6 months ago

Looks all good to me now! -> merging.