What do you mean by the homotopy fiber of a functor? Usually people talk about homotopy fibers when discussing morphisms of spaces, i.e. functors between groupoids, not general categories. In the case of groupoids the formula is indeed the one that you stated. It's often taken as a definition of the homotopy fiber, if you are using some other definition you should state it.

And thus secondly, whatever the extra "global" structure is, it would make the "completed" theory incompatible with classical homotopy theory in a sense that some homotopy equivalent notions and objects would be distinct. The models of spectra seem very much related to this "completed" theory, and the problems with $G$-equivariant theory and geometric topology look like an evidence for this extra structure.

I have speculated in this question that there should be some "completed" homotopy theory which lives not over $\mathrm{Spec}\mathbb Z$, but over $\widehat{\mathrm{Spec}\mathbb Z}$. Now, I don't know what that theory looks like, although I have some guesses, e.g. it should be geometric and at the infinity it should relate to metric geometry. However two things are clear: firstly, all classical stable homotopy theory lives over the open part, since spectra are just souped-up abelian groups. (..cont..)

But I can't imagine how you would connect homotopy theory with practical applications in algebra and differential geometry without specific models. Yes, you could define $G$-equivariant spectra $\infty$-categorically via the orbit categories, once you know that this is a good model of equivariant spectra, and I can't imagine how you would argue that or invent it without models of spectra and spaces. Neither I have a clue how you would move from bordism and surgery theory to homotopy theory without passing through some specific models.

I feel like this question is not specific enough. Homotopy theory is a broad subject, so who precisely is "we" in the question and what do we want to prove? If we restrict the question to proving theorems about homotopy-invariant structures on the homotopy category of spectra, then the answer is most likely "yes, we only need $\infty$-categories, but we would have pigeonholed ourselves into the problem area which $\infty$-categories were designed to be the best tool for. (..cont..)

This seems an invitation to discussion rather than a focused question, so it appears to be offtopic on this site. However, note that the projective spaces in your question aren't really well-defined (neither as projectivizations of some space nor as some algebraic spaces), but rather appear in a very ad-hoc fashion as some special Jordan algebras. Nor are the higher projective spaces over bioctonions etc defined, really. This means there is still no natural series here but rather very different and disconnected examples with only an intuition connecting them.

What is $\mathcal C / F$? Do you mean the overcategory of representables?

I don't think this is a good question for MO. This posts basically asks for open-ended discussion without any specific problem, while MO (and StackExchange in general) are suited for well-defined problems with verifiable solutions. This post is more of a research article posted on a forum. Regarding your question, I find missing in your observations any theorems that would connect your hyperoperations at different level. It's not hard to make up a new group, a family of groups with some strong connections is a much more interesting (a recursive definition on its own is too weak a connection).

@nfdc23 , would you mind turning your comment into an answer?

I always believed that the term "module" for a 2d lattice and the "moduli space" as the space of parameters were directly related. After all, a lattice of the form $\langle 1, \tau \rangle$ is the same as a complex elliptic curve, and the theory of elliptic functions and Jacobi theta functions was well developed by the 1870. People could certainly see the connection between the lattices and the elliptic moduli in the elliptic functions.

It isn't natural to believe that a product of nonempty sets is nonempty once you generalize a bit: an $I$-indexed family of sets $\{ J_i \}_{i\in I}$ is the same as an epimorphism $J \to I$, $J = \sum_{i\in I} J_i$. An element of a product of this family is the same as a section of this epimorphism --- and of course epimorphisms in categories can have no sections! This is true even in categories that are a model of (extensional) set theory, i.e. in toposes like a category of sheaves of sets on a space. E.g. for any nontrivial manifold $X$ its $Sh(X)$ will not satisfy AC.