Anders Mörtberg
Anders Mörtberg
Btw, with this hack it's obviously easy to do bad things. Just have a type with parameters called "S1" and make some coercion that shouldn't compute like the identity. However,...
> A friend told me it's when your type is not parameterized, but I actually don't quite understand why it works this way. I guess I'll need to read some...
I had a look at this and made the following short self-contained piece of code based on Thorsten's code which shows where Agda's termination checker gets unhappy: ```agda {-# OPTIONS...
Sounds good to me! Please go ahead and make a PR
Could some reorganization be done to avoid duplication? Another thing is that I generally don't like operations that take hProp's as input and produce hProp's if they don't have to....
> The main aspect is that `Cubical.Functions.Embeddings` needs some proofs regarding powersets such as `Embedding→Subset` and the like. It might be possible to isolate the proofs involving powersets in the...
Feel free to make PRs either removing one of the proofs or documenting why we have two versions (maybe also moving results to the same place). Something that annoyed me...
> I tried on my own computer, and after waiting for a long time I finally get some unsolved metas: > > ``` > Unsolved metas at the following locations:...
Ps: me looking into this was prompted by https://github.com/agda/cubical/pull/1129 which would benefit from global `--guardedness`
Feel free to make a PR if nothing breaks. I like short PRs that make things better :-)