Definition precomp_adjoint_equivalence : adj_equivalence_of_cats (pre_composition_functor C₁ C₂ (pr1 D) F). Proof. use rad_equivalence_of_cats. - apply is_univalent_functor_category. exact (pr2 D). - exact (pre_composition_with_ess_surj_and_fully_faithful_is_fully_faithful C₁ C₂ D F HF₁ HF₂). - exact (pre_composition_essentially_surjective C₁ C₂ D (pr2 D) F HF₁ HF₂). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.precomp_ess_surj. Require Import UniMath.CategoryTheory.precomp_fully_faithful. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.