I just noticed that [agda supposedly has support for HITs](https://github.com/agda/agda/issues/2761) since November. Since I didn't realise this was the case I am letting people here know too.
Now my questions:
Are these really HITs?
Do they work without axiom K?
What can and can't be done with them?