Definition weq_on_objects_from_adj_equiv_of_cats (A B : category) (HA : is_univalent A) (HB : is_univalent B) (F : ob [A, B]) (HF : adj_equivalence_of_cats F) : weq (ob A) (ob B). Proof. exists (pr1 (pr1 F)). now apply (@adj_equiv_of_cats_is_weq_of_objects _ _ HA). 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.