Jasper Hugunin

> Can you elaborate a bit more.. Would that be this? > > `...` I was thinking of: ```agda primitive primGlueProp : ∀ {ℓ ℓ'} (A : Prop ℓ) {φ...

@nad > During the Agda meeting today we discussed disallowing the combination of `--cubical` and `--prop`, because little thought seems to have gone into the combination of these features (see...

I was frustrated by the current state of proof handling when trying to refactor the implicit arguments subsystem. This project should clarify the current state and make it easier to...