Open pufferffish opened 10 months ago
Turns out this would involve a lot of refactoring, a lot of arbitrary types in Sig
, EqSig
, struct
, and such would need to be changed so that they are accompanied with a proof that states they are of a certain h-level, which would then involve spamming implicit h-level arguments everywhere. This would then add a lot of proof burden since we now need to constantly prove certain types are of the specified h-level, which is annoying because isOfHLevel h (𝔜 .carrier)
isn't really used anywhere aside from defining Free
definition anyway (e.g. the free monoid definition, where trunc
is not used once outside of proving theorems about sharp).
Probably best to put this on hold until we find a nicer way to deal with general h-level for Free. One potential solution would be instance arguments, however this does not follow the convention of the cubical library since instance arguments aren't really used in the library.
It's not clear how to handle the trunc for sets and groupoids, what we can say for sure is that for sets, eqs should be a proposition, and for groupoids, cohs should be a proposition.
ext
in Free should be renamed to sharp, but to make it work nicely with infix we should move(H : isOfHLevel h (𝔜 .carrier))
to struct instead