Definition precomp_is_iso : ∏ E : univalent_category, is_catiso (pre_composition_functor _ _ E H). Proof. intro E. transparent assert (a : (Core.adj_equivalence_of_cats (pre_composition_functor _ _ (pr1 E) H))). { apply precomp_adjoint_equivalence ; apply Hw. } use (pr2 (adj_equivalence_of_cats_to_cat_iso a _ _)) ; apply is_univalent_functor_category ; apply E. 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.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecompEquivalence.