proposition: Lemma counit_natural_transformation__of__adjunction_unit_helper (A : AdjunctionUnit F G) s d (m : morphism D s d) (eta := A.1) (eps := fun X => (@center _ (A.2 (G X) X 1)).1) : G _1 (eps d o F _1 (G _1 m)) o eta (G s) = G _1 m -> G _1 (m o eps s) o eta (G s) = G _1 m -> eps d o F _1 (G _1 m) = m o eps s.
proof: Proof. intros. transitivity (@center _ (A.2 _ _ (G _1 m))).1; [ symmetry | ]; let x := match goal with |- _ = ?x => constr:(x) end in refine ((fun H => ap pr1 (@contr _ (A.2 _ _ (G _1 m)) (x; H))) _); assumption. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Adjoint.UnitCounit Adjoint.Dual Functor.Composition.Core Functor.Identity HoTT.Tactics Basics.Trunc Types.Sigma Basics.Tactics