Colimits in HSET

[vladimirias]

1. To construct colimits of arbitrary functors C -> HSET (using setquot)
2. To construct, for any h-set X an isomorphism between X and the colimit of its finite subsets (a finite subset is defined as S : X -> hProp such that isfinite ( carrier S ) ) .

I have looked through it on paper and it seems to work.

[DanGrayson]

I suppose the same is true for the colimit of the finite sets T mapping to X. Would both suffice for the application envisioned?

[vladimirias]

I guess so.

[langston-barrett]

We have

Lemma ColimsHSET : Colims HSET.

So it seems that (1) is already done.

[peterlefanulumsdaine]

Reopening since I think the result formalised in #1564 isn’t quite the right result here (although it is indeed the result Vladimir originally asked for).

The point is that for most of the intended applications, we need a set exhibited as a directed colimit of finite sets — and the diagram of all finite subsets of a set (as considered in #1564) will be directed iff LEM holds. But there are two alternatives which are directed without needing to assume LEM:

• the diagram of all maps from finite sets into X (as @DanGrayson suggested above)
• the diagram of all Kuratowski-finite subsets of X

(Here Kuratowki-finite, or K-finite for short, means “admitting a surjection from some {1,…,n}”. Our definition of finite is “admitting an equivalence with some {1,…,n}”, which is of course classically equivalent; constructively it’s sometimes called cardinal-finite to avoid ambiguity.)

So I’m reopening this issue to ask for the colimit result also to be given for at least one of the two diagrams above. And it would be great if the directedness of the diagram could be given as well!

If I remember right, we already have a treatment of directedness/filteredness in the CategoryTheory library; I don’t remember if we have K-finiteness anywhere, will check later.

[m-lindgren]

In a private repo / external to UniMath I have proof that every set is a filtered colimit of its K-finite subsets. I can maybe try to integrate it with UniMath this weekend. As far as I know K-finiteness is not defined in UniMath currently, so would have to include that in the PR unless it's already in there somewhere. Same with filteredness.

I have an half-finished attempt to formalise filtered colimits/compactness/locally finitely presentable categories + some applications (last time I looked at it I was stuck on proving that filtered colimits commute with finite limits in SET, maybe I should take a look at it again)

[peterlefanulumsdaine]

Those would be marvellous to have!

[arnoudvanderleer]

@peterlefanulumsdaine This is resolved now, right?