Lemma from_row_entry {C:category} {I} {b:I -> ob C} (B:Sum b) {d:ob C} (f : ∏ j, Hom C (b j) d) : ∏ j, from_row B f ∘ opp_mor (universalElement B j) = f j. Proof. intros. exact (eqtohomot (homotweqinvweq (to_row B) f) j). Qed.
Require Import