[0,1] does not have exact filtered colimits (?)

[catdat-issue-creation]

Colimits in [0,1] are given by sup (=max if the colimit is finite), and finite limits in [0,1] are given by inf (=min if the limit if finite). All limits and colimits can be made (co)filtered.

Now consider the collection of elements

x_{0,0} = 1
x_{0,1} = 0
x_{1,0} = 0
x_{1,1} = 1

(indexed by {0,1} \times {0,1}). We have

min_i max_j x_{i,j} = 1

and

max_j min_i x_{i,j} = 0.

---

This issue has been created by Ben Spitz via the submission form on https://catdat.app/category/real_interval

[diracdeltafunk]

Sorry, this is wrong. I forgot that x_{i,j} needs to be monotone in j to give a filtered colimit in that variable! Please close and ignore.

[ScriptRaccoon]

Yes, indeed [0,1] has exact filtered colimits. There is a general implication that I will add and which implies this.

[diracdeltafunk]

Cheers, I was about to submit another issue with a proof of this :)

[ScriptRaccoon]

Yes, indeed [0,1] has exact filtered colimits. There is a general implication that I will add and which implies this.

Done in #84