Goal: Develop an agda library for representing (first-order) theories and the relations between them. TO DO: Define Morita extension of a theory. Give an axiomatization of special relativity.