Specialization and instantiation

Two orderings run through the model, and conflating them is the common error.

Specialization, A <: B, holds between concepts: every instance of A is an instance of B. It is a statement about classes, reflexive and transitive.

pub type Person { name: String, age: Nat }
pub type Employee <: Person { employer: String }
pub type Manager  <: Employee;

Manager <: Employee <: Person, so by transitivity every manager is a person. <: orders the vocabulary: it lays out which classes refine which, before any individual exists.

Instantiation, x : A — equivalently iof(x, A) — relates an individual to a concept. It is not transitive, and it is what populates the order <: lays out.

pub fact Manager(dana);

dana : Manager holds by assertion. dana : Employee and dana : Person hold too — not because instantiation chains, but because specialization carries membership upward: an individual in a subclass is in every superclass. The two orderings meet exactly here. <: is the rule; instantiation is the consequence of applying it.

The extent of a concept is the set of individuals that instantiate it. extent(Person) includes dana, because Manager <: Person lifts her into it. This is the distinction that matters for reasoning: rules and queries compute over extents — sets of individuals — never over the subtype relation itself. <: decides who is in an extent; it is not a thing the engine ranges over. The subtyping rules and the upward closure of membership are specified in Subtyping; the intrinsics that read both orderings are in Reflection.