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: Jan 29 2023 at 01:02 UTC