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][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][2], 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][3].

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.


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