prod C D gives the cartesian product of two categories.

prod.category.uniform C D is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution.

inl C Z is the functor X ↦ (X, Z).

inr D Z is the functor X ↦ (Z, X).

fst is the functor (X, Y) ↦ X.

snd is the functor (X, Y) ↦ Y.

The cartesian product of two functors.

The cartesian product of two natural transformations.