proposition: Lemma adjunction_naturality' : adjunction_naturalityT'.
proof: Proof. pose proof (ap10 (commutes A (c', d) (c, d) (g, 1%morphism))^ f) as H'; simpl in *. rewrite ?identity_of, ?left_identity, ?right_identity in H'. exact H'. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Adjoint.UnitCounit Adjoint.UnitCounitCoercions Adjoint.Hom Category.Morphisms Functor.Composition.Core FunctorCategory.Morphisms Functor.Identity SetCategory.Morphisms Basics.Trunc Types.Sigma HoTT.Tactics Equivalences