Contents

# Contents

## Definition

A locale $L$ is locally positive or overt if every open sublocale $O \in \mathcal{O}(L)$ is an indexed join of positive open sublocales, or equivalently, if it has a base of positive open sublocales.

Other definitions of a locally positive locale include that the unique map $!:L \to 1$ is open, and that the product projection $\pi_2:L \times L' \to L'$ is open for every locale $L'$.