Definition family_functor (I : UU) {A B : I -> category} (F : ∏ (i : I), (A i) ⟶ (B i)) : (product_category A) ⟶ (product_category B). Proof. apply (tpair _ (family_functor_data I F)). abstract (split; [ intro x; apply funextsec; intro i; simpl; apply functor_id | intros x y z f g; apply funextsec; intro i; apply functor_comp]). 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.