Definition Quotobjectscategory (c : C) : UU := Undercategory (subprecategory_of_epis C) (has_homsets_subprecategory_of_epis C) (subprecategory_of_epis_ob C c).
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.