Definition pr_functor_data (I : UU) (C : I -> category) (i : I) : functor_data (product_category C) (C i). Proof. use tpair. - intro a; apply (a i). - intros x y f; simpl; apply (f i). 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.