The φ-bundle capability

HasPhi equips a carrier with its agreement φ-features (person, number, gender) as a UD bundle; HasPhi.Agree is the induced agreement relation. The per-axis analytical capabilities are HasPerson/HasNumber/HasGender; HasPhi is their UD-realization face, the bundle φ-agreement (UD.MorphFeatures.compatible) consumes.

class HasPhi (α : Type u_1) : Type u_1

A φ-bearer is an expression that exposes person, number, and gender for agreement, as a UD feature bundle.

• phi : α → UD.MorphFeatures

  The agreement φ-features (person/number/gender).

@[instance_reducible]

instance instHasPhiMorphFeatures : HasPhi UD.MorphFeatures

A φ-bundle bears itself.

Equations

• instHasPhiMorphFeatures = { phi := id }

def HasPhi.Agree {α : Type u_1} {β : Type u_2} [HasPhi α] [HasPhi β] (a : α) (b : β) : Prop

Two φ-bearers agree when their features unify (UD.MorphFeatures.compatible), an unspecified feature acting as a wildcard.

Equations

• HasPhi.Agree a b = ((phi a).compatible (phi b) = true)

@[instance_reducible]

instance instDecidableAgree {α : Type u_1} {β : Type u_2} [HasPhi α] [HasPhi β] (a : α) (b : β) : Decidable (HasPhi.Agree a b)

Equations

• instDecidableAgree a b = id inferInstance