Hi, is there an exemple of cauchy real implementation using coq-hott ? in particular (** Definition 11.3.2 *) is empty here https://github.com/HoTT/HoTT/blob/master/contrib/HoTTBook.v

The work by @GaĆ«tan Gilbert

https://arxiv.org/abs/1610.05072

https://github.com/HoTT/HoTT/blob/master/theories/Classes/interfaces/cauchy.v

Last updated: Jan 29 2023 at 08:28 UTC