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 ?
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?
https://github.com/HoTT/HoTT/blob/master/STYLE.md#15-higher-inductive-types
Last updated: Oct 13 2024 at 01:02 UTC