Lambda the Ultimate

I've recently been working on formalizing the type system for one of my programming languages. While writing out the rules for inference I found it helpful to use both traditional type syntactic inference as well as some categorical language. The back-and-forth is so common that I have considered color-coding terms to indicate when they correspond to an object or morphism in which category.

My question for LtU is whether color-coding seems goofy or maybe helpful in some contexts. I have considered alternatives and I think there are three options:

1) Color-code terms by Category
2) Add text describing which terms correspond to which Category
3) Alter the term/type syntax to make category an explicit syntactic property