Stream: Miscellaneous

Topic: Cauchy real in coq-hott


view this post on Zulip vlj (Sep 16 2020 at 11:50):

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

view this post on Zulip Bas Spitters (Sep 16 2020 at 12:35):

The work by @Gaƫtan Gilbert
https://arxiv.org/abs/1610.05072

view this post on Zulip Bas Spitters (Sep 16 2020 at 12:42):

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


Last updated: Aug 19 2022 at 19:03 UTC