Definition adj_equivalence_of_cats_to_cat_iso {C D : category} {F : functor C D} (Fa : adj_equivalence_of_cats F) (Cuniv : is_univalent C) (Duniv : is_univalent D) : catiso C D. Proof. exists F. split. - apply fully_faithful_from_equivalence, Fa. - apply(weq_on_objects_from_adj_equiv_of_cats C D Cuniv Duniv F Fa). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.