Why do I have to give match patterns which don't type check?

Neat! A very nice example of using Program. And it does not use axioms (I checked with Print Assumptions on your definition).Thanks for pointing this out - I would say this is good enough.

well there is the issue that e.g. axiom K is incompatible with univalence. See the post by @Zimmi48: