As far as I know, there is no published attempt at a "circular" foundations of mathematics though I'ave seen it noted by many category theorists and logicians without in-depth analysis, e.g Notes on predicate logic. The current and past attempts at foundations of math seem to be about choosing the right axiomatic schema and universes in which math can be formalized. Notable examples include set theory-ZFC, homotopy type theory/Univalent foundations-HoTT and $\infty$-categories.
I will try to explain what I mean by circular foundations. By the syntax-semantics duality, every theory corresponds to the internal logic of some category which acts as the model. The category itself has a definition which serves as the metatheory, with a new model, it's metamodel. This process seems to be an infinite regress which may converge on itself forming a loop of meta-theories. This means that any foundations of math based on axiom schemas should be subject to such circularity or at least regression. A circular foundation seems to have 'uncommon' consequences, which by stating them I hope will help give a deeper understanding into the question:
- No axiom is irrelevant, because it is math itself which decides what theory will be the background of another theory.
- Math maybe quasi-empirical, because by being 'self-delimiting' it is independent of mathematicians whose work then should be only to observe it unfold. That is, self-reference may imply the objective reality of math.
Have such claims been considered in-depth ?
Edit : This is my attempt to have a precise formulation of "circularity"(I may be wrong)
Let $\mathfrak C$$_H$ and $\mathfrak C$$^H$ be the kleisli and eilenberg-moore categories on some monad H respectively. Then the syntax-semantics duality is between a term algebra $\mathfrak C$$_H$ and its model $\mathfrak C$$^H$. I propose that a syntax-semantics duality is a lifting of the corresponding meta-syntax-semantics duality between the metatheory and metamodel with this forming an algebraic square as defined here. Then by monadic decomposition, iterated lifting should converge forming an 'infinite regress' of metatheories. I interpret the two different possibilities of Kleisli lifting and Eilenberg-moore lifting as the concept of "meta" and its dual.
Best Answer
This is not exactly an answer, but the name I think of here is Jon Barwise. He has a book with Moss, called Vicious Circles, which uses non-well founded set theory (following Peter Aczel) not only to discuss foundations but serious applications to things like computer science and fixed point theorems.
Maybe more relevant to the foundational questions would be his book Admissible Sets and Structures, which starts off by developing a weak (non-well founded, but in a different way) set theory called "Kripke-Platek" as a tool to study definability and infinitary logics.
A final comment: this answer doesn't directly talk about homotopy type theory or univalence. Much of Barwise's work involves applying non-well founded ideas to understand second-order set theory. Once you remember the 'point' of set theory is to write all these different kinds of mathematics within the same first-order theory, the fact that second-order set theory is a thing might be kind of.... hrm. My point is, you can insist on categorical terminology, but already at the 'set level' so to speak, this question is pretty interesting.
Best