Lemma from_matrix_entry_assoc {C:category} {I} {d:I -> ob C} (D:Product d) {J} {b:J -> ob C} (B:Sum b) (f : ∏ i j, Hom C (b j) (d i)) : ∏ i j, universalElement D i ∘ (from_matrix D B f ∘ opp_mor(universalElement B j)) = f i j. Proof. intros. rewrite <- assoc. exact (from_matrix_entry D B f i j). Qed.
Require Import