Let \(T\) be a base type theory. We work in type theory of spaces in \(T\). We say a point of \(\mathcal {E}\) is finitely presented if it is constructed from \(\mathord {\textnormal {\textsf {1}}}\) by finite colimits.
Let \(T\) be a base type theory. We work in type theory of spaces in \(T\). We say a point of \(\mathcal {E}\) is finitely presented if it is constructed from \(\mathord {\textnormal {\textsf {1}}}\) by finite colimits.