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. 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.
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.