Lemma pr_tuple_functor {I : UU} {A : category} (B : I → category) (F : ∏ i, A ⟶ (B i)) (i : I) : tuple_functor F ∙ pr_functor I B i = F i. Proof. apply functor_eq. apply (B i). apply idpath. Qed.
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.