Contents

# Contents

## Definition

A premetric locale is a locally positive locale that is also a setoid enriched in $(\overleftarrow{\mathbb{R}_+^\infty}, \geq, +, 0)$, the locale of non-negative extended real numbers whose topology is upper semi-continuity.