Point-free substitution

A new characterization of substitution, viz. as a universally conjunctive and universally disjunctive predicate transformer, is proposed. This characterization is also meaningful in point-free models for predicate calculus, and agrees with the classical definition of substitution whenever the latter is applicable.