NaturalTransformation (pointwise (identity E) F o pointwise (identity E) G) (identity (E -> D)). Proof. pose proof (A : AdjunctionCounit _ _) as A''. refine ((((idtoiso (C := (_ -> _)) (Functor.Pointwise.Properties.identity_of _ _)))%morphism : morphism _ _ _) o _). refine (NaturalTransformation.Pointwise.pointwise_r (Functor.Identity.identity E) (proj1 A'') o _). refine (_ o (((idtoiso (C := (_ -> _)) (Functor.Pointwise.Properties.composition_of (Functor.Identity.identity E) G (Functor.Identity.identity E) F))^-1)%morphism : morphism _ _ _)). refine (NaturalTransformation.Pointwise.pointwise_l _ _). exact (NaturalTransformation.Composition.Laws.left_identity_natural_transformation_1 _). 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.