  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 program can be associated with a
"derivative" relating errors in input with errors in output. Moreover, after
relating the semantics of dTT to the standard weak factorization systems
semantics of ITT, we describe the interpretation of dTT in some quantitative
models developed for approximate program transformations, incremental
computing, program differentiation and differential privacy.
