proposition: Lemma functor_into_product_weq {I : UU} {A : category} {B : I → category} : A ⟶ (product_category B) ≃ (∏ i : I, A ⟶ (B i)).
proof: Proof. use weq_iso. - intros ? i. apply (functor_composite (C' := product_precategory B)). + assumption. + exact (pr_functor _ _ i). - exact tuple_functor. - intro y. apply functor_eq; [apply homset_property|]. reflexivity. - intro f; cbn. apply funextsec; intro i. apply functor_eq; [exact (homset_property (B i))|]. reflexivity. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.opp_precat