proposition: Lemma curry_after_uncurry_pointwise (G: D ⟶ [C, E]) (d: D) : pr1 (curry_functor (uncurry_functor G)) d = pr1 G d.
proof: Proof. apply functor_eq. { exact E. } use functor_data_eq. - intro c. apply idpath. - cbn. intros c c' f. assert (H := functor_id G d). apply (maponpaths (fun f => pr1 f c')) in H. etrans. { apply maponpaths. exact H. } apply id_right. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat