proposition: 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: Proof. intros. exact (eqtohomot (homotweqinvweq (to_row B) f) j). Qed.
imports: UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.RepresentableFunctors.Representation UniMath.CategoryTheory.RepresentableFunctors.Precategories