Stream: Coq users

Topic: Is there a way to represent Intervals as inductive types?


view this post on Zulip walker (Sep 13 2022 at 10:50):

Question says it all, this is the intervals I am trying to see how can they be done:
image.png

From my basic knowledge, 0 = 1: I feels like it breaks the inversion principle in Coq, so if one tried to formalize that and assuming that induction types are not going to work, what will be the way to go ?

view this post on Zulip walker (Sep 13 2022 at 11:04):

Edit: I found this:

Private Inductive interval : Type0 :=
  | zero : interval
  | one : interval.

Axiom seg : zero = one.

here: https://hott.github.io/HoTT/proviola-html/HoTT.HIT.Interval.html

This looks scary, doesn't seg -> False already?

view this post on Zulip Gaƫtan Gilbert (Sep 13 2022 at 11:16):

https://github.com/HoTT/HoTT/blob/master/STYLE.md#15-higher-inductive-types


Last updated: Jan 29 2023 at 01:02 UTC