In the context of dependent type theory, we show that coinductive predicates have an equivalent topological counterpart in terms of coinductively generated positivity relations, introduced by G. Sambin to represent closed subsets in point-free topology. Our work is complementary to a previous one with M. E. Maietti, where we showed that, in dependent type theory, the well-known concept of wellfounded trees has a topological counterpart in terms of proof-relevant inductively generated formal covers used to provide a predicative and constructive representation of complete suplattices. The proofs performed within Martin–Löf’s type theory and the Minimalist Foundation have been checked in the Agda proof assistant.

The results of Section 3.1 of the 2017 paper “Isomorphism Theorems between Models of Mixed Choice” need an additional assumption when $\bullet$ is “$1$.” If $\bullet$ is nothing or “$\leq 1$,” no change is needed. Also, the mistake only applies to the angelic cases, namely to the maps $r_{{\mathtt {A}}{\mathtt {P}}}$ and $s^\bullet _{{\mathtt {A}}{\mathtt {P}}}$; the demonic cases $r_{{\mathtt {D}}{\mathtt {P}}}$ and $s^\bullet _{{\mathtt {D}}{\mathtt {P}}}$ are unaffected. If $\bullet$ is “$1$,” and in the angelic cases, instead of just assuming that $\mathcal L X$ is locally convex, we need to additionally assume that $X$ is compact, or that $\mathcal L X$ is locally convex-compact, sober, and topological – for example, if $X$ is core-compact – or that $X$ is LCS-complete, namely, a homeomorph of a $G_\delta$ subspace of a locally compact sober space.

We develop the theory of limits and colimits in $\infty$-categories within the synthetic framework of simplicial homotopy type theory established by Riehl and Shulman. We also show that in this setting, the limit of a family of spaces can be computed as a dependent product.