§ Limits of a functor category are computed pointwise.

§ Reduction to discrete category

§ Formal proof by limits of product categories

§ Draw the right diagram.

F =α=> H <=β= G
[Fp     Fq]
 |       |
 αp     αq
 v       v
[Hp      Hq]
 ^       ^
 βp      βq
 |       |
[Gp      Gq]

§ This extends to [X, Y]