Lemma filtered_forms_cocone : forms_cocone d inject. 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.
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.