remove all admits from ProgrammingLanguage.v
unbreak lots more stuff
update to new coq-categories, base ND_Relation on inert sequences
update to account for coq-categories changes
update submodule pointer, account for changes upstream
lots of cleanup
fix typo
update submodule pointer
update submodule pointer
update submodule pointer
update submodule pointer
fix proof that Judgments(L) is Cartesian
update categories submodule pointer
update categories submodule pointer
add coq-categories as a submodule