Niels van der Weide
Niels van der Weide
We start with `T_0` which is just Bool. For `T_1` we start with `T_0`. Since there are no recursive constructors, we don't add points. Then we add paths `p_1 :...
The paths lzero and lone are supposed to be there. We have the path `p : \prod x y : A, x = y`. They are the paths `p zero...
I was able to prove the introduction, elimination and computation rules, so the result is a mere proposition if my proof is correct. The introduction rule required the coherencies, and...
Similar argument. I used `S^1` because if you restrict it, it is a circle. We start with ``` Inductive T_1 = | a_1 : T_1 | b_1 : T_1 |...
At `T_(n+1)` we add paths `p : Π x y : T_n, i x = i y`. With these the path between `p one one` and `refl` are made.
> @mikeshulman suggested that the systematic use of `PathOver` (Mike also called it "displayed identity") could simplify definitions and constructions of displayed things. It would be great to try it...
One important thing here, is merging order. There are a couple of PRs that will be affected: - For https://github.com/UniMath/UniMath/pull/1843 and https://github.com/UniMath/UniMath/pull/1840: I think they can be merged rather quickly...
Recently, in Coq dev there was a patch in Coq dev that affected private inductive types (https://github.com/coq/coq/pull/9609). GrpdHITs was affected by it, because it uses private inductive types to implement...
> @nmvdw This is resolved now, right? Yes