The number-bearing capability

HasNumber equips a carrier with the grammatical number it bears; HasNumber.Compatible is the induced agreement relation, slot compatibility in the flat information order. Underspecification is the typologically normal case ([Cor00]): an unmarked carrier (none) is a wildcard, not a default singular.

class HasNumber (α : Type u_1) : Type u_1

A carrier of grammatical number. ⊥ = the carrier does not mark number.

• numberOf : α → Flat Number

  The number value the carrier bears, if marked.

@[instance_reducible]

instance instHasNumberMorphFeatures : HasNumber UD.MorphFeatures

A UD bundle bears the number its number tag ingests (Number.fromUD); Inv/Coll/Count have no analytical value and leave it unmarked.

Equations

• instHasNumberMorphFeatures = { numberOf := fun (f : UD.MorphFeatures) => Option.bind f.number Number.fromUD }

@[instance_reducible]

instance instHasNumberNumber : HasNumber Number

Equations

• instHasNumberNumber = { numberOf := fun (x : Number) => ↑x }

@[reducible, inline]

abbrev HasNumber.Compatible {α : Type u_1} {β : Type u_2} [HasNumber α] [HasNumber β] (a : α) (b : β) : Prop

Number compatibility: valued numbers coincide, an unvalued carrier is a wildcard.

Equations

• HasNumber.Compatible a b = Compat (numberOf a) (numberOf b)

theorem UD.MorphFeatures.compatible_hasNumber {f1 f2 : MorphFeatures} (h : f1.compatible f2 = true) : HasNumber.Compatible f1 f2

φ-compatibility of UD bundles entails number compatibility.