proposition: Lemma rad_equivalence_of_cats' : adj_equivalence_of_cats F.
proof: Proof. exists rad_is_left_adjoint. split; simpl. intro a. unfold rad_eta. set (H := fully_faithful_reflects_iso_proof _ _ _ HF a (rad_ob (F a))). simpl in *. set (H' := H (z_iso_inv_from_z_iso (rad_eps (F a)))). change ((fully_faithful_inv_hom HF a (rad_ob (F a)) (inv_from_z_iso (rad_eps (F a))))) with (fully_faithful_inv_hom HF a (rad_ob (F a)) (z_iso_inv_from_z_iso (rad_eps (F a)))). apply H'. intro b. apply (pr2 (rad_eps b)). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core