Typology.Gender

@cite{corbett-1991} @cite{corbett-2013} @cite{dryer-haspelmath-2013} @cite{dixon-1972} @cite{wals-2013}

Per-language typological substrate for gender / noun class systems. Covers three WALS chapters by @cite{corbett-2013}:

• Ch 30: number of genders (none, 2, 3, 4, 5+).
• Ch 31: sex-based vs non-sex-based.
• Ch 32: systems of gender assignment (semantic only, semantic + formal).

Mirrors the Linglib/Typology/{Possession,Negation,Comparison,Coordination,Modality} substrate-extension pattern. Fragment-importable.

What lives here

• GenderCount (5-way), GenderBasis (3-way), AssignmentSystem (3-way), SemanticBasis (5-way) enums.
• GenderProfile per-language struct.
• WALS converters: fromWALS30A, fromWALS31A, fromWALS32A.
• Corpus-only generalisations from WALS Ch 30/31/32.
• Helper predicates (rawCountConsistent, crossChapterConsistent, isNounClassSystem, hasAgreement, lowestAgreementTarget, isCanonicalGender, hasTarget).

Theory-laden caveats

• GenderCount.fivePlus is a single bin for systems with 5+ noun classes. The boundary between "gender" (2-3) and "noun class" (4+) is conventional, not categorical (@cite{corbett-1991}). Bantu languages with ~15 classes and Fula with ~20 are both .fivePlus.
• SemanticBasis lists 5 dimensions (sex, animacy, humanness, shape, rationality); other classifications (e.g. Aikhenvald 2003 noun-classifier semantics) cut differently.

Out of scope

The 21-language sample and Corbett's typological generalisations live in Phenomena/Gender/Studies/Corbett1991.lean. @cite{kramer-2020}'s feature-tier analysis lives in Phenomena/Gender/Studies/Kramer2020.lean.

inductive Typology.Gender.GenderCount : Type

Number of gender / noun class distinctions in a language (WALS Ch 30).

• none : GenderCount
• two : GenderCount
• three : GenderCount
• four : GenderCount
• fivePlus : GenderCount

@[implicit_reducible]

instance Typology.Gender.instDecidableEqGenderCount : DecidableEq GenderCount

Equations

• Typology.Gender.instDecidableEqGenderCount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Gender.instBEqGenderCount : BEq GenderCount

Equations

• Typology.Gender.instBEqGenderCount = { beq := Typology.Gender.instBEqGenderCount.beq }

def Typology.Gender.instBEqGenderCount.beq : GenderCount → GenderCount → Bool

Equations

• Typology.Gender.instBEqGenderCount.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Typology.Gender.instReprGenderCount.repr : GenderCount → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Typology.Gender.instReprGenderCount : Repr GenderCount

Equations

• Typology.Gender.instReprGenderCount = { reprPrec := Typology.Gender.instReprGenderCount.repr }

@[implicit_reducible]

instance Typology.Gender.instInhabitedGenderCount : Inhabited GenderCount

Equations

• Typology.Gender.instInhabitedGenderCount = { default := Typology.Gender.GenderCount.none }

def Typology.Gender.GenderCount.lowerBound : GenderCount → ℕ

Numeric lower bound for each GenderCount category.

Equations

• Typology.Gender.GenderCount.none.lowerBound = 0
• Typology.Gender.GenderCount.two.lowerBound = 2
• Typology.Gender.GenderCount.three.lowerBound = 3
• Typology.Gender.GenderCount.four.lowerBound = 4
• Typology.Gender.GenderCount.fivePlus.lowerBound = 5

def Typology.Gender.GenderCount.Contains (gc : GenderCount) (n : ℕ) : Prop

Whether a raw gender count falls in a given GenderCount category.

Equations

• Typology.Gender.GenderCount.none.Contains n = (n = 0)
• Typology.Gender.GenderCount.two.Contains n = (n = 2)
• Typology.Gender.GenderCount.three.Contains n = (n = 3)
• Typology.Gender.GenderCount.four.Contains n = (n = 4)
• Typology.Gender.GenderCount.fivePlus.Contains n = (n ≥ 5)

@[implicit_reducible]

instance Typology.Gender.instDecidableContains (gc : GenderCount) (n : ℕ) : Decidable (gc.Contains n)

Equations

• One or more equations did not get rendered due to their size.

inductive Typology.Gender.GenderBasis : Type

Whether a gender system is based on biological sex (WALS Ch 31).

• noGender : GenderBasis
• sexBased : GenderBasis
• nonSexBased : GenderBasis

@[implicit_reducible]

instance Typology.Gender.instDecidableEqGenderBasis : DecidableEq GenderBasis

Equations

• Typology.Gender.instDecidableEqGenderBasis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Gender.instBEqGenderBasis : BEq GenderBasis

Equations

• Typology.Gender.instBEqGenderBasis = { beq := Typology.Gender.instBEqGenderBasis.beq }

def Typology.Gender.instBEqGenderBasis.beq : GenderBasis → GenderBasis → Bool

Equations

• Typology.Gender.instBEqGenderBasis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Typology.Gender.instReprGenderBasis.repr : GenderBasis → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Typology.Gender.instReprGenderBasis : Repr GenderBasis

Equations

• Typology.Gender.instReprGenderBasis = { reprPrec := Typology.Gender.instReprGenderBasis.repr }

@[implicit_reducible]

instance Typology.Gender.instInhabitedGenderBasis : Inhabited GenderBasis

Equations

• Typology.Gender.instInhabitedGenderBasis = { default := Typology.Gender.GenderBasis.noGender }

inductive Typology.Gender.AssignmentSystem : Type

How nouns are assigned to their gender categories (WALS Ch 32).

• noGender : AssignmentSystem
• semanticOnly : AssignmentSystem
• semanticAndFormal : AssignmentSystem

@[implicit_reducible]

instance Typology.Gender.instDecidableEqAssignmentSystem : DecidableEq AssignmentSystem

Equations

• Typology.Gender.instDecidableEqAssignmentSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Gender.instBEqAssignmentSystem.beq : AssignmentSystem → AssignmentSystem → Bool

Equations

• Typology.Gender.instBEqAssignmentSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Gender.instBEqAssignmentSystem : BEq AssignmentSystem

Equations

• Typology.Gender.instBEqAssignmentSystem = { beq := Typology.Gender.instBEqAssignmentSystem.beq }

@[implicit_reducible]

instance Typology.Gender.instReprAssignmentSystem : Repr AssignmentSystem

Equations

• Typology.Gender.instReprAssignmentSystem = { reprPrec := Typology.Gender.instReprAssignmentSystem.repr }

def Typology.Gender.instReprAssignmentSystem.repr : AssignmentSystem → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Typology.Gender.instInhabitedAssignmentSystem : Inhabited AssignmentSystem

Equations

• Typology.Gender.instInhabitedAssignmentSystem = { default := Typology.Gender.AssignmentSystem.noGender }

inductive Typology.Gender.SemanticBasis : Type

Semantic dimensions that can underlie gender / noun class assignment.

• sex : SemanticBasis
• animacy : SemanticBasis
• humanness : SemanticBasis
• shape : SemanticBasis
• rationality : SemanticBasis

@[implicit_reducible]

instance Typology.Gender.instDecidableEqSemanticBasis : DecidableEq SemanticBasis

Equations

• Typology.Gender.instDecidableEqSemanticBasis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Gender.instBEqSemanticBasis.beq : SemanticBasis → SemanticBasis → Bool

Equations

• Typology.Gender.instBEqSemanticBasis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Gender.instBEqSemanticBasis : BEq SemanticBasis

Equations

• Typology.Gender.instBEqSemanticBasis = { beq := Typology.Gender.instBEqSemanticBasis.beq }

def Typology.Gender.instReprSemanticBasis.repr : SemanticBasis → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Typology.Gender.instReprSemanticBasis : Repr SemanticBasis

Equations

• Typology.Gender.instReprSemanticBasis = { reprPrec := Typology.Gender.instReprSemanticBasis.repr }

structure Typology.Gender.GenderProfile : Type

A language's gender profile combining WALS Chs 30/31/32 + extra fields (raw count, agreement targets per @cite{corbett-1991}'s Agreement Hierarchy, and semantic-basis dimensions).

• name : String

  Language name.

• iso639 : String

  ISO 639-3 code.

• genderCount : GenderCount

  Ch 30: number of genders (WALS bin).

• rawGenderCount : ℕ

  Actual number of gender / noun class categories.

• basis : GenderBasis

  Ch 31: sex-based or non-sex-based.

• assignment : AssignmentSystem

  Ch 32: assignment system.

• agreementTargets : List Core.AgreementTarget

  Where gender agreement surfaces (@cite{corbett-1991} Agreement Hierarchy: attributive > predicate > relative > pronoun > verb).

• semanticBases : List SemanticBasis

  Semantic dimensions organising the system.

• attestedSurfaceGenders : List Features.SurfaceGender

  Bridge to the lexical-layer Features.SurfaceGender taxonomy: the surface gender values attested in this language. Defaults to [] for noun-class systems (Bantu, Mixtec, Dyirbal) whose per-class agreement doesn't map onto the Indo-European masculine/feminine/neuter/common scheme; per-Fragment files for those languages retain a fine-grained Gender type and provide their own Features.SurfaceGender bridge via a .primary function.

def Typology.Gender.instReprGenderProfile.repr : GenderProfile → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Typology.Gender.instReprGenderProfile : Repr GenderProfile

Equations

• Typology.Gender.instReprGenderProfile = { reprPrec := Typology.Gender.instReprGenderProfile.repr }

def Typology.Gender.instDecidableEqGenderProfile.decEq (x✝ x✝¹ : GenderProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Typology.Gender.instDecidableEqGenderProfile : DecidableEq GenderProfile

Equations

• Typology.Gender.instDecidableEqGenderProfile = Typology.Gender.instDecidableEqGenderProfile.decEq

Mathlib-style Prop-typed predicates with Decidable instances and @[simp] _iff lemmas. Filter sites that need Bool should call decide at the boundary.

def Typology.Gender.GenderProfile.IsRawCountConsistent (p : GenderProfile) : Prop

Equations

• p.IsRawCountConsistent = p.genderCount.Contains p.rawGenderCount

@[simp]

theorem Typology.Gender.GenderProfile.isRawCountConsistent_iff (p : GenderProfile) : p.IsRawCountConsistent ↔ p.genderCount.Contains p.rawGenderCount

@[implicit_reducible]

instance Typology.Gender.GenderProfile.instDecidablePredIsRawCountConsistent : DecidablePred IsRawCountConsistent

Equations

• p.instDecidablePredIsRawCountConsistent = decidable_of_iff (p.genderCount.Contains p.rawGenderCount) ⋯

def Typology.Gender.GenderProfile.IsCrossChapterConsistent (p : GenderProfile) : Prop

Internal consistency across WALS chapters: no-gender in Ch 30 aligns with noGender in Ch 31, Ch 32, and an empty agreement-target list.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Typology.Gender.GenderProfile.isCrossChapterConsistent_iff (p : GenderProfile) : p.IsCrossChapterConsistent ↔ if p.genderCount = GenderCount.none then p.basis = GenderBasis.noGender ∧ p.assignment = AssignmentSystem.noGender ∧ p.agreementTargets = [] else p.basis ≠ GenderBasis.noGender ∧ p.assignment ≠ AssignmentSystem.noGender

@[implicit_reducible]

instance Typology.Gender.GenderProfile.instDecidablePredIsCrossChapterConsistent : DecidablePred IsCrossChapterConsistent

Equations

• p.instDecidablePredIsCrossChapterConsistent = inferInstance

def Typology.Gender.GenderProfile.IsNounClassSystem (p : GenderProfile) : Prop

"Noun class" system: 5+ categories per @cite{corbett-1991}.

Equations

• p.IsNounClassSystem = (p.rawGenderCount ≥ 5)

@[simp]

theorem Typology.Gender.GenderProfile.isNounClassSystem_iff (p : GenderProfile) : p.IsNounClassSystem ↔ p.rawGenderCount ≥ 5

@[implicit_reducible]

instance Typology.Gender.GenderProfile.instDecidablePredIsNounClassSystem : DecidablePred IsNounClassSystem

Equations

• p.instDecidablePredIsNounClassSystem = decidable_of_iff (p.rawGenderCount ≥ 5) ⋯

def Typology.Gender.GenderProfile.HasAgreement (p : GenderProfile) : Prop

Whether the language has any gender agreement.

Equations

• p.HasAgreement = (p.agreementTargets ≠ [])

@[simp]

theorem Typology.Gender.GenderProfile.hasAgreement_iff (p : GenderProfile) : p.HasAgreement ↔ p.agreementTargets ≠ []

@[implicit_reducible]

instance Typology.Gender.GenderProfile.instDecidablePredHasAgreement : DecidablePred HasAgreement

Equations

• p.instDecidablePredHasAgreement = decidable_of_iff (p.agreementTargets ≠ []) ⋯

def Typology.Gender.GenderProfile.IsCanonicalGender (p : GenderProfile) : Prop

"Canonical" gender system in @cite{corbett-1991}'s sense: sex-based, 2 or 3 genders, semantic + formal assignment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Typology.Gender.GenderProfile.isCanonicalGender_iff (p : GenderProfile) : p.IsCanonicalGender ↔ (p.genderCount = GenderCount.two ∨ p.genderCount = GenderCount.three) ∧ p.basis = GenderBasis.sexBased ∧ p.assignment = AssignmentSystem.semanticAndFormal

@[implicit_reducible]

instance Typology.Gender.GenderProfile.instDecidablePredIsCanonicalGender : DecidablePred IsCanonicalGender

Equations

• p.instDecidablePredIsCanonicalGender = inferInstance

def Typology.Gender.GenderProfile.lowestAgreementTarget (p : GenderProfile) : Option Core.AgreementTarget

Lowest agreement target in @cite{corbett-1991}'s hierarchy.

Equations

• One or more equations did not get rendered due to their size.

def Typology.Gender.fromWALS30A : Data.WALS.F30A.GenderCount → GenderCount

WALS Ch 30A → GenderCount.

Equations

• Typology.Gender.fromWALS30A Data.WALS.F30A.GenderCount.none = Typology.Gender.GenderCount.none
• Typology.Gender.fromWALS30A Data.WALS.F30A.GenderCount.two = Typology.Gender.GenderCount.two
• Typology.Gender.fromWALS30A Data.WALS.F30A.GenderCount.three = Typology.Gender.GenderCount.three
• Typology.Gender.fromWALS30A Data.WALS.F30A.GenderCount.four = Typology.Gender.GenderCount.four
• Typology.Gender.fromWALS30A Data.WALS.F30A.GenderCount.fiveOrMore = Typology.Gender.GenderCount.fivePlus

def Typology.Gender.fromWALS31A : Data.WALS.F31A.GenderBasis → GenderBasis

WALS Ch 31A → GenderBasis.

Equations

• Typology.Gender.fromWALS31A Data.WALS.F31A.GenderBasis.noGender = Typology.Gender.GenderBasis.noGender
• Typology.Gender.fromWALS31A Data.WALS.F31A.GenderBasis.sexBased = Typology.Gender.GenderBasis.sexBased
• Typology.Gender.fromWALS31A Data.WALS.F31A.GenderBasis.nonSexBased = Typology.Gender.GenderBasis.nonSexBased

def Typology.Gender.fromWALS32A : Data.WALS.F32A.SystemsOfGenderAssignment → AssignmentSystem

WALS Ch 32A → AssignmentSystem.

Equations

• Typology.Gender.fromWALS32A Data.WALS.F32A.SystemsOfGenderAssignment.noGender = Typology.Gender.AssignmentSystem.noGender
• Typology.Gender.fromWALS32A Data.WALS.F32A.SystemsOfGenderAssignment.semantic = Typology.Gender.AssignmentSystem.semanticOnly
• Typology.Gender.fromWALS32A Data.WALS.F32A.SystemsOfGenderAssignment.semanticAndFormal = Typology.Gender.AssignmentSystem.semanticAndFormal

def Typology.Gender.walsGenderCount (iso : String) : Option GenderCount

Equations

• Typology.Gender.walsGenderCount iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F30A.GenderCount) => Typology.Gender.fromWALS30A x.value) (Data.WALS.F30A.lookupISO iso)

def Typology.Gender.walsGenderBasis (iso : String) : Option GenderBasis

Equations

• Typology.Gender.walsGenderBasis iso = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F31A.GenderBasis) => Typology.Gender.fromWALS31A x.value) (Data.WALS.F31A.lookupISO iso)

def Typology.Gender.walsAssignment (iso : String) : Option AssignmentSystem

Equations

• One or more equations did not get rendered due to their size.

def Typology.Gender.GenderProfile.fromWALS (name iso : String) (rawGenderCount : ℕ) (agreementTargets : List Core.AgreementTarget := []) (semanticBases : List SemanticBasis := []) (attestedSurfaceGenders : List Features.SurfaceGender := []) (genderCountFb : GenderCount := GenderCount.none) (basisFb : GenderBasis := GenderBasis.noGender) (assignmentFb : AssignmentSystem := AssignmentSystem.noGender) : GenderProfile

Build a GenderProfile from an ISO 639-3 code via WALS lookups for Chs 30/31/32. The three required-field fallbacks (genderCountFb, basisFb, assignmentFb) fire only when WALS is silent for that ISO. The rawGenderCount, agreementTargets, semanticBases, and attestedSurfaceGenders fields are paper-stipulated per @cite{corbett-1991} — they are not derivable from any WALS chapter and must be passed explicitly.

Equations

• One or more equations did not get rendered due to their size.

Earlier revisions of this file carried five aggregate-count theorems on the full WALS Ch 30/31/32 corpora (ch30_no_gender_modal, ch30_two_most_common, ch31_sex_based_dominant, ch32_mixed_slightly_more, ch32_no_purely_formal). These were the "aggregate-count theorems go stale" anti-pattern AND required native_decide for ~1000-element list reductions; deleted as part of the GenderProfile mathlib polish. The corpus distributions remain documentary in @cite{corbett-2013}'s WALS chapters.