add finite products
add a lemma about representations of functors

  Lemma representingIso {C} (X:C==>SET) (r:Representation X) :
    forall d:ob C,
      isweq (fun p : Hom (representingObject r) d => (#X p) (representingElement r)).

The proof is short:

  Proof. intros. intros y. exact (representingInitiality r (d,,y)). Qed.