proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.covyoneda UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSets UniMath.CategoryTheory.Limits.StandardDiagrams