Contents

# Contents

## Definition

A metric locale is a premetric locale such that for all $U:\mathcal{O}(x)$,

$U =_{\mathcal{O}(x)} \bigvee_{V:\sum_{V':\mathcal{O}(x)} V' \lhd U} V$

where

$\sum_{V':\mathcal{O}(x)} V' \lhd U$

is the subtype of all $V':\mathcal{O}(x)$ such that $V' \lhd U$.