From Identity to Difference: A Quantitative Interpretation of the Identity Type

We explore a quantitative interpretation of 2-dimensional intuitionistic type theory (ITT) in which the identity type is interpreted as a "type of differences". We show that a fragment of ITT, that we call difference type theory (dTT), yields a general logical framework to talk about quantitative properties of programs like approximate equivalence and metric preservation. To demonstrate this fact, we show that dTT can be used to capture compositional reasoning in presence of errors, since any pr...