# Individuation

This module defines the abstract individuation interface used by a referential regime.

Individuation distinguishes:

• candidate presentations;
• admissible whole-directed presentations;
• successful singular presentation of one whole; and
• dyadic identity between successful presentations.

The distinction between one and sameUnit is intentional:

• one is a monadic unity judgment;
• sameUnit is a dyadic identity judgment.

Carrier equality is not identified with either judgment.

The account remains abstract. No decidability, finiteness, enumeration, equivalence-relation laws, semantic-status representation, or computational procedure is assumed here.

structure SE.Substrate.IndividuationAccount (Referent : Type u) : Type (u + 1)

An individuation account for one referent kind.

The account itself represents the governing individuation criterion. Context supplies the circumstances under which that criterion is applied.

Presentation supplies candidate presentations from which successful one-whole and same-unit judgments may be made.

presents relates a presentation to a referent-carrier element. No totality, functionality, injectivity, surjectivity, or identity consequence is assumed for this relation.

• Context : Type u

  The circumstances in which the individuation account is evaluated.

• Presentation : Type u

  Candidate presentations to which the individuation account may apply.

• presents : self.Context → self.Presentation → Referent → Prop

  Whether a candidate presentation presents a particular carrier element under the selected context.

  This relation does not identify presentation equality, carrier equality, or same-unit identity.

• admissiblePresentation : self.Context → self.Presentation → Prop

  Whether a candidate presentation is admissible as a whole-directed presentation under the selected context.

  Admissibility does not itself establish that the presentation succeeds in presenting one whole.

• one : self.Context → self.Presentation → Prop

  Whether a candidate presentation succeeds as a singular presentation of one whole under the selected context.

  This is the monadic unity judgment.

• sameUnit : self.Context → self.Presentation → self.Presentation → Prop

  Whether two candidate presentations count as presentations of the same individuated unit under the selected context.

  This is the dyadic identity judgment. No global equivalence-relation laws are imposed by this interface.

structure SE.Substrate.IndividuationRegime (R : Referent.ReferentCarriers) : Type (u + 1)

The individuation accounts for the three referent kinds distinguished by Structural Explainability.

Each referent kind has its own individuation account. No relationship among the three accounts is assumed.

• entity : IndividuationAccount R.Entity

  Individuation account for entities.

• occurrence : IndividuationAccount R.Occurrence

  Individuation account for occurrences.

• institutionalArtifact : IndividuationAccount R.InstitutionalArtifact

  Individuation account for institutional artifacts.