I think the most interesting design space is around not requiring normalisation. After all, if you have a normal form, you can probably represent it with sum an

I think the most interesting design space is around not requiring normalisation. After all, if you have a normal form, you can probably represent it with sum and product types. Cubical Agda gives you this ability but it's really hard to use (as you might expect from one of the first attempts to create the functionality).