Definition iso_comma_essentially_surjective {C₁ C₂ C₃ : category} (F : C₁ ⟶ C₃) (HF : essentially_surjective F) (G : C₂ ⟶ C₃) : essentially_surjective (iso_comma_pr2 F G). Proof. intros y. use (factor_through_squash _ _ (HF (G y))). - apply isapropishinh. - intros x. induction x as [ x i ]. apply hinhpr. simple refine (((_ ,, _) ,, _) ,, _) ; cbn. + exact x. + exact y. + exact i. + apply identity_z_iso. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.