Has Goedel's Second Incompleteness Theorem been proven using Lawvere's Fixed Point Theorem?

Question

This question is a request for assistance in surveying the existing literature on applications of Lawvere's Fixed Point Theorem (LFPT).

Yanofsky [0] has demonstrated several applications of LFPT to prove various limitative results, in particular Goedel's First Incompleteness Theorem, and alludes to its applicability for proofs of the Second Incompleteness Theorem:

Goedel’s second incompleteness theorem about the unprovability within arithmetic of the consistency of arithmetic. This theorem is a simple consequence of the first incompleteness theorem. However Kreisal has a direct model theoretic proofs that uses a diagonal method (see, e.g., page 860 of Smorynski’s article in [1].) This proof seems amenable to our scheme.

Has there been any work conducted to further this vein of inquiry? Can the LFPT be used to prove Goedel's Second Incompleteness Theorem?

[0] https://arxiv.org/abs/math/0305282

[1] Handbook of mathematical logic. North-Holland Publishing Co., Amsterdam, 1977. Edited by Jon Barwise, With the cooperation of H. J. Keisler, K. Kunen, Y. N. Moschovakis and A. S. Troelstra, Studies in Logic and the Foundations of Mathematics, Vol. 90.

Answer 1

As suggested by the OP, I'm turning my comment into an affirmative answer. WARNING: The presentation of Joyal's proof in the paper I cited contains an incorrect conclusion about Joyal's sentence (that it is undecidable from mere consistency). I have modified my answer accordingly.

Both Gödel's first and second incompleteness theorems have been proven by André Joyal mimicking the arithmetization of metamathematics in Gödel's original proof with internal reasoning inside the initial arithmetic universe. This latter is none other than (the pretopos completion of) the syntactic category, in coherent logic, of the sequents expressing the axioms of primitive recursive arithmetic ($PRA$); in particular the type theoretic treatment of arithmetic universes is not really needed in the proof. Joyal gives an alternative construction of the initial arithmetic universe by defining the category of primitive recursive predicates, which corresponds to taking a different site of definition of the classifying topos (Coste's construction).

The proof has been very recently made available on arxiv in the paper of van Dijk/Oldenziel, although it's been part of categorical folklore since the seventies. Once an internal initial arithmetic universe has been shown to exist inside the initial arithmetic universe, its externalization provides the Gödel numbering of formulas, and one can define functorially the provability predicate $Prov(x)$. Then the proof of the incompleteness theorems proceeds by building a self-referential sentence similar to Gödel's sentence "I am not provable", exactly as Gödel did, using that this sentence is the fixed point of $\neg Prov(x)$, and an argument essentially equivalent to applying Lawvere's fixed point theorem provides its construction. The sentence is however slightly changed to "I am provably false" (which I call Joyal's sentence, the fixed point of $Prov(\neg x)$). It is well known that a fixed point for $\neg Prov(x)$ is equivalent to $\neg Prov(\bot)$, i.e., to $Con(PRA)$, and similarly Joyal also proves categorically that Joyal's sentence is equivalent to $Incon(PRA)$.

The second incompleteness then follows from the observation that Joyal's sentence cannot be provably false (though for certain consistent but $\omega$-inconsistent recursive extensions of PRA it can very well be provably true; here's what goes wrong with the conclusion of the cited paper).

While Lawvere's fixed point theorem is quite trivial, Gödel's incompleteness theorems are much deeper, more complex and subtle than just the fixed point lemma, since they contain the arithmetization of syntax, which Joyal has shown to correspond precisely to internal reasoning inside the arithmetic universe (it is certainly not trivial at all to internally construct an arithmetic universe inside an arithmetic universe). His proof thus deserves to be much widely known than it is.