proposition: Lemma adjunction_unit__of__adjunction_hom__mate_of__commutes (A : AdjunctionHom F G) (s d : C) (m : morphism C s d) : A (d, F d) 1 o m = G _1 (F _1 m) o A (s, F s) 1.
proof: Proof. simpl; rewrite adjunction_naturality', adjunction_naturality. rewrite ?left_identity, ?right_identity. reflexivity. 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