Lemma comp_essentially_surjective {C D E : precategory} (F : functor C D) (esF : essentially_surjective F) (G : functor D E) (esG : essentially_surjective G) : essentially_surjective (functor_composite F G). Proof. unfold essentially_surjective. intros e. apply (squash_to_prop (esG e)); [apply isapropishinh|]; intros isoGe. apply (squash_to_prop (esF (pr1 isoGe))); [apply isapropishinh|]; intros isoFGe. apply hinhpr. exists (pr1 isoFGe); unfold functor_composite; cbn. apply (@z_iso_comp E _ (G (pr1 isoGe))). - apply functor_on_z_iso. exact (pr2 isoFGe). - apply (pr2 isoGe). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.