There is a generalization of Gödel's incompleteness theorem that is more naturally applicable to MLTT: Löb's theorem says that to prove $P$, it suffices to prove that $P$ is true whenever $P$ is provable. Symbolically, using $\square P$ to mean "$P$ is provable", this is $$\square(\square P \to P)\to \square P$$

If you instantiate $P$ with a contradiction (say, $1=0$ or $\bot$), you get Gödel's incompleteness theorem: $$\square(\square \bot \to \bot)\to \square \bot$$ or, using the fact that $\neg A$ is $A\to \bot$, $$\square(\neg\square \bot)\to \square \bot$$ If your theory is consistent, i.e., if $\square P \to P$, then this becomes $$\neg\square(\neg\square \bot)$$ or "you cannot prove that there is no prove of false". In the standard phrasing of Gödel's incompleteness theorem, this would be "the statement 'there is no proof of false' is true, but unprovable".

While formalizing theorems and proofs using natural numbers is standard in set theory, in MLTT, it's much more natural to formulate provability by giving an inductive type of theorems (also called types), and an inductive type of proofs (also called terms).

A standard presentation of simply typed lambda calculus in HOAS might define (using Agda notation)

open import Agda.Builtin.Unit

infixr 1 _‘→’_

data ⊥ : Set where

data Type : Set where
  _‘→’_ : Type → Type → Type
  ‘⊤’ : Type
  ‘⊥’ : Type

⟦_⟧ᵀ : Type → Set
⟦ A ‘→’ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
⟦ ‘⊤’ ⟧ᵀ = ⊤
⟦ ‘⊥’ ⟧ᵀ = ⊥

data Term : Type → Set where
  lam : ∀ {A B} → ( ⟦ A ⟧ᵀ → Term B ) → Term (A ‘→’ B)
  app : ∀ {A B} → Term (A ‘→’ B) → Term A → Term B
  ‘tt’ :  Term ‘⊤’

⟦_⟧ᵗ : ∀ {T} → Term T → ⟦ T ⟧ᵀ
⟦ lam f ⟧ᵗ = λ a → ⟦ f a ⟧ᵗ
⟦ app f a ⟧ᵗ = ⟦ f  ⟧ᵗ ⟦ a ⟧ᵗ
⟦ ‘tt’ ⟧ᵗ = tt

Out interpretation function, ⟦_⟧ᵗ, proves that this theory is consistent relative to Agda. Said another way, we can use ⟦_⟧ᵗ to prove that no Term inhabits the empty type, ‘⊥’:

¬_ : Set → Set
¬ A = A → ⊥

□ = Term

consistent : ¬ □ ‘⊥’
consistent = ⟦_⟧ᵗ

Now, here is a neat trick you can play to get most of the power of Löb's theorem when your formalization is not HOAS: given any formalization of type theory (or lambda calculus) with a sufficiently nice proof of consistency relative to Agda (i.e., an interpretation function that is simple or local enough that the theory can be extended without needing to modify the interpretation of existing constructs), you can add a term for Löb's theorem, and give it an interpretation.

We extend the definition of Types with a type of theorems (named ‘□’), and we extend the type of Terms with a proof of Löb's theorem. To satisfy the positivity checker, we index terms over a context, rather than using HOAS.

record _×_ (A : Set) (B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

data Type : Set where
  _‘→’_ : Type → Type → Type
  ‘⊤’ : Type
  ‘⊥’ : Type
  ‘□’ : Type → Type

Now we have an inductive type of Contexts, which is a list of Types which can be accessed via variables:

data Context : Set where
  ε : Context
  _▻_ : (Γ : Context) → Type → Context

data Term : Context → Type → Set where
  lam : ∀ {Γ A B} → Term (Γ ▻ A) B → Term Γ (A ‘→’ B)
  app : ∀ {Γ A B} → Term Γ (A ‘→’ B) → Term Γ A → Term Γ B
  var₀ : ∀ {Γ A} → Term (Γ ▻ A) A
  varₙ : ∀ {Γ A B} → Term Γ A → Term (Γ ▻ B) A
  ‘tt’ : ∀ {Γ} → Term Γ ‘⊤’
  Löb : ∀ {P} → Term ε (‘□’ P ‘→’ P) → Term ε P

Note that we only add a constructor for Löb's theorem in the empty context.

We can again define interpretation functions, proving that this theory is consistent relative to Agda:

□ = Term ε

⟦_⟧ᵀ : Type → Set
⟦ A ‘→’ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
⟦ ‘⊤’ ⟧ᵀ = ⊤
⟦ ‘⊥’ ⟧ᵀ = ⊥
⟦ ‘□’ P ⟧ᵀ = □ P

⟦_⟧ᶜ : Context → Set
⟦ ε ⟧ᶜ = ⊤
⟦ Γ ▻ A ⟧ᶜ = ⟦ Γ ⟧ᶜ × ⟦ A ⟧ᵀ

⟦_⟧ᵗ : ∀ {Γ T} → Term Γ T → ⟦ Γ ⟧ᶜ → ⟦ T ⟧ᵀ
⟦ lam f ⟧ᵗ Γᵥ = λ a → ⟦ f ⟧ᵗ (Γᵥ , a)
⟦ app f a ⟧ᵗ Γᵥ = ⟦ f ⟧ᵗ Γᵥ (⟦ a ⟧ᵗ Γᵥ)
⟦ var₀ ⟧ᵗ (Γᵥ , a) = a
⟦ varₙ v ⟧ᵗ (Γᵥ , a) = ⟦ v ⟧ᵗ Γᵥ
⟦ ‘tt’ ⟧ᵗ Γᵥ = tt
⟦ Löb interp ⟧ᵗ tt = ⟦ interp ⟧ᵗ tt (Löb interp)

Note the interpretation of Löb's theorem: the premise of Löb's theorem, across the Curry-Howard isomorphism, is (syntax for) a compiler or an interpreter: it is a thing that takes in syntax for a term of type $P$ and spits out an actual term of type $P$. Since our interpretation function is nicely local, we can use this interpreter to interpret Löb's theorem! Note that this is very similar to the proof that the Halting Problem is undecidable; there, you take a putative decider, and run it on a slight modification of itself, causing it go awry; here you take a putative interpreter, and run it on a wrapped version of itself, causing it to loop.

Finally, we can get consistency and incompleteness of this theory:

¬_ : Set → Set
¬ A = A → ⊥

‘¬’_ : Type → Type
‘¬’ P = P ‘→’ ‘⊥’

consistent : ¬ □ ‘⊥’
consistent absurd = ⟦ absurd ⟧ᵗ tt

incomplete : ¬ □ (‘¬’ (‘□’ ‘⊥’))
incomplete interp = ⟦ Löb interp ⟧ᵗ tt

This argument does not show that Löb's theorem is provable in MLTT; it merely argues that Löb's theorem is admissible as an axiom in MLTT (and hence is true as a metatheorem of MLTT). If you are interested in actually constructing the Löbian sentence in a formalization of MLTT based on simpler primitives, I refer you to this blog post by Neelakantan Krishnaswami on how Löb's theorem is basically the same thing as the Y combinator, or to this unpublished paper that I wrote about a formalization similar to the one described here, or to this repo where I have a number of stabs at formalizing variants of Löb's theorem.

To answer your questions more directly:

1. How can we construct the Gödel’s sentence $G$ in MLTT?

You can axiomatize it as part of your formalization of MLTT (and show that doing so doesn't break consistency); or you can construct it in a way analogous to the Y combinator.

3. What interpretation are we referring when we say that $G$ is true?

As I understand it, when you define syntax for a theory, you should also define a standard model, and an interpretation function into that model. In the formalization I gave above, the standard model is Agda, and the interpretation function is ⟦_⟧ᵀ for theorems and ⟦_⟧ᵗ for proofs. To say that something is "true" is to say that it is true in the model, i.e., is provable of the model. Hence a proof of "P is true in the standard model" is an inhabitant of ⟦ P ⟧ᵀ.

2. How come there is no contradiction if $G$ is true but it is not inhabited?

The better question is, what would the contradiction be? Inhabitation talks about syntax trees, while truth talks about inhabitation of the interpretation of a type. It is very simple to have a syntactic type with no syntactic term of that type, but to say that the interpretation of that type is $\top$. To make this more concrete, here is a formalization of a theory where every sentence is true but unprovable:

data Type : Set where
  ‘⊤’ : Type

data Term : Type → Set where

⟦_⟧ᵀ : Type → Set
⟦ ‘⊤’ ⟧ᵀ = ⊤

⟦_⟧ᵗ : ∀ {T} → Term T → Set
⟦ () ⟧ᵗ

¬_ : Set → Set
¬ A = A → ⊥

true : (T : Type) → ⟦ T ⟧ᵀ
true ‘⊤’ = tt

unprovable : (T : Type) → ¬ Term T
unprovable ‘⊤’ ()