Definition functor_pointwise (a : A) : functor J C. Proof. use tpair. - apply (tpair _ (λ v, pr1 (D v) a)). intros u v e; simpl; apply (pr1 (# D e) a). - abstract (use tpair; [ intro x; simpl; apply (toforallpaths _ _ _ (maponpaths pr1 (functor_id D x)) a) | intros x y z f g; simpl; apply (toforallpaths _ _ _ (maponpaths pr1 (functor_comp D f g)) a)]). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory.