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?