The title is a bit sneaky. Division by zero in "type theory" will depend on just that -- your type theory. Some theories use special values for division by zero

The title is a bit sneaky. Division by zero in "type theory" will depend on just that -- your type theory. Some theories use special values for division by zero (e.g. could spit out DNE or +INF/-INF). But then you need to formalize how you do "things" with DNE or infinities. This is, more often than not, an unnecessary rabbit hole, so just returning 0 is simpler. Some theories might require a proof that the denominator isn't zero (essentially making division a three-argument function) -- which is kind of a cool way of thinking about it[1]. [1] https://math.stackexchange.com/questions/334393/how-does-type-theory-handle-division-by-zero-and-such https://math.stackexchange.com/questions/334393/how-does-typ...