Contents

# Contents

## Definition

An open sublocale $O \in \mathcal{O}(L)$ is positive if, whenever $O$ is the indexed join of open sublocales $U_i \in \mathcal{O}(L)$

$O = \bigvee_{i:I} U_i$

the index set $I$ is inhabited.

A locale $L$ is positive if the top open sublocale $L \in \mathcal{O}(L)$ is positive.