16. The object type
A measured quantity is always the property of some object — the length of this pencil, the glucose concentration of this plasma sample — and R19 puts that object in the type. What kind of thing an object may be is a separate question, and this chapter is its answer: the object is drawn from an arbitrary type, and the consequences of that decision are not symmetric.
Two things are wanted of an object, and they turn out to have different prices.
Discrimination — telling two objects apart — is what the gate needs, and it is
free. It is definitional equality of a type index, a mechanism every type in Lean
already has. The evidence is a measurement of the instance layer itself: of the
declarations in IndividualQuantity, exactly one reads its object. add,
mul, div, recip and all three classification certificates carry o and never
inspect it. What stops a length of R1 multiplying a width of R2 is that the two
types differ, and nothing else.
Designation — naming an object in the terminological vocabulary — is what
Dybkær's instance layer consumes, and it is not free. It is supplied by
Designated (the foundations chapter), and an object type that has no identity of
its own has no instance. (The Chapter 20 dedicated kind consumes the object's
sort, not its name — that half is Sorted's, in the same chapter.)
The asymmetry is the point. A host library's own objects — the particles of a mechanical system, the cells of a mesh, the pixels of a scene — can be gated with nothing supplied, on their own types, without that library changing. They cannot be named, and the layer says so rather than inventing a name that is not there.