Geometric logic (source code)

= Geometric logic

The fragment uses finite conjunction, set-indexed disjunction and existential quantification, with equality and atomic relations. It is preserved under <inverse image functors of geometric morphisms>. The universal closure of an axiom is expressed by its variable context, not an unrestricted universal-quantifier constructor.