Definition pr_functor (I : UU) (C : I -> category) (i : I) : (product_category C) ⟶ (C i). Proof. apply (tpair _ (pr_functor_data I C i)). abstract (split; intros x *; apply idpath). 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.