I am confused about an issue in set theory.

Tychonoff's theorem says that "an arbitrary product of compact topological spaces is compact". We often talk of an index set $I$ and then for each $n\in I$ we have a compact topological space $X_n$, and the claim is that $\prod_{n\in I}X_n$ is compact. There's a really cool super-short proof of this using filters by the way ;-)

My question is about how one might formalise this in ZFC. In Lean I just found myself writing `X : I → Type` for the family, and in the set theory model of Lean this is a "function" from a set $I$ to "the universe of all sets". This can't be done in ZFC, so one might want to start brandishing the axiom of replacement around a bit. My question is I think on the details of this.

Let's say I'm talking to you, a set theorist, and I ask you what your definition of a topological space structure is. You say it's an ordered pair consisting of a set $X$ and a topology $\mathcal{T}$ on $X$, which is a collection of subsets of $X$ satisfying some axioms. I say great, I write a few lines of computer code (just a small interface corresponding to your definition), run a proof checking system on my code, and it outputs a Haskell function which takes as input a natural number `n` and then prints out two strings which (after coming to some arrangement about parsers) uniquely define a set `X n` and a topology `T n` on `X n`. Furthermore I can prove that `X n` is compact for all `n` and indeed a computer has checked my proof, but I won't bore you with the details. The question is how now to *state* that the product of the `X n` is compact in ZFC, because I have not given you a function in the internal sense of a set which happens to be a function in the sense that it's a set of ordered pairs blah blah blah.