Definition product_precategory_ob_mor : precategory_ob_mor. Proof. use tpair. - apply (∏ (i : I), ob (C i)). - intros f g. apply (∏ i, f i --> g 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.