HasGender — the gender-bearing capability

[Cor91]

The typeclass mixin for carriers that bear grammatical gender — the gender axis of the capability tower over lexical carriers, the analogue of HasNumber (Features/Number/Capabilities.lean) and HasPerson (Features/Person/Capabilities.lean). A consumer (agreement checker, resolution, semantics) requires [HasGender α] and works over any representation: a UD feature bundle, a Word, a Pronoun.

The accessor is label-valued (Option Gender, the comparative-concept vocabulary), because the mixin is the cross-linguistic interface: language-particular fine-grained access goes through the language's Gender.System carrier, not through this class. It is Option-valued because underspecification is the typologically normal case: a carrier with no gender marking is a wildcard for agreement, and most languages have no gender at all ([Cor91]).

Instances live with their carriers (mathlib-style): UD.MorphFeatures here (its type is upstream of this file); downstream carriers (Word, Pronoun) declare theirs where they are defined.

class HasGender (α : Type u_1) : Type u_1

A carrier that bears grammatical gender. none = unmarked or underspecified (a wildcard for agreement, not a default value).

• genderOf : α → Option Gender

  The comparative gender label the carrier bears.

@[implicit_reducible]

instance instHasGenderMorphFeatures : HasGender UD.MorphFeatures

A UD morphology 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 }

@[reducible, inline]

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

Gender compatibility between two (possibly heterogeneous) carriers: the slot values are compatible in the flat information order (Compat) — valued genders must coincide; an unvalued carrier is a wildcard. The gender axis of φ-agreement (UD.MorphFeatures.compatible).

Equations

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

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

φ-compatibility entails gender compatibility: the HasGender mixin never diverges from the unification-based agreement engine (UD.MorphFeatures.compatible).