We can in fact instantiate and prove these axioms.

Definition nt := nat.
Definition znt := Z.
Definition snt := S.

(* Define nt_neq etc. *)

Theorem nt_irr : nt_neq / nt_inv / nt_inj / nt_ind.
Proof.
  (* exercise for the reader *)
Qed.

There is some confusion in your terminology. The “irrefutability of the Peano axioms” is better stated by putting the double negation on the outside of the quantification on the nt type and its primitives. Then it’s a straightforward consequence of the fact that the axioms are provable.

Record Peano_theory : Type :=
  { nt : Type
  ; znt : nt
  ; snt : nt
  ; nt_NEQ : forall n: nt, znt <> snt n
  ; (* other axioms here *)
  }.

Theorem Peano_theory_provable : Peano_theory.
Proof.
  refine {| nt := nat ; znt := Z ; snt := S |}.
  (* exercise for the reader *)
Qed.

(* inhabited : Type -> Prop
   https://coq.inria.fr/doc/V8.20.0/stdlib/Coq.Init.Logic.html#inhabited *)
Theorem Peano_theory_irrefutable : ~~ inhabited Peano_theory.
Proof.
  intros H; apply H; constructor; apply Peano_theory_provable.
Qed.

Irrefutability (in the sense of double negation) is not the same thing as consistency. A proof of irrefutability (~~Axioms) implies that you can’t derive a contradiction (consistency) only if you also assume that Coq—or whatever logical system the proof of ~~Axioms lives in—is consistent in the first place. And you can’t say anything about the converse. A set of Axioms could be consistent with Coq without there being a proof of irrefutability, ~~Axioms. Consistency is really a meta-theoretical property, meaning that it’s a property about the logical system (Coq here), which cannot be stated or proved inside of that system. To propertly state consistency as a formal property, one would need to model the logical system explicitly, which entails the many subtleties difficulties of formalizing a logical system within a logical system.