Rahul Chhabra
Rahul Chhabra
Hey I would be willing to work on this. I would like to know exactly how effects are implemented? Using monads, a la Haskell? Algebraic effects a la Eff? Non-well-founded...
Hi, I've opened a PR. Let me know if any changes are necessary. Thanks!
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 `Embeddings`...
Sure, I'll have a go at it! :D