Constructive reflectivity principles for regular theories

Henrik Forssell, Peter LeFanu Lumsdaine

Classically, any structure for a signature $\hat{I}\pounds$ may be completed to a model of a desired regular theory $T$ by means of the chase construction or small object argument. Moreover, t…