Let $C,D$ be categories with objects $O_C,O_D$ and morphisms $M_C:O_C\times O_C\to Type_0$, $M_D:O_D\times O_D\to Type_0$. Let $F,G:C\to D$ be functors. A natural transformation $\eta$ associates to each object $x\in O_C$ a morphism $\eta(x) : M_D(F(x), G(x))$.
How can I express this restriction in the type of $\eta$? I want to write $\eta: (x\in O_C) \to M_D(F(x),G(x))$, but this notation is not standard.
You express it with a dependent product: $\eta : \prod_{x : O_C} M_D (F(x), G(x))$.