A Type describes a property of a Term. Terms are multifaceted and can be described from a variety of perspectives. A Term can have multiple properties, so Terms can also have multiple Types.
Each Term is associated with a singular Type Expression. A Type Expression represents all properties of that term, structured in Conjunctive Normal Form (CNF). Conjunctive Normal Form is just a way of saying that all the Ands are at the top level, above the Ors.
Two Types can be attached to one Term.
a: Integer + Prime
One Type can imply another Type. When this happens there is an implicit expansion of the implication to enforce CNF.
type Aa: Bb; a : Aa // Aa + Aa => Bb //rewrite as just Aa + Bb a : Aa + Bb