Compact locale
= 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.