Notation for modules (as in Coq modules)

Question

Wondering if there is a math notation for "modules", such as in Coq modules:

Module Type Sig.
Parameter A : Type.
Parameter le : A ⇒ A ⇒ Prop.
Infix "≤" := le : order_scope.
Open Scope order_scope.
Axiom le_refl : ∀ x, x ≤ x.
Axiom le_antisym : ∀ x y, x ≤ y ⇒ y ≤ x ⇒ x = y.
Axiom le_trans : ∀ x y z, x ≤ y ⇒ y ≤ z ⇒ x ≤ z.
Axiom le_total : ∀ x y, {x ≤ y} + {y ≤ x}.
Parameter le_dec : ∀ x y, {x ≤ y} +{¬ x ≤ y}.
End Sig.

Here, you define basically a block of equations in a module. Wondering if there is any equivalent math notation for this sort of thing.

Answer 1

I think you’re asking if “modules” as a way of organising classical mathematics exists, in which case the answer is not really.

Modules are a way of structuring things that is understandable to a computer. However, most of math is done in a way that is supposed to be interpreted by humans, so it is structured for humans where similar goals are achieved by:

• dividing material into book, papers, classes, and so on,
• dividing those further into parts, chapters, section, and so on,
• relying on our ability to infer things from context, so a parameter like above might be introduced by a sentence like “In this section, let $A$ denote any type and let $\leq$ be a relation on $A$”, though it is not uncommon to repeat these assumptions (at least partially) for every lemma and theorem,
• “importing” other results by citing the relevant paper or book.

There is no strict notation for this; natural language is your friend.

The reason is probably that strict notation only becomes useful when you to start analysing an object. But studying these “modules” is not something a lot of mathematicians would be interested in, I suppose.

(If you are asking about modules as a subject of study in type theory or the theory of programming languages then I don’t know. Probably people just reuse the notation from the language they are studying.)