functor.category C D gives the category structure on functors and natural transformations between categories C and D.

Notice that if C and D are both small categories at the same universe level, this is another small category at that level. However if C and D are both large categories at the same universe level, this is a small category at the next higher level.

hcomp α β is the horizontal composition of natural transformations.