16.3. The generality of the paradigm🔗

It is tempting to read the census as a taxonomy the calculus provides — six kinds of object, pick one. It is the opposite. PKC contributes no taxonomy of objects; it contributes the fact that it needs none.

What a metrology layer must have of an object is discrimination, and discrimination is what a type is. So every entry in the census is either a type the host library already has (nominal, structural, indexed, singleton) or an ordinary type former applied to such types (composite, joint) — and the gate on all of them is definitional equality, which comes with the type and costs nothing to carry.

That is why the shapes compose without any provision being made for it. A quantity of this instrument, at this pixel, of that particle is a quantity of the triple Object × Cell × Particle, and its gate is the triple's own equality: differ in any one factor and the sum is refused. Nothing in the library knows that this combination exists.

16.3.1. What the library ships, and what it refuses to ship🔗

Exactly two things do not come from the type former:

The one object type a host cannot have. A whole is not one of its parts, so a part type does not contain the assembly, so the total has nowhere to live. The composite is that type, and it is the only object construction this library ships.

Closure of designation. Naming a derived object is a terminological commitment, not a derivation, and the library states the obligation instead of guessing the convention. The composition principle is that a designation travels along an injection; the injectivity is the author's claim, decide for a finite object type and a lemma otherwise.

The refusal is the substantive half. An automatic designation for pairs would have to join two names into one, and the encoding an author reaches for first — concatenate with a separator — is not injective, because the separator can occur inside a name. Two different couplings, one name, silently. The Examples library carries that counterexample as a compiled fact; it is the reason Designated carries an injectivity field rather than a docstring.

Definition16.3.1.1

Group: The object of an individual quantity (the foundations chapter's mode) ranges over an arbitrary type. The gate needs nothing from it; the designation needs Designated , whose injectivity field is what distinguishes a designation from a formality. (7)

Group member previews

Preview

Definition 16.4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

Designation travels along an injection. An object type that injects into a designated one is designated: name each object by the name of its image. This is the composition principle for the whole census — an index family, a combination of factors, a sub-selection of a named set — and the only one most models need.

Lean code for Definition16.3.1.1●1 definition

defdefined in PropertyKindCalculus/Foundations.lean

complete

def PropertyKindCalculus.Designated.ofInjective.{u, v} {O : Type u}
  {P : Type v} [PropertyKindCalculus.Designated P] (f : O → P)
  (hf : ∀ {x y : O}, f x = f y → x = y) :
  PropertyKindCalculus.Designated O

def PropertyKindCalculus.Designated.ofInjective.{u,
    v}
  {O : Type u} {P : Type v}
  [PropertyKindCalculus.Designated P]
  (f : O → P)
  (hf : ∀ {x y : O}, f x = f y → x = y) :
  PropertyKindCalculus.Designated O

**Designation travels along an injection.** An object type that injects into a designated
one is designated: name each object by the name of its image. This is the composition
principle for the whole census of object shapes — an index family, a structural object with a
key, a sub-selection of a named set — and it is the only one most cases need.

The injectivity hypothesis is the *author's* claim about `f`, and for a concrete finite object
type it is discharged by `decide`.

Proof for Definition 16.3.1.1

uses 0

Compose the two maps and the two injectivity proofs. A definition, not an instance: which naming a model uses is the model's decision, and instance search finding one by accident is the failure designation_inj exists to prevent. Designated.prod is its specialization to a pair, taking the join of two names and the proof that the join is injective.