Definition initial_functor_category_equivalence : adjoint_equivalence (B := bicat_of_univ_cats) D D'. Proof. exists G. apply (invmap (adj_equiv_is_equiv_cat _)). use (adjointification (make_equivalence_of_cats (make_adjunction_data G _ _ _) (make_forms_equivalence _ _ _))). + exact G'. + exact (z_iso_mor η). + exact (z_iso_mor ɛ). + intro. apply (is_functor_z_iso_pointwise_if_z_iso _ _ (homset_property _)). apply z_iso_is_z_isomorphism. + intro. apply (is_functor_z_iso_pointwise_if_z_iso _ _ (homset_property _)). apply z_iso_is_z_isomorphism. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.RezkCompletions.RezkCompletions. Require Import UniMath.CategoryTheory.WeakEquivalences.Core.