Theorem well_pointed_of_fully_faithful_right_adjoint {C D : category} (L : functor C D) (R : functor D C) (H : are_adjoints L R) (η := unit_from_are_adjoints H) : fully_faithful R → well_pointed (L∙R,,η). Proof. intro R_ff. apply (nat_trans_eq (homset_property _)). intros A. simpl. set (ɛ := counit_from_are_adjoints H). assert (t1 : # R (# L (η A)) · # R (ɛ (L A)) = identity (R (L A))). { rewrite <- functor_id, <- functor_comp. apply maponpaths. apply triangle_id_left_ad. } assert (t2 : η (R (L A)) · # R (ɛ (L A)) = identity (R (L A))). { apply triangle_id_right_ad. } assert (ɛ_z_iso := counit_is_z_iso_if_right_adjoint_is_fully_faithful H R_ff). assert (p : is_z_isomorphism (# R (ɛ (L A)))). { apply functor_on_is_z_isomorphism. apply counit_is_z_iso_if_right_adjoint_is_fully_faithful. exact R_ff. } apply (post_comp_with_z_iso_is_inj p). exact (t2 @ ! t1). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.