We extend Lawvere-Pitts prop-categories (aka. hyperdoctrines) to develop a general framework for providing "algebraic'' semantics for nonclassical first-order logics. This framework includes a natural notion of substitution, ...