Benedikt Ahrens

Thanks for preparing this overview! Where is the definition of the “non-standard” invertibility?

Thanks again, @peterlefanulumsdaine , for the very helpful message. I agree with your proposal from the first message.

What is missing in this PR? I believe that at least a suitable entry in the Makefile is missing - anything else? I am not sure we need this to...

@DanGrayson : would you be able to assist @Bigstep22 in creating a target in the Makefile?

I think it is best to stick with the established name, though I agree with Dan's objections. I am closing this issue.

I don't think that UniMath is a good place to have a discussion on vocabulary used in CT.

@m-lindgren : this PR is still marked as a draft - is this correct, or is it ready for review?

@peterlefanulumsdaine thanks a lot for preparing this. There is a warning about deprecated "Export Set" - should we address this before merging?

@arnoudvanderleer : thanks for fixing this issue!

By '"needed", do you mean "needed" or "used"?