A partitioned category with a set of terminal objects

Stream: Is there code for X?

[Kenny Lau]

While making #27309 I came across a category C with this interesting property:

There is a (small) set of objects s : Set C such that for every c c' : C with c' ∈ s, the type c ⟶ c' is a subsingleton, and for every c : C there is c' ∈ s with an arrow c ⟶ c', and there are also no non-trivial arrows within s.

In other words, s witnesses a disjoint partition of C where there are no arrows between two different parts, and the c' ∈ s is a terminal object in each part.

Is there a term for something like this?

[Aaron Liu]

Did it follow that there are no arrows between two different parts?

[Kenny Lau]

no, but it was true :upside_down: