Definition from_matrix {C:category} {I} {d:I -> ob C} (D:Product d) {J} {b:J -> ob C} (B:Sum b) : weq (∏ i j, Hom C (b j) (d i)) (Hom C (universalObject B) (universalObject D)). Proof. intros. apply invweq. apply to_matrix. Defined.
Require Import