Port most of NaturalTransformation
Port most of FunctorCategory
Add more tactics
Port GroupoidCategory
Add {in,}discrete categories
Port NatCategory
Update Notations file
Don't duplicate notations logic
Add InitialTerminalCategory
Merge pull request #225 from JasonGross/categories2

Second large port from HoTT-categories