proposition: 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: Proof. apply functor_eq. apply (B i). apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.opp_precat