What is Axiom K?
<p>I've noticed the discussion of "Axiom K" comes up more often since HoTT. I believe it's related to pattern matching. I'm surprised that I cannot find a reference in TAPL, ATTAPL or PFPL.</p>

<ul>
<li>What is Axiom K?</li>
<li>Is it used for ML-style pattern matching as in SML (or just dependent pattern matching)?</li>
<li>What's an appropriate reference for Axiom K?</li>
</ul>