search

HoTT / book

A textbook on informal homotopy type theory
2.04k stars 360 forks source link

Inverse of a Dedekind real #1130

Closed valis closed 1 year ago

valis commented 2 years ago

Fixes the definition of an inverse of a Dedekind real

mikeshulman commented 2 years ago

We discussed this on Zulip and it looks necessary and correct to me. Any other opinions, e.g. @andrejbauer?