Lemma functor_into_product_weq {I : UU} {A : category} {B : I → category} : A ⟶ (product_category B) ≃ (∏ i : I, A ⟶ (B i)). 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.opp_precat.