proposition: Lemma from_matrix_entry {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: Proof. intros. exact (eqtohomot (eqtohomot (homotweqinvweq (to_matrix D B) f) i) 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