search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
378 stars 22 forks source link

Definition of ordered field and real numbers #143

Open ghost opened 2 years ago

ghost commented 2 years ago

I assume that for the definition of an ordered field, we just lift the definition of ordered field from the HoTT book.

For defining the real numbers, are we looking for Dedekind completeness or Cauchy completeness (by Cauchy sequences) in the definition of the real numbers? The latter is not unique, but I don't know if we are assuming propositional resizing in this book, so for the time being I'm assuming that the former is also not unique.

DanGrayson commented 2 years ago

We discussed this on our zoom call this morning, and we don't really see an application for completeness to the topics in the book. Perhaps the following will suffice: we say that we let R be the field of real numbers, which the students have encountered in other courses, and list the properties we will need. It should be an ordered field, and positive elements should have square roots at least (so we can construct the icosahedron, whose vertices have coordinates involving the square root of 5). If we need other properties, we can add them at the time needed.

I'll write something soon and add it.