Manuell, [2023] “Pointfree topology and constructive mathematics”
Introduction to constructive (pointfree) topology via the frame/local mechanism, discussing, among other things, the connection between intuitionistic and geometric logic, and introducing compactness as a “quantifiability” property. Geometric logic is a subset of first-order logic, which has finite conjunctions, infinite disjunctions, existentials, and equality (but no implication).