I have been enjoying the course immensely, and feel like I am finally getting my grounding in category theory. I've explored all sorts of advanced topics, but coming back to base has really made me feel like I understand, not just parrot these ideas.

I do need to do my homework for this course though. I keep trying to compleatly formalize and getting distracted by fun but mathematically trivial proof system issues.

(For example it takes a page of tactics to prove that direct image with powerset on objects is a endo-functor on Set)