Typo fix: $FinSet^op$ is freely generated by finite limits (not finite colimits).

]]>Added facts about the universal properties of FinSet and its opposite.

]]>Added to *FinSet* a remark on the opposite category $FinSet^{op}$ from a constructive perspective:

“In constructive mathematics, for any flavor of *finite*, $\mathcal{P}$ defines an equivalence of $FinSet$ with the opposite category of that of those complete atomic Heyting algebras whose set of atomic elements is finite (in the same sense as in the definition of $FinSet$).”

I don’t know whether for some values of *finite*, this characterization can be made more interesting, i.e. whether we can give a condition which does not explicitly mention the set of atomic elements.

I have briefly recorded the equivalence of FinSet${}^{op}$ with finite Booplean algebras at *FinSet – Properties – Opposite category*. Then I linked to this from various related entries, such as *finite set*, *power set*, *Stone duality*, *opposite category*.

(I thought we long had that information on the $n$Lab, but it seems we didn’t)

]]>