Constructive Urysohn Universal Metric Space

We construct the urysohn metric space in constructive setting without choice principles. the urysohn space is a complete separable metric space which contains an isometric copy of every separable metric space, and any isometric embedding into it from a finite subspace of a separable metric space extends to the whole domain.