proposition: Lemma from_col_entry {C:category} {I} {b:I -> ob C} (D:Product b) {d:ob C} (f : ∏ i, Hom C d (b i)) : ∏ i, universalElement D i ∘ from_col D f = f i.
proof: Proof. intros. apply (eqtohomot (homotweqinvweq (to_col D) f ) i). 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