Meaning
A proposal is well typed when every component has the right declared source, target, and conditions of use.
Each arrow must say what it acts on and where it lands. Representations must be genuine or marked unverified. Coefficient lines and fillings must have specified bases, boundaries, and coefficient systems. Seams and comparisons must state their validity conditions. These checks make the proposed operations meaningful.
Example (illustrative)
If A maps H₁ to H₂ and B maps H₂ to H₃, then BA has a declared meaning. If B instead expects vectors in an unrelated space K, writing BA does not repair the missing identification.
Scope and limits
Correct typing is a prerequisite for a physical realization. It does not prove existence, positivity, or any analytic estimate.
Source
GAT 0 — Finite Cohomological and Coercive Recognition. GAT 0, Definition 3.2.