proposition: Lemma counit_is_z_iso_if_right_adjoint_is_fully_faithful : fully_faithful G -> ∏ x, is_z_isomorphism (ε x).
proof: Proof. intros ? ?. apply merely_split_monic_is_epi_to_is_z_iso. - apply counit_is_split_monic_if_right_adjoint_is_full. apply fully_faithful_implies_full_and_faithful; assumption. - apply counit_is_epi_if_right_adjoint_is_faithful. apply fully_faithful_implies_full_and_faithful; assumption. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Epis UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.Monics UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering