Computational Category Theory
cs.man.ac.uk
cs.man.ac.uk
A lot of the encodings seem to around that
I've over time gotten a lot out of efforts to model category theory in agda, one example being https://github.com/copumpkin/categories (though theres many more).