Lemma essentially_surjective_2_from_comp {C C' C'' : category} (F : C ⟶ C') (F' : C' ⟶ C'') (H : essentially_surjective (functor_composite F F')) : essentially_surjective F'. Proof. intro. refine (hinhfun _ (H b)). intro x. exists (F (pr1 x)). exact (pr2 x). Qed.
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.