Return to Answer

As suggested by the OP, I'm turning my comment into an affirmative answer and editing upon closer examination of Joyal's proof.

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.

A striking feature of Joyal's proof is that he only needs consistency to prove the undecidability of Joyal's sentence, unlike Gödel's original proof requiring $\omega$-consistency for the undecidability of Gödel's sentence. So this workaround provides the undecidability of Joyal's sentence directly from the assumption of consistency, without having to recur to Rosser's trick.

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.

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.

As suggested by the OP, I'm turning my comment into an affirmative answer.

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 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. It is well known that such a fixed point is equivalent to $\neg Prov(\bot)$, i.e., to $Con(PRA)$, and this is also proven categorically by Joyal. The second incompleteness then follows.

A striking feature of Joyal's proof is that he only needs consistency to prove the undecidability of Gödel's sentence, unlike Gödel's original proof requiring $\omega$-consistency. This is because the internalization process inside the arithmetic universe can only be made when the recursively axiomatized extension of $PRA$ contains only coherent sentences as axioms (as opposed to coherent sequents), a fact that is explained by the observation that arithmetic universes are not cartesian closed, and thereby implication is not available. On the other hand, this restriction provides the undecidability of Gödel's sentence directly from the assumption of consistency, without having to recur to Rosser's trick.

While Lawvere's fixed point theorem is quite trivial, Gödel's incompleteness theorems are much 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.

As suggested by the OP, I'm turning my comment into an affirmative answer and editing upon closer examination of Joyal's proof.

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.

A striking feature of Joyal's proof is that he only needs consistency to prove the undecidability of Joyal's sentence, unlike Gödel's original proof requiring $\omega$-consistency for the undecidability of Gödel's sentence. So this workaround provides the undecidability of Joyal's sentence directly from the assumption of consistency, without having to recur to Rosser's trick.

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.

As suggested by the OP, I'm turning my comment into an affirmative answer.

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 at arxiv.org/abs/2004.10482, 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 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. It is well known that such a fixed point is equivalent to $\neg Prov(\bot)$, i.e., to $Con(PRA)$, and this is also proven categorically by Joyal. The second incompleteness then follows.

A striking feature of Joyal's proof is that he only needs consistency to prove the undecidability of Gödel's sentence, unlike Gödel's original proof requiring $\omega$-consistency. This is because the internalization process inside the arithmetic universe can only be made when the recursively axiomatized extension of $PRA$ contains only coherent sentences as axioms (as opposed to coherent sequents), a fact that is explained by the observation that arithmetic universes are not cartesian closed, and thereby implication is not available. On the other hand, this restriction provides the undecidability of Gödel's sentence directly from the assumption of consistency, without having to recur to Rosser's trick.

While Lawvere's fixed point theorem is quite trivial, Gödel's incompleteness theorems are much 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.

As suggested by the OP, I'm turning my comment into an affirmative answer.

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 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. It is well known that such a fixed point is equivalent to $\neg Prov(\bot)$, i.e., to $Con(PRA)$, and this is also proven categorically by Joyal. The second incompleteness then follows.

A striking feature of Joyal's proof is that he only needs consistency to prove the undecidability of Gödel's sentence, unlike Gödel's original proof requiring $\omega$-consistency. This is because the internalization process inside the arithmetic universe can only be made when the recursively axiomatized extension of $PRA$ contains only coherent sentences as axioms (as opposed to coherent sequents), a fact that is explained by the observation that arithmetic universes are not cartesian closed, and thereby implication is not available. On the other hand, this restriction provides the undecidability of Gödel's sentence directly from the assumption of consistency, without having to recur to Rosser's trick.

While Lawvere's fixed point theorem is quite trivial, Gödel's incompleteness theorems are much 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.