pointwise (identity C) (identity D) = identity _. Proof. path_functor. exists identity_of_helper. unfold identity_of_helper. abstract functor_pointwise_t identity_of_helper_helper identity_of_helper_helper_object_of. Defined.
Require Import Category.Core Functor.Core Functor.Pointwise.Core NaturalTransformation.Core NaturalTransformation.Paths Functor.Composition.Core Functor.Identity Functor.Paths. Require Import PathGroupoids Types.Forall HoTT.Tactics. Require Import Basics.Tactics.