Implementing a Category-Theoretic Framework for Typed Abstract Syntax