Definition tuple_functor_data {I : UU} {A : category} {B : I → category} (F : ∏ i, A ⟶ (B i)) : functor_data A (product_category B). Proof. use tpair. - intros a i; exact (F i a). - intros a b f i; exact (# (F i) f). 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.