Definition from_cobase_hrel {Y : SET} (cc : cocone d Y) : hrel cobase. Proof. intros a b. use make_hProp. - exact(from_cobase cc a = from_cobase cc b). - apply setproperty. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.QuotientSet. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Filtered. Require Import UniMath.CategoryTheory.Limits.StandardDiagrams. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Combinatorics.KFiniteTypes. Require Import UniMath.Combinatorics.KFiniteSubtypes.