Definition is_filtered_alt (J : category) : UU := ∥ J ∥ × (∏ (d : diagram bool_graph J), ∃ z : J, cocone d z) × (∏ (d : diagram pair_graph J), ∃ z : J, cocone d z).
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.