proposition: Lemma filtered_forms_cocone : forms_cocone d inject.
proof: Proof. intros u v e. apply funextfun; intros x. apply(weqpathsinsetquot filtered_eqrel). apply eqrel_impl. use(hinhfun _ (Jfiltered _ (make_interval_diagram u v e) (is_finite_graph_interval))). intros P; destruct P as [apex cc]; cbn. exists apex. exists (coconeIn cc false). exists (coconeIn cc true). change (dmor d (coconeIn cc false) (dmor d e x)) with ((dmor d e · (dmor d (coconeIn cc false))) x). use(eqtohomot _ x). etrans; [apply(!functor_comp F e (coconeIn cc false)) |]; apply maponpaths. exact(coconeInCommutes cc true false tt). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Sets UniMath.MoreFoundations.QuotientSet UniMath.MoreFoundations.Subtypes UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Filtered UniMath.CategoryTheory.Limits.StandardDiagrams UniMath.CategoryTheory.Categories.HSET.Core UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.KFiniteTypes UniMath.Combinatorics.KFiniteSubtypes