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.
```