Definition to_matrix {C:category} {I} {d:I -> ob C} (D:Product d) {J} {b:J -> ob C} (B:Sum b) : (Hom C (universalObject B) (universalObject D)) ≃ (∏ i j, Hom C (b j) (d i)). Proof. intros. apply @weqcomp with (Y := ∏ i, Hom C (universalObject B) (d i)). { apply to_col. } { apply weqonsecfibers; intro i. apply to_row. } Defined.
Require Import