proposition: Lemma filtered_alt_has_parallell_cocones {J : category} (filtalt : is_filtered_alt J) (X : UU) (n : nat) (w : X ≃ ⟦ n ⟧) (d : diagram (parallell_graph X) J) : ∃ z : J, cocone d z.
proof: Proof. set (dₙ := make_parallell_diagram (⟦ n ⟧) (dob d parallell_start) (dob d parallell_end) (λ k : ⟦ n ⟧, dmor d (parallell_edge (invmap w k)))). use(hinhfun _ (filtered_alt_has_parallell_stn filtalt n dₙ)). intros [P Pcc]. exists P. use make_parallell_cocone. - exact(coconeIn Pcc parallell_start). - exact(coconeIn Pcc parallell_end). - apply(weqonsecbase _ (invweq w)). exact(λ k : ⟦ n ⟧, parallell_cocone_commutes Pcc k). 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