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][1] ($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][2].

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.


  [1]: https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic
  [2]: https://en.wikipedia.org/wiki/Rosser%27s_trick