Book cauchy reals#1182

Draft

marcinjangrzybowski wants to merge 34 commits intoagda:masterfrom

marcinjangrzybowski:book-cauchy-reals

Commits on Nov 19, 2025

Commits on Nov 22, 2025

edit `zero-≤pos`, using an easier proof, add `zero-<possuc`
LorenzoMolena
committed

Commits on Nov 23, 2025

rebased, but I nedd to remove few more files with experiments before updating PR
marcinjangrzybowski
committed
fix defintions of `min` and `max`, add comment on limitations of `UsingEq` (#26)
LorenzoMolena
authored
add instances of `Nat` and `Int` as `Pseudolattice`s, and of `Int` as `OrderedCommRing` (#28)
LorenzoMolena
authored
Pseudolattice properties for cauchy rebase (#29)
LorenzoMolena
authored
Fast int update for cauchy rebase (#30)

authored
comment `sign`, `sign·abs` (they are duplicated), fix import on `Nat.Order`, add `0<` and its property into `Int.Fast.Order`, add Fast Rationals. The module `Rationals.Fast.Order.Properties` is sti…
LorenzoMolena
committed
`Rational.Fast.Order.Properties`: until `equivInvℚ₊`, every except `floor-frac` typechecks
LorenzoMolena
committed
removed underdeveloped files
marcinjangrzybowski
committed
Merge remote-tracking branch 'lorenzo/cauchy--rebase-fast' into cauchy--rebased
marcinjangrzybowski
committed
whitespace fix
marcinjangrzybowski
committed
small fix
marcinjangrzybowski
committed
Merge branch 'agda:master' into cauchy--rebased
marcinjangrzybowski
authored

Commits on Nov 24, 2025

remove underdeveloped file
marcinjangrzybowski
committed

Commits on Nov 29, 2025

reals - order, got rid of lossy unification, and aplied solver
marcinjangrzybowski
committed

Commits on Dec 5, 2025

Commits on Dec 7, 2025

Commits on Dec 10, 2025

solver for reals, more robust solver for rationals, inverse real, and nth root of reals without laousy unification and using solvers
marcinjangrzybowski
committed