Definition PushoutQuotobject {c : C} (Q : Quotobjectscategory c) {c' : C} (h : C⟦c, c'⟧) : Quotobjectscategory c'. Proof. set (po := hpo _ _ _ h (pr1 (pr2 Q))). use Quotobjectscategory_ob. - exact po. - exact (Limits.Pushouts.PushoutIn1 po). - use EpiPushoutisEpi'. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.UnderCategories. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Limits.Pushouts.