Thanks for clearing that up! One of the rare cases where something is less subtle than I thought it was.

Incidentally, regarding the disclaimer: I was (quite informally) familiar with type theory (from occasionally dabbling in Agda and implementing type systems in Haskell) before I ever started learning maths, and your answer was quite readable. :)

+1, this is a great answer from the "other side" and made the similarities a little clearer!

Seconded. I'd never thought of categories as "groupoids with structure" before, and "To some extent the set of object and of arrows with the appropriate structure is a "presentation" of your category." was a bit of an aha-moment (a breakthrough, if you will!) for me. :)

I had no idea what to tag this with; appropriate retagging would be appreciated. I'm not sure if this is a valid soft-question.

@AndrésE.Caicedo ah, my apologies. Thank you for reverting the edit.

@TheMathemagician it would be nice if you could emphasise your words *like this* rather than shouting. :)