One weird trick to encode modal types

Using Rocq
1

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.