Post #2093349

Happy to have made my first contribution to Agda :) We now have a sharp modality (from https://arxiv.org/abs/1509.07584) which is a right adjoint to the flat modality which Agda already has. Sharp is an idempotent monad, so unlike flat it can be postulated in type theory… but I think having it as a builtin provides a lot of convenience for not a lot of extra complication to the theory. By defining it as a record, we have definitional eta-laws and I think it’s pretty cool being able to use Sharp via copattern matching. Excited to formalise some stuff with it soon!