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