The scale of individuation

[Gri18] [SF21]

Individuation types: equivalence classes of nominal descriptions by individuation properties, linearly ordered from entities with no perceptible minimal units to fully independent individuals ([Gri18] (17)/(19)). Graduated from Studies/Grimm2018.lean on gaining its second consumer: [Gri18] partitions the scale into grammatical countability classes by order-preserving maps; [SF21] organizes count/mass lexicalization options by the same notional classes (granulars are the pivotal type: count as English lentil, mass as English rice or Czech čočka). The mereotopological content of the middle types (units clumped together vs. connected but separable) is self-connection in the sense of [CV99].

inductive IndividuationType : Type

Individuation types ([Gri18] (17)/(19)): the scale substance < granular aggregate < collective aggregate < individual.

• substance : IndividuationType

  No perceptible minimal units (liquids, substances: water, mud).

• granularAggregate : IndividuationType

  Perceptible units, typically not separated from one another (rice, sand, lentils).

• collectiveAggregate : IndividuationType

  Perceptible units, separated but spatially or functionally connected (ants, cherries; functional aggregates: furniture).

• individualEntity : IndividuationType

  Independent, free-standing units (dog, chair).

@[implicit_reducible]

instance instDecidableEqIndividuationType : DecidableEq IndividuationType

Equations

• instDecidableEqIndividuationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprIndividuationType : Repr IndividuationType

Equations

• instReprIndividuationType = { reprPrec := instReprIndividuationType.repr }

def instReprIndividuationType.repr : IndividuationType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprIndividuationType.repr IndividuationType.substance prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "IndividuationType.substance")).group prec✝

@[implicit_reducible]

instance instFintypeIndividuationType : Fintype IndividuationType

Equations

• instFintypeIndividuationType = { elems := { val := ↑IndividuationType.enumList, nodup := IndividuationType.enumList_nodup }, complete := instFintypeIndividuationType._proof_1 }

def IndividuationType.toNat : IndividuationType → ℕ

Numeric embedding preserving the individuation order.

Equations

• IndividuationType.substance.toNat = 0
• IndividuationType.granularAggregate.toNat = 1
• IndividuationType.collectiveAggregate.toNat = 2
• IndividuationType.individualEntity.toNat = 3

@[implicit_reducible]

instance IndividuationType.instLinearOrder : LinearOrder IndividuationType

Equations

• IndividuationType.instLinearOrder = LinearOrder.lift' IndividuationType.toNat IndividuationType.instLinearOrder._proof_1