The person-bearing capability

HasPerson equips a carrier with the grammatical person it bears; HasPerson.Compatible is the induced agreement relation, slot compatibility in the flat information order. Carriers storing UD realization lift through Person.fromUD; carriers storing a (UD person, clusivity) pair recover the quadripartition cell ([Cys09]) in Syntax/Category/Pronoun/Capabilities.lean.

class HasPerson (α : Type u_1) : Type u_1

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

• personOf : α → Flat Person

  The person value the carrier bears, if marked.

@[instance_reducible]

instance instHasPersonMorphFeatures : HasPerson UD.MorphFeatures

Equations

• instHasPersonMorphFeatures = { personOf := fun (mf : UD.MorphFeatures) => Option.map Person.fromUD mf.person }

@[instance_reducible]

instance instHasPersonPerson : HasPerson Person

Equations

• instHasPersonPerson = { personOf := fun (x : Person) => ↑x }

@[reducible, inline]

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

Person compatibility: valued persons coincide, an unvalued carrier is a wildcard.

Equations

• HasPerson.Compatible a b = Compat (personOf a) (personOf b)

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

φ-compatibility of UD bundles entails person compatibility.