Modularizing Coq scripts with defining Parameters/proving Axioms

Using Coq
1

I have this coq file, for example aFile.v, that has a bunch of definitions and parameters and axioms and lemmas, some depending on each other. So for example, let’s say aFile.v looks something like this:
Definition def1 := .. Parameter param1 :=.. Definition def2 :=.. (* uses parameters & definitions from above *) Axiom ax1 :.. (* uses parameters & definitions from above *) Lemma lem1: (* uses parameters & definitions from above *)

Is there a way to turn this file into something like a module that I can instantiate in other coq files in a way that allows me to define the parameters and prove the axioms in this instantiation?
I tried turning it into a module type, but then when I tried instantiating it I had to basically write down all the definitions again, otherwise I’d get an error. I want something similar to this but where I only define Parameters and prove Axioms, and any Definitions or Lemmas are just imported as is.

2

Here is a very basic example, but it can get more complicated, e.g. if you need multiple levels/paths of inheritance, and/or if you need to share concrete definitions, not just parameters and axioms, etc.

Module Type MySpec.

  Parameter X : Type.

  Axiom X_inhabited : X.

End MySpec.

Module MyModule <: MySpec.

  Definition X := Prop.

  Lemma X_inhabited : X.
  Proof. apply True. Qed.

End MyModule.

Import MyModule.

Print X.            (* X = Prop : Type *)
Print X_inhabited.  (* X_inhabited = True : X *)

A slightly more sophisticated example is here, see the modules GnpSpec, GnpLogic, and GnpLogic_NatEq, where beside modules, functors (module constructors) and module types, I am using the Include command: Grelling–Nelson Paradox (in Coq) · GitHub