proposition: Lemma right_adj_equiv_is_ff : fully_faithful G.
proof: Proof. intros c d. set (inv := (fun f : D1 ⟦G c, G d⟧ => εinv _ · #F f · ε _ )). simpl in inv. apply (isweq_iso _ inv ). - intro f. simpl in f. unfold inv. assert (XR := nat_trans_ax ε). simpl in XR. rewrite <- assoc. etrans. apply maponpaths. apply XR. rewrite assoc. etrans. apply maponpaths_2. apply z_iso_after_z_iso_inv. apply id_left. - intro g. unfold inv. do 2 rewrite functor_comp. intermediate_path ((# G (inv_from_z_iso (counit_pointwise_z_iso_from_adj_equivalence GG c)) · ηinv _ ) · (η _ · # G (# F g)) · # G (ε d)). + do 4 rewrite <- assoc. apply maponpaths. do 2 rewrite assoc. etrans. 2: do 2 apply maponpaths_2; eapply pathsinv0, z_iso_after_z_iso_inv. refine (_ @ assoc _ _ _). exact (!id_left _). + assert (XR := nat_trans_ax η). simpl in XR. rewrite <- XR. clear XR. do 3 rewrite <- assoc. etrans. do 3 apply maponpaths. apply triangle_id_right_ad. rewrite id_right. rewrite assoc. etrans. 2: apply id_left. apply maponpaths_2. etrans. apply maponpaths_2. apply functor_on_inv_from_z_iso. assert (XR := triangle_id_right_ad (pr2 (pr1 GG))); simpl in XR. unfold ηinv; simpl. pose (XRR := maponpaths pr1 (z_iso_inv_of_z_iso_comp _ _ _ (unit_pointwise_z_iso_from_adj_equivalence GG ((adj_equivalence_inv GG) c)) (functor_on_z_iso G (counit_pointwise_z_iso_from_adj_equivalence GG c)) )). simpl in XRR. etrans. apply (! XRR). clear XRR. apply pathsinv0, inv_z_iso_unique'. cbn. unfold precomp_with. rewrite id_right. apply XR. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct