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. intros. apply (eqtohomot (homotweqinvweq (to_col D) f ) i). Qed.
Require Import