Closed inexxt closed 3 years ago
The zeroth one is not necessarily the HIT, in the HIT the point and path constructors are generated recursively. Using nil
instead of w
is too weak a generator. It is true that the path space of the HIT satisfies the equations of the relation you wrote.
Ok, changed the back to w. It respects cons by default, right?
The interface is to connect to the part of the proof with Pi transpositions, and to easily fit it in the FSMG part (e.g. when doing encode/decode from HIT), and for documentation as well.
Ah, I see, so that was the reason to use CList! No, it still allows for pattern matching, but using CList is fine (I just thought that it might be more elegant to use the stdlib types).
That's probably still not what you want, but here are some possible definitions of Coxter quotient.
Zeroth one is based on what we used to define HIT - for some reason it uses a custom
CList
type instead of HoTTList
. First one is the first one modified to use HoTTList
and not usew
. Second one is not using any Fins, and instead encodes the knowledge in the explicit parameter, which from my perspective is somewhat easier to work with, but I'm not sure how this quotient should look like (it will be "global", e.g. (⋃_(n : ℕ) S_n) / ~, while the zeroth and first one are S_n / ~.