Lemma filtered_alt_has_finite_multispan_cocones {J : category} (filtalt : is_filtered_alt J) (X : UU) (n : nat) (w : X ≃ ⟦ n ⟧) (d : diagram (multispan_graph X) J) : ∃ z : J, cocone d z. Proof. set (base := dob d multispan_base). set (point_diagram := make_discrete_diagram' d). assert(r : (X ⨿ unit) ≃ ⟦ (S n) ⟧). { use(weqcomp (weqcoprodf1 w)). exact(weqdnicoprod n lastelement). } use(filtered_alt_has_discrete_cocones filtalt _ point_diagram (S n) r). intros [P Pcc]. transparent assert(edge_diagram : (diagram (parallell_graph (X ⨿ unit)) J)). { use make_parallell_diagram. - exact base. - exact P. - apply sumofmaps. * exact(λ x : X, dmor d (multispan_edge x) · (coconeIn Pcc (multispan_vertex x))). * exact(unit_rect _ (coconeIn Pcc multispan_base)). } use(filtered_alt_has_parallell_cocones filtalt (X ⨿ unit) (S n) r edge_diagram). intros [Q Qcc]; apply hinhpr. exists Q. use make_multispan_cocone. - exact(coconeIn Qcc parallell_start). - exact(λ x : X, coconeIn Pcc (multispan_vertex x) · coconeIn Qcc parallell_end). - intro x. etrans;[apply assoc |]. exact(parallell_cocone_commutes Qcc (inl x)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.CategoryTheory.Limits.StandardDiagrams.