Constructive Urysohn's Universal Metric Space

A construction of the Urysohn's universal metric space is given in the context of constructive theory of metric spaces. The space is universal in the sense that every separable metric space isometrically embeds into it. Moreover, every isometry between two finite subspaces extends to total isometry, and this determines the Urysohn space uniquely up to isometric isomorphism.