Lemma rad_equivalence_of_cats' : adj_equivalence_of_cats F. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core.