Definition tuple_functor {I : UU} {A : category} {B : I → category} (F : ∏ i, A ⟶ (B i)) : A ⟶ (product_category B) := (tuple_functor_data F,, tuple_functor_axioms F).
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.