 Compact locale

A locale is compact when every directed family of opens whose join is $1$ contains $1$. Equivalently every open cover has a finite subcover. The truth-valued test $a\mapsto [a=1]$ is a preframe homomorphism exactly when the locale is compact.