proposition: Lemma adjunction_hom__of__adjunction_unit__commutes (T : AdjunctionUnit F G) sc sd dc dd (mc : morphism C dc sc) (md : morphism D sd dd) : (fun x : morphism D (F sc) sd => G _1 (md o x o F _1 mc) o T .1 dc) = (fun x : morphism D (F sc) sd => G _1 md o (G _1 x o T .1 sc) o mc).
proof: Proof. apply path_forall; intro. rewrite !composition_of, !associativity. simpl rewrite (commutes T.1). 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