10. Units and the Dimension-1 Problem
This chapter states the layer that originally motivated PropertyKindCalculus. Every
node in it is proved and carries a (lean := …) declaration: the motivating
capstone — the dimension-1 disambiguation, whose forgetful map the Dimension as a
Forgetful Functor chapter supplies — and the unit-arithmetic nodes around it alike.
PhysLib's Dimension (a ℚ-exponent free commutative group over the SI base
quantities) makes every dimension-one quantity equal. Volumetric water content
(\mathrm{L^3/L^3}), gravimetric water content (\mathrm{M/M}), relative
permittivity, reflectivity, and emissivity are all dimension one — so a
dimension-only type system cannot tell them apart. In soil-moisture retrieval
that is precisely the class of confusion that silently corrupts a result. The
kind layer is what restores the distinction.