pointwise (identity E) F -| pointwise (identity E) G. Proof. exists unit_l counit_l; abstract ( path_natural_transformation; intros; destruct A; simpl in *; repeat match goal with | _ => progress simpl | _ => progress autorewrite with adjoint_pointwise | [ |- context[ap object_of (path_functor_uncurried ?F ?G (?HO; ?HM))] ] => rewrite (@path_functor_uncurried_fst _ _ _ F G HO HM) | _ => progress unfold Functor.Pointwise.Properties.identity_of | _ => progress unfold Functor.Pointwise.Properties.composition_of | _ => progress unfold Functor.Pointwise.Properties.identity_of_helper | _ => progress unfold Functor.Pointwise.Properties.composition_of_helper | _ => progress unfold Functor.Pointwise.Properties.identity_of_helper_helper | _ => progress unfold Functor.Pointwise.Properties.composition_of_helper_helper | [ H : _ |- _ ] => apply H end ). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Identity. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core. Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.UnitCounitCoercions. Require Import Functor.Pointwise.Core. Require Import Category.Morphisms FunctorCategory.Morphisms. Require Import FunctorCategory.Core. Import NaturalTransformation.Identity.NaturalTransformationIdentityNotations. Require Import NaturalTransformation.Paths Functor.Paths. Require Import Basics.PathGroupoids HoTT.Tactics Types.Arrow.