Right now we have a category where the objects are contexts, and the morphisms are context maps. This is equivalent to the category of free algebras of the syntax monad for a theory. We should also allow more general algebras, which include laws, and maps between these that respect the laws.
Right now we have a category where the objects are contexts, and the morphisms are context maps. This is equivalent to the category of free algebras of the syntax monad for a theory. We should also allow more general algebras, which include laws, and maps between these that respect the laws.