Lemma filtered_alt_has_discrete_cocones {J : category} (filtalt : is_filtered_alt J) (X : UU) (d : diagram (discrete_graph X) J) (n : nat) (w : X ≃ ⟦ n ⟧) : ∃ z : J, cocone d z. Proof. use(filtered_alt_has_discrete_cocones_stn filtalt n). - exact(make_discrete_diagram (λ k : ⟦ n ⟧, dob d (invmap w k))). - intros [P Pcc]; apply hinhpr. exists P. use make_discrete_cocone. + intro x. apply(transportf (fun y : X => J⟦ dob d y, P ⟧) (homotinvweqweq w x)). exact(coconeIn Pcc (w 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.