At various points, we would like to quantify internally not over all types, but over "locally locally constant sheaves" (?). For example, naively we would say a general (not necessarily quasi-compact) open proposition is one of the form $\exists (i : I), f(i) \ne 0$, where $I$ is some type and $f : I \to R$. But if we allow all types, then every proposition $P$ is open (take $I = P$ and $f$ constantly $1$). Instead we restrict to finite types.
But how about the following more general notion. (I think we discussed something like this at SAG 2 with @iblech.) We define what it means for a (0-truncated) type $I$ to be external. It is a general fact that $I$ is the filtered colimit of $[n]$ over all $n : \mathbb N$ and maps $[n] \to I$. Say $I$ is external if this colimit is preserved by the functor $(-)^X$ for every affine scheme $X$. I think this means that any map $X \to I$ factors through $[n]$ for some $[n]$, and that two maps $X \to [n] \to I$ and $X \to [m] \to I$ are equal only if there is a common co-refinement $X \to [k] \to I$ (via maps $[n] \to [k]$, $[m] \to [k]$ making everything commute). For example $\mathbb N$ (by boundedness) and any finite set should be external.
I don't know if this is exactly the right definition. But my question is: can we use some definition like this to go beyond finiteness restrictions in SAG, to define general opens and perhaps general schemes (not necessarily finitely presented)?
