Well-orderings and Ordinals #1072
Conversation
Also added the statement that WellFounded is a prop
Defined operations on ordinals; exponentation remains to be defined.
|
Please rebase/merge master |
There was a problem hiding this comment.
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).
| @@ -72,19 +75,20 @@ elim2 Cset f (squash₂ x y p q i j) z = | |||
| -- (λ a → elim (λ _ → Cset _ _) (f a)) | |||
|
|
|||
| -- TODO: generalize | |||
There was a problem hiding this comment.
I guess this comment can go.
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. |
|
Good - that would be great! |
|
Looks all good to me now! -> merging. |
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).