What axiom makes you be able to skip definition for impossible input for function in Agda?

Question

_/_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
m / (suc n) = div-helper 0 n m n

In this function definition, there is no definition of case when second input is zero, because Agda knows second input cannot be zero. But in formal(theoretical) perspective, what justify these function definition? Is there axioms like 'you can skip definition for impossible input' in Type Theory, like axiom J and axiom K?

Answer 1

The axiom that you need is called the "principle of explosion" or "ex falso quodlibet" (see https://en.wikipedia.org/wiki/Principle_of_explosion). In type theory, this is typically formulated as an elimination principle for the empty type:

A : Type    b : ⊥
————————————————–
  absurd b : A