premetric.dist_setoid

The canonical equivalence relation on a premetric space.

premetric.metric_quot

The canonical quotient of a premetric space, identifying points at distance 0.