Definition filtered_cobase_rel_impl {Y : SET} (cc : cocone d Y) (a b : cobase) (Rab : filtered_cobase_rel a b) : from_cobase_eqrel cc a b. Proof. use Rab; intros h. etrans; [refine(!eqtohomot (coconeInCommutes cc _ _ _) a); exact(pr12 h) |]. etrans; [| refine(eqtohomot (coconeInCommutes cc _ _ _) b); exact(pr122 h)]. apply(maponpaths _ (pr222 h)). 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.