Felix Cherubini

> Thank you for pointing out this synthetic approach. I am not sure that it is directly related but i would be interested to see how it is implemented. There...

I think I defined ```_$a_``` but ended up not using it. But now that I think of it, I'm actually for using it and similar functions.

#917 merged -> ready for review.

...once the conflicts are resolved.

Sure - can you have a look here: https://github.com/agda/cubical/pull/914/files#diff-10188ff3797498a9126f5c681c626d1393821b30b54631a297879880a90fe8b1L96-L106 Maybe this is something you want to use in ongoing work.

Don't know how I missed the implementation in #729... -> Closing.

@guilhermehas : What is the status of this PR? Does it need more testing?

@phijor : Thanks for joining! @guilhermehas : Thanks for updating... Could you also rebase/merge master?

I assume the second, slow, apparently not cached ci job added by this PR is intended - I don't mind it since it doesn't seem to slow down the old...

@guilhermehas : Feel free to use the "Resolve conversation" button in the conversations above, if you think something is resolved.