One weird trick to encode modal types

You can encode modal logics using the module system.

Also private inductive types work for this.

But I’m not really sure this is quite correct or meaningful.

Module ATheorem.
  Axiom t: Set.
  Axiom v: t.
End ATheorem.

Module Type Modal.
  Axiom N: Set -> Set.
  Axiom extract: forall {A}, N A -> A.
  Module Necessity (M: ATheorem).
    Axiom necessity: N M.t.
    Axiom extract_necessity: extract necessity = M.v.
  End Necessity.
  Axiom dist: forall {A B}, N (A -> B) -> N A -> N B.
  Axiom extract_dist: extract (dist f x) = extract f (extract x).
End Modal.