Lemma is_filtered_kfinite_subsets (X : hSet) : is_filtered (kfinite_subsets_category X). Proof. intros g d gfinite. apply hinhpr. simple refine(_ ,, _). - exact(kfinite_subtype_union (dob d) (finite_vertexset gfinite)). - use make_cocone. + apply subtype_union_containedIn. + abstract(red; intros ; apply funextsec; intro ; apply funextsec; intro ; apply squash_path). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.QuotientSet. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Filtered. Require Import UniMath.CategoryTheory.Limits.StandardDiagrams. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Combinatorics.KFiniteTypes. Require Import UniMath.Combinatorics.KFiniteSubtypes.