The gender-bearing capability

HasGender equips a carrier with the comparative gender label it bears; HasGender.Compatible is the induced agreement relation, slot compatibility in the flat information order. The label vocabulary is the cross-linguistic interface; language-particular fine-grained access goes through the language's Gender.System. ⊥ is the typologically normal case: most languages have no gender at all ([Cor91]).

class HasGender (α : Type u_1) : Type u_1

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

• genderOf : α → Flat Gender

  The comparative gender label the carrier bears, if marked.

@[instance_reducible]

instance instHasGenderMorphFeatures : HasGender UD.MorphFeatures

A UD bundle bears the label its gender tag ingests (Gender.fromUD, total on UD genders).

Equations

• instHasGenderMorphFeatures = { genderOf := fun (f : UD.MorphFeatures) => Option.map Gender.fromUD f.gender }

@[instance_reducible]

instance instHasGenderGender : HasGender Gender

Equations

• instHasGenderGender = { genderOf := fun (x : Gender) => ↑x }

@[reducible, inline]

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

Gender compatibility: valued genders coincide, an unvalued carrier is a wildcard.

Equations

• HasGender.Compatible a b = Compat (genderOf a) (genderOf b)

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

φ-compatibility of UD bundles entails gender compatibility.