I think type theory is really nice for writing down certain things. Quantified statements are a perfect example! But Category Theory has nice properties, too. You already mention universal properties and adjunctions. Those are obvious examples in the other way.
Much of math is this way. Find a subject that you can see from two perspectives and abuse the best parts of each!
Much of math is this way. Find a subject that you can see from two perspectives and abuse the best parts of each!