proposition: Lemma filtered_alt_has_discrete_cocones_stn {J : category} (filtalt : is_filtered_alt J) (n : nat) (d : diagram (discrete_graph (⟦ n ⟧)) J) : ∃ z : J, cocone d z.
proof: Proof. destruct filtalt as [inhab [boolcc paircc]]. induction n as [| n IHn]. - use(hinhfun _ inhab). intro j. exists j. use make_discrete_cocone. exact(λ x : ⟦ 0 ⟧, fromempty (negstn0 x)). - set (d₁ := make_discrete_diagram (λ k : ⟦ n ⟧, dob d (dni lastelement k))). use(IHn d₁); intros [P Pcc]. set (d₂ := make_bool_diagram P (dob d lastelement)). use(boolcc d₂); intros [Q Qcc]; apply hinhpr. exists Q. use make_discrete_cocone. + apply(weqonsecbase (λ (v : ⟦ S n ⟧), J ⟦ dob d v, Q ⟧) (weqdnicoprod n lastelement)). apply coprod_rect. * exact(λ k : ⟦ n ⟧, coconeIn Pcc k · coconeIn Qcc true). * apply unit_rect. exact(coconeIn Qcc false). 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