Gender and Noun Class Typology (WALS Chapters 30--32)

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

Formalizes three chapters from the World Atlas of Language Structures (WALS) covering the typology of gender and noun class systems, all authored by @cite{corbett-2013}:

• Chapter 30: Number of Genders -- how many gender/noun class distinctions a language makes. Values range from none (no gender system) through 2, 3, 4, to 5 or more. Most of the world's languages have no gender system at all; among those that do, 2 and 3 genders are most common. Systems with 5 or more categories are typically called "noun class" systems rather than "gender" systems (the Bantu languages being the canonical example).

• Chapter 31: Sex-based and Non-sex-based Gender Systems -- whether the gender system is organized around biological sex (masculine/feminine, with or without neuter) or around other semantic/formal criteria such as animacy, shape, or size. The distinction cross-cuts the number of genders: a 2-gender system may be masculine/feminine (French) or animate/inanimate (Ojibwe).

• Chapter 32: Systems of Gender Assignment -- how nouns are assigned to their gender categories. Assignment may be purely semantic (based on the meaning of the noun, e.g. male referents are masculine), purely formal (based on phonological or morphological properties), or a combination. A key typological finding is that no language has a purely formal assignment system: formal rules always supplement a semantic core.

Key Concepts

The boundary between "gender" (2--3 categories, typically sex-based) and "noun class" (4+ categories, often with semantic and formal assignment) is gradient rather than categorical. @cite{corbett-1991} treats them as a single phenomenon at different scales.

Corbett's Agreement Hierarchy governs where gender agreement surfaces: attributive adjective > predicate adjective > relative pronoun > personal pronoun > verb target. If a language shows gender agreement on a lower target, it shows agreement on all higher targets.

inductive Phenomena.Gender.Typology.GenderCount : Type

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

The five values form a scale from no gender system at all through increasingly fine-grained classification. Systems with 5 or more categories are often called "noun class" systems rather than "gender" systems, but the boundary is conventional, not categorical.

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

instance Phenomena.Gender.Typology.instDecidableEqGenderCount : DecidableEq GenderCount

Equations

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

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

Equations

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

instance Phenomena.Gender.Typology.instBEqGenderCount : BEq GenderCount

Equations

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

def Phenomena.Gender.Typology.instReprGenderCount.repr : GenderCount → Nat → Std.Format

Equations

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

instance Phenomena.Gender.Typology.instReprGenderCount : Repr GenderCount

Equations

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

instance Phenomena.Gender.Typology.instInhabitedGenderCount : Inhabited GenderCount

Equations

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

def Phenomena.Gender.Typology.GenderCount.lowerBound : GenderCount → Nat

Numeric lower bound for each GenderCount category.

Equations

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

def Phenomena.Gender.Typology.GenderCount.contains (gc : GenderCount) (n : Nat) : Bool

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

Equations

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

theorem Phenomena.Gender.Typology.ch30_total : Phenomena.Gender.Typology.ch30✝.length = 257

Chapter 30 total sample size (from generated data).

inductive Phenomena.Gender.Typology.GenderBasis : Type

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

Sex-based systems organize genders around a masculine/feminine distinction (possibly with additional genders like neuter). Non-sex-based systems use other semantic criteria: animate/inanimate, human/non-human, shape-based, etc. Many Bantu noun class systems are non-sex-based, organized instead around semantic categories like human, plant, artifact, abstract, liquid, etc.

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

instance Phenomena.Gender.Typology.instDecidableEqGenderBasis : DecidableEq GenderBasis

Equations

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

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

Equations

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

instance Phenomena.Gender.Typology.instBEqGenderBasis : BEq GenderBasis

Equations

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

def Phenomena.Gender.Typology.instReprGenderBasis.repr : GenderBasis → Nat → Std.Format

Equations

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

instance Phenomena.Gender.Typology.instReprGenderBasis : Repr GenderBasis

Equations

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

instance Phenomena.Gender.Typology.instInhabitedGenderBasis : Inhabited GenderBasis

Equations

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

theorem Phenomena.Gender.Typology.ch31_total : Phenomena.Gender.Typology.ch31✝.length = 257

Chapter 31 total sample size (from generated data).

inductive Phenomena.Gender.Typology.AssignmentSystem : Type

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

Semantic assignment means gender is determined by meaning: male referents are masculine, female referents are feminine, etc. Formal assignment means gender is determined by the phonological or morphological shape of the noun: e.g., in Italian, nouns ending in -o tend to be masculine, nouns ending in -a tend to be feminine.

A key typological finding is that no language has a purely formal assignment system: formal rules always supplement a semantic core. Languages either use semantic assignment alone or combine semantic and formal criteria.

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

instance Phenomena.Gender.Typology.instDecidableEqAssignmentSystem : DecidableEq AssignmentSystem

Equations

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

instance Phenomena.Gender.Typology.instBEqAssignmentSystem : BEq AssignmentSystem

Equations

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

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

Equations

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

def Phenomena.Gender.Typology.instReprAssignmentSystem.repr : AssignmentSystem → Nat → Std.Format

Equations

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

instance Phenomena.Gender.Typology.instReprAssignmentSystem : Repr AssignmentSystem

Equations

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

instance Phenomena.Gender.Typology.instInhabitedAssignmentSystem : Inhabited AssignmentSystem

Equations

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

theorem Phenomena.Gender.Typology.ch32_total : Phenomena.Gender.Typology.ch32✝.length = 257

Chapter 32 total sample size.

theorem Phenomena.Gender.Typology.ch30_no_gender_modal : have noGender := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.none) Phenomena.Gender.Typology.ch30✝).length; noGender > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.two) Phenomena.Gender.Typology.ch30✝¹).length ∧ noGender > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.three) Phenomena.Gender.Typology.ch30✝²).length ∧ noGender > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.four) Phenomena.Gender.Typology.ch30✝³).length ∧ noGender > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.fiveOrMore) Phenomena.Gender.Typology.ch30✝⁴).length

Ch 30: Languages with no gender are the modal category.

theorem Phenomena.Gender.Typology.ch30_two_most_common : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.two) Phenomena.Gender.Typology.ch30✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.three) Phenomena.Gender.Typology.ch30✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.two) Phenomena.Gender.Typology.ch30✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.four) Phenomena.Gender.Typology.ch30✝³).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.two) Phenomena.Gender.Typology.ch30✝⁴).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => x.value == Core.WALS.F30A.GenderCount.fiveOrMore) Phenomena.Gender.Typology.ch30✝⁵).length

Ch 30: Among gender-bearing languages, 2-gender systems are most common.

theorem Phenomena.Gender.Typology.ch31_sex_based_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => x.value == Core.WALS.F31A.GenderBasis.sexBased) Phenomena.Gender.Typology.ch31✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => x.value == Core.WALS.F31A.GenderBasis.nonSexBased) Phenomena.Gender.Typology.ch31✝¹).length

Ch 31: Sex-based systems far outnumber non-sex-based ones.

theorem Phenomena.Gender.Typology.ch32_mixed_slightly_more : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => x.value == Core.WALS.F32A.SystemsOfGenderAssignment.semanticAndFormal) Phenomena.Gender.Typology.ch32✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => x.value == Core.WALS.F32A.SystemsOfGenderAssignment.semantic) Phenomena.Gender.Typology.ch32✝¹).length

Ch 32: Semantic-and-formal assignment slightly outnumbers semantic-only.

theorem Phenomena.Gender.Typology.ch32_no_purely_formal : (Phenomena.Gender.Typology.ch32✝.all fun (d : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => d.value == Core.WALS.F32A.SystemsOfGenderAssignment.noGender || d.value == Core.WALS.F32A.SystemsOfGenderAssignment.semantic || d.value == Core.WALS.F32A.SystemsOfGenderAssignment.semanticAndFormal) = true

Ch 32: No purely formal assignment system is attested. This is Corbett's key generalization: formal assignment always supplements a semantic core, never replaces it. WALS F32A has only three categories: noGender, semantic, and semanticAndFormal — no "formal only" category exists.

inductive Phenomena.Gender.Typology.SemanticBasis : Type

Semantic dimensions that can underlie gender/noun class assignment.

Different languages organize their noun classification around different semantic properties. Sex is the most common, but animacy, humanness, and shape/size are also attested as organizing principles.

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

instance Phenomena.Gender.Typology.instDecidableEqSemanticBasis : DecidableEq SemanticBasis

Equations

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

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

Equations

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

instance Phenomena.Gender.Typology.instBEqSemanticBasis : BEq SemanticBasis

Equations

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

instance Phenomena.Gender.Typology.instReprSemanticBasis : Repr SemanticBasis

Equations

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

def Phenomena.Gender.Typology.instReprSemanticBasis.repr : SemanticBasis → Nat → Std.Format

Equations

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

structure Phenomena.Gender.Typology.GenderProfile : Type

A language's gender profile combining classifications from WALS Chapters 30, 31, and 32, plus additional typological information.

The rawGenderCount field stores the actual number of gender/noun class categories (not just the WALS bin), enabling finer-grained comparisons. The agreementTargets list records where gender agreement surfaces. The semanticBases list records the semantic dimensions organizing the system.

• name : String

  Language name

• iso639 : String

  ISO 639-3 code

• genderCount : GenderCount

  Ch 30: Number of genders (WALS category)

• rawGenderCount : Nat

  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 AgreementTarget

  Where gender agreement surfaces

• semanticBases : List SemanticBasis

  Semantic dimensions organizing the system

instance Phenomena.Gender.Typology.instReprGenderProfile : Repr GenderProfile

Equations

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

def Phenomena.Gender.Typology.instReprGenderProfile.repr : GenderProfile → Nat → Std.Format

Equations

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

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

Equations

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

instance Phenomena.Gender.Typology.instDecidableEqGenderProfile : DecidableEq GenderProfile

Equations

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

instance Phenomena.Gender.Typology.instBEqGenderProfile : BEq GenderProfile

Equations

• Phenomena.Gender.Typology.instBEqGenderProfile = { beq := Phenomena.Gender.Typology.instBEqGenderProfile.beq }

def Phenomena.Gender.Typology.instBEqGenderProfile.beq : GenderProfile → GenderProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Gender.Typology.instBEqGenderProfile.beq x✝¹ x✝ = false

def Phenomena.Gender.Typology.GenderProfile.rawCountConsistent (p : GenderProfile) : Bool

Whether the raw gender count is consistent with the WALS bin.

Equations

• p.rawCountConsistent = p.genderCount.contains p.rawGenderCount

def Phenomena.Gender.Typology.GenderProfile.crossChapterConsistent (p : GenderProfile) : Bool

Whether the profile is internally consistent across chapters: no-gender in Ch 30 should align with noGender in Ch 31 and Ch 32.

Equations

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

def Phenomena.Gender.Typology.GenderProfile.isNounClassSystem (p : GenderProfile) : Bool

Whether the language qualifies as a "noun class" system (5+ categories).

Equations

• p.isNounClassSystem = decide (p.rawGenderCount ≥ 5)

def Phenomena.Gender.Typology.GenderProfile.hasAgreement (p : GenderProfile) : Bool

Whether the language has any gender agreement.

Equations

• p.hasAgreement = decide (p.agreementTargets.length > 0)

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

Lowest agreement target (most marked in Corbett's hierarchy).

Equations

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

def Phenomena.Gender.Typology.english : GenderProfile

English: no grammatical gender on nouns or adjectives; only natural gender in 3sg pronouns (he/she/it). No gender agreement on adjectives or verbs.

Equations

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

def Phenomena.Gender.Typology.mandarin : GenderProfile

Mandarin Chinese: no gender system whatsoever. No morphological gender marking on nouns, adjectives, or verbs. Third-person pronouns were historically undifferentiated; the written distinction ta1/ta1 is a 20th-century orthographic innovation.

Equations

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

def Phenomena.Gender.Typology.japanese : GenderProfile

Japanese: no gender system. Classifier system organizes nouns but does not trigger agreement. No gender marking on adjectives, verbs, or pronouns.

Equations

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

def Phenomena.Gender.Typology.turkish : GenderProfile

Turkish: no gender system. No morphological gender distinctions on nouns, adjectives, verbs, or pronouns. The third-person pronoun o is used for all referents regardless of sex or animacy.

Equations

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

def Phenomena.Gender.Typology.finnish : GenderProfile

Finnish: no gender system. No grammatical gender on nouns, adjectives, or verbs. The third-person pronoun han is used for all referents.

Equations

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

def Phenomena.Gender.Typology.korean : GenderProfile

Korean: no gender system. No morphological gender marking. Third-person reference uses demonstratives rather than gendered pronouns.

Equations

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

def Phenomena.Gender.Typology.quechua : GenderProfile

Quechua (Cusco): no gender system. Agglutinative morphology with rich case and number but no gender distinctions.

Equations

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

def Phenomena.Gender.Typology.french : GenderProfile

French: 2 genders (masculine/feminine). Sex-based with considerable formal reinforcement (nouns ending in -tion, -ence tend feminine; -ment, -age tend masculine). Agreement on determiners, adjectives (attributive and predicate), past participles. Assignment is semantic + formal.

Equations

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

def Phenomena.Gender.Typology.spanish : GenderProfile

Spanish: 2 genders (masculine/feminine). Sex-based with strong formal correlates (-o masculine, -a feminine, with many exceptions). Agreement on determiners, adjectives, past participles, and some verb forms.

Equations

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

def Phenomena.Gender.Typology.hindiUrdu : GenderProfile

Hindi-Urdu: 2 genders (masculine/feminine). Sex-based with strong formal assignment (nouns ending in -aa tend masculine, -ii feminine). Agreement on adjectives, verbs (in perfective aspect), and auxiliaries. One of the clearest cases of verb agreement for gender.

Equations

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

def Phenomena.Gender.Typology.irish : GenderProfile

Irish: 2 genders (masculine/feminine). Sex-based with formal assignment playing a role (initial consonant mutations triggered by gender). Agreement on determiners, attributive adjectives, and pronouns.

Equations

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

def Phenomena.Gender.Typology.hebrew : GenderProfile

Hebrew (Modern): 2 genders (masculine/feminine). Sex-based with formal correlates (-a, -et endings often feminine). Agreement on adjectives, verbs (all tenses), demonstratives, and numerals.

Equations

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

def Phenomena.Gender.Typology.german : GenderProfile

German: 3 genders (masculine/feminine/neuter). Sex-based with extensive formal assignment (suffixes like -ung, -heit, -keit are feminine; -chen, -lein diminutives are neuter; Ge- collectives are neuter). Agreement on determiners, adjectives (attributive and predicate), relative pronouns, and personal pronouns.

Equations

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

def Phenomena.Gender.Typology.russian : GenderProfile

Russian: 3 genders (masculine/feminine/neuter). Sex-based with strong formal correlates (consonant-final stems tend masculine, -a final feminine, -o or -e final neuter). Agreement on adjectives, verbs (past tense), demonstratives, relative pronouns, and personal pronouns.

Equations

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

def Phenomena.Gender.Typology.latin : GenderProfile

Latin: 3 genders (masculine/feminine/neuter). Sex-based with formal assignment via declension classes (-us, -er 2nd decl. mostly masculine, -a 1st decl. mostly feminine, -um 2nd decl. neuter). Agreement on adjectives and relative/demonstrative pronouns.

Equations

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

def Phenomena.Gender.Typology.romanian : GenderProfile

Romanian: 3 genders (masculine/feminine/neuter -- the neuter behaves as masculine in the singular and feminine in the plural, sometimes analyzed as "ambigeneric"). Sex-based with formal assignment. Agreement on determiners (enclitic definite article), adjectives, and pronouns.

Equations

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

def Phenomena.Gender.Typology.dyirbal : GenderProfile

Dyirbal (Australia): 4 genders. I: males, most animate beings; II: females, water, fire, fighting; III: edible plants and fruit; IV: residual (everything else). Non-sex-based in the sense that the system includes categories organized around edibility and natural forces, not just biological sex. Semantic assignment only (no formal correlates). Agreement on determiners/classifiers.

Equations

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

def Phenomena.Gender.Typology.georgian : GenderProfile

Georgian: 4 categories in traditional analysis -- rational (humans) vs non-rational, cross-cut by an older masculine/feminine trace in pronouns. More recent analyses posit a simpler animacy-based split. Non-sex-based: the primary division is rational/non-rational. Semantic assignment. Agreement on verbs (verb agreement cross-references subjects and objects, tracking the rational/non-rational distinction).

Equations

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

def Phenomena.Gender.Typology.swahili : GenderProfile

Swahili (Bantu): approximately 15--18 noun classes (paired into 9 singular/plural pairings + locative classes). The system is organized around semantic dimensions (human, plant, artifact, abstract, liquid, augmentative, diminutive) but with extensive formal assignment via prefixes (m-, wa- for Class 1/2 humans; ki-, vi- for Class 7/8 tools; etc.). Agreement permeates: determiners, adjectives, verbs, pronouns, numerals, and possessives all agree in noun class.

Equations

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

def Phenomena.Gender.Typology.zulu : GenderProfile

Zulu (Bantu): approximately 15 noun classes, closely related to the Swahili system (both are Bantu). Organized by similar semantic dimensions with prefix-based formal assignment (umu-, aba- for Class 1/2 humans, etc.). Full agreement across all targets.

Equations

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

def Phenomena.Gender.Typology.fula : GenderProfile

Fula (Atlantic, Niger-Congo): approximately 20+ noun classes, one of the richest class systems in Africa. Classes encode semantic distinctions including human, animal, plant, liquid, diminutive, augmentative, and pejorative. Formal assignment via class suffixes (-o, -Be for Class 1/2 humans; -nde, -de for trees, etc.). Agreement on determiners, adjectives, verbs, pronouns.

Equations

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

def Phenomena.Gender.Typology.allProfiles : List GenderProfile

All language profiles in our sample.

Equations

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

theorem Phenomena.Gender.Typology.allProfiles_count : allProfiles.length = 21

Every language's raw gender count falls within its declared WALS category.

theorem Phenomena.Gender.Typology.english_raw_consistent : english.rawCountConsistent = true

theorem Phenomena.Gender.Typology.mandarin_raw_consistent : mandarin.rawCountConsistent = true

theorem Phenomena.Gender.Typology.japanese_raw_consistent : japanese.rawCountConsistent = true

theorem Phenomena.Gender.Typology.turkish_raw_consistent : turkish.rawCountConsistent = true

theorem Phenomena.Gender.Typology.finnish_raw_consistent : finnish.rawCountConsistent = true

theorem Phenomena.Gender.Typology.korean_raw_consistent : korean.rawCountConsistent = true

theorem Phenomena.Gender.Typology.quechua_raw_consistent : quechua.rawCountConsistent = true

theorem Phenomena.Gender.Typology.french_raw_consistent : french.rawCountConsistent = true

theorem Phenomena.Gender.Typology.spanish_raw_consistent : spanish.rawCountConsistent = true

theorem Phenomena.Gender.Typology.hindiUrdu_raw_consistent : hindiUrdu.rawCountConsistent = true

theorem Phenomena.Gender.Typology.irish_raw_consistent : irish.rawCountConsistent = true

theorem Phenomena.Gender.Typology.hebrew_raw_consistent : hebrew.rawCountConsistent = true

theorem Phenomena.Gender.Typology.german_raw_consistent : german.rawCountConsistent = true

theorem Phenomena.Gender.Typology.russian_raw_consistent : russian.rawCountConsistent = true

theorem Phenomena.Gender.Typology.latin_raw_consistent : latin.rawCountConsistent = true

theorem Phenomena.Gender.Typology.romanian_raw_consistent : romanian.rawCountConsistent = true

theorem Phenomena.Gender.Typology.dyirbal_raw_consistent : dyirbal.rawCountConsistent = true

theorem Phenomena.Gender.Typology.georgian_raw_consistent : georgian.rawCountConsistent = true

theorem Phenomena.Gender.Typology.swahili_raw_consistent : swahili.rawCountConsistent = true

theorem Phenomena.Gender.Typology.zulu_raw_consistent : zulu.rawCountConsistent = true

theorem Phenomena.Gender.Typology.fula_raw_consistent : fula.rawCountConsistent = true

theorem Phenomena.Gender.Typology.all_raw_consistent : (allProfiles.all fun (x : GenderProfile) => x.rawCountConsistent) = true

All raw gender counts are consistent with their WALS bins.

Cross-chapter consistency: no-gender in Ch 30 aligns with noGender in Ch 31 and Ch 32; gender-bearing languages do not have noGender in Ch 31 or Ch 32.

theorem Phenomena.Gender.Typology.english_cross_consistent : english.crossChapterConsistent = true

theorem Phenomena.Gender.Typology.mandarin_cross_consistent : mandarin.crossChapterConsistent = true

theorem Phenomena.Gender.Typology.french_cross_consistent : french.crossChapterConsistent = true

theorem Phenomena.Gender.Typology.german_cross_consistent : german.crossChapterConsistent = true

theorem Phenomena.Gender.Typology.swahili_cross_consistent : swahili.crossChapterConsistent = true

theorem Phenomena.Gender.Typology.all_cross_consistent : (allProfiles.all fun (x : GenderProfile) => x.crossChapterConsistent) = true

All profiles are cross-chapter consistent.

Spot-checks that each language has the expected WALS category values.

theorem Phenomena.Gender.Typology.english_no_gender : english.genderCount = GenderCount.none

theorem Phenomena.Gender.Typology.mandarin_no_gender : mandarin.genderCount = GenderCount.none

theorem Phenomena.Gender.Typology.japanese_no_gender : japanese.genderCount = GenderCount.none

theorem Phenomena.Gender.Typology.turkish_no_gender : turkish.genderCount = GenderCount.none

theorem Phenomena.Gender.Typology.finnish_no_gender : finnish.genderCount = GenderCount.none

theorem Phenomena.Gender.Typology.korean_no_gender : korean.genderCount = GenderCount.none

theorem Phenomena.Gender.Typology.quechua_no_gender : quechua.genderCount = GenderCount.none

theorem Phenomena.Gender.Typology.french_two_genders : french.genderCount = GenderCount.two

theorem Phenomena.Gender.Typology.spanish_two_genders : spanish.genderCount = GenderCount.two

theorem Phenomena.Gender.Typology.hindiUrdu_two_genders : hindiUrdu.genderCount = GenderCount.two

theorem Phenomena.Gender.Typology.irish_two_genders : irish.genderCount = GenderCount.two

theorem Phenomena.Gender.Typology.hebrew_two_genders : hebrew.genderCount = GenderCount.two

theorem Phenomena.Gender.Typology.german_three_genders : german.genderCount = GenderCount.three

theorem Phenomena.Gender.Typology.russian_three_genders : russian.genderCount = GenderCount.three

theorem Phenomena.Gender.Typology.latin_three_genders : latin.genderCount = GenderCount.three

theorem Phenomena.Gender.Typology.romanian_three_genders : romanian.genderCount = GenderCount.three

theorem Phenomena.Gender.Typology.dyirbal_four_genders : dyirbal.genderCount = GenderCount.four

theorem Phenomena.Gender.Typology.georgian_four_genders : georgian.genderCount = GenderCount.four

theorem Phenomena.Gender.Typology.swahili_fivePlus : swahili.genderCount = GenderCount.fivePlus

theorem Phenomena.Gender.Typology.zulu_fivePlus : zulu.genderCount = GenderCount.fivePlus

theorem Phenomena.Gender.Typology.fula_fivePlus : fula.genderCount = GenderCount.fivePlus

theorem Phenomena.Gender.Typology.french_sex_based : french.basis = GenderBasis.sexBased

theorem Phenomena.Gender.Typology.hindiUrdu_sex_based : hindiUrdu.basis = GenderBasis.sexBased

theorem Phenomena.Gender.Typology.russian_sex_based : russian.basis = GenderBasis.sexBased

theorem Phenomena.Gender.Typology.swahili_non_sex_based : swahili.basis = GenderBasis.nonSexBased

theorem Phenomena.Gender.Typology.dyirbal_non_sex_based : dyirbal.basis = GenderBasis.nonSexBased

theorem Phenomena.Gender.Typology.georgian_non_sex_based : georgian.basis = GenderBasis.nonSexBased

theorem Phenomena.Gender.Typology.french_formal_assignment : french.assignment = AssignmentSystem.semanticAndFormal

theorem Phenomena.Gender.Typology.dyirbal_semantic_assignment : dyirbal.assignment = AssignmentSystem.semanticOnly

theorem Phenomena.Gender.Typology.swahili_mixed_assignment : swahili.assignment = AssignmentSystem.semanticAndFormal

Generalization 1: No gender is the most common state.

The majority of the world's languages have no grammatical gender system at all (145 out of 257 in the WALS Ch 30 sample). This is reflected in our sample, where 7 out of 21 languages have no gender.

theorem Phenomena.Gender.Typology.no_gender_most_common_wals : 145 > 50 ∧ 145 > 26 ∧ 145 > 12 ∧ 145 > 24

theorem Phenomena.Gender.Typology.no_gender_in_sample : (List.filter (fun (p : GenderProfile) => p.genderCount == GenderCount.none) allProfiles).length = 7

Generalization 2: Among gender systems, 2-gender is most common.

Of the 112 languages with gender in the WALS Ch 30 sample, 50 have exactly 2 genders -- the single most common count among gender-bearing languages.

theorem Phenomena.Gender.Typology.two_gender_most_common_among_gendered : 50 > 26 ∧ 50 > 12 ∧ 50 > 24

theorem Phenomena.Gender.Typology.two_gender_in_sample : (List.filter (fun (p : GenderProfile) => p.genderCount == GenderCount.two) allProfiles).length = 5

Generalization 3: Sex-based systems dominate over non-sex-based.

Among languages with gender, sex-based systems (84) far outnumber non-sex-based ones (25) in the WALS Ch 31 sample. In our sample, all 2- and 3-gender systems are sex-based; non-sex-based systems appear only with 4+ categories.

theorem Phenomena.Gender.Typology.sex_based_dominates_wals : (84 > 25 * 3) = (true = true)

theorem Phenomena.Gender.Typology.two_three_gender_all_sex_based : (allProfiles.all fun (p : GenderProfile) => if (p.genderCount == GenderCount.two || p.genderCount == GenderCount.three) = true then p.basis == GenderBasis.sexBased else true) = true

Generalization 4: No purely formal assignment exists.

Corbett's key finding: no language assigns gender on a purely formal basis without any semantic core. In our sample, every language with gender has semantic assignment (either alone or combined with formal).

theorem Phenomena.Gender.Typology.no_purely_formal_in_sample : (allProfiles.all fun (p : GenderProfile) => if (p.genderCount != GenderCount.none) = true then p.assignment == AssignmentSystem.semanticOnly || p.assignment == AssignmentSystem.semanticAndFormal else true) = true

Generalization 5: Formal assignment correlates with more genders.

Languages that combine semantic and formal assignment tend to have richer gender systems. In our sample, all 3-gender languages use semantic + formal assignment, while semantic-only assignment is attested only in 4-gender systems.

theorem Phenomena.Gender.Typology.three_gender_always_formal : (allProfiles.all fun (p : GenderProfile) => if (p.genderCount == GenderCount.three) = true then p.assignment == AssignmentSystem.semanticAndFormal else true) = true

Generalization 6: Agreement targets respect Corbett's hierarchy.

In our sample, every language that shows gender agreement on verbs also shows it on attributive adjectives (i.e., no language agrees only on verbs without agreeing higher on the hierarchy).

def Phenomena.Gender.Typology.hasTarget (targets : List AgreementTarget) (t : AgreementTarget) : Bool

Equations

• Phenomena.Gender.Typology.hasTarget targets t = targets.any fun (x : Core.AgreementTarget) => x == t

theorem Phenomena.Gender.Typology.verb_agreement_implies_attributive : (allProfiles.all fun (p : GenderProfile) => if hasTarget p.agreementTargets Core.AgreementTarget.verbTarget = true then hasTarget p.agreementTargets Core.AgreementTarget.attributive || hasTarget p.agreementTargets Core.AgreementTarget.predicate || hasTarget p.agreementTargets Core.AgreementTarget.personalPronoun else true) = true

Generalization 7: Noun class systems (5+) have the richest agreement.

Languages with 5+ genders show agreement on more targets than languages with fewer genders. In our sample, all noun class systems (Swahili, Zulu, Fula) agree on at least 4 out of 5 target types.

theorem Phenomena.Gender.Typology.noun_class_rich_agreement : (allProfiles.all fun (p : GenderProfile) => if p.isNounClassSystem = true then decide (p.agreementTargets.length ≥ 4) else true) = true

Generalization 8: Non-sex-based systems tend to have more genders.

In our sample, non-sex-based systems have 4+ genders, while sex-based systems have 2--3. This reflects the cross-linguistic pattern: when gender is not organized around sex, the system tends to proliferate into a richer noun class system.

theorem Phenomena.Gender.Typology.non_sex_based_more_genders : (allProfiles.all fun (p : GenderProfile) => if (p.basis == GenderBasis.nonSexBased) = true then decide (p.rawGenderCount ≥ 4) else true) = true

Generalization 9: All GenderCount bins are attested in the sample.

Our 21-language sample covers every WALS Chapter 30 category, from no gender through 5+ genders.

theorem Phenomena.Gender.Typology.all_gender_counts_attested : (((((allProfiles.any fun (p : GenderProfile) => p.genderCount == GenderCount.none) && allProfiles.any fun (p : GenderProfile) => p.genderCount == GenderCount.two) && allProfiles.any fun (p : GenderProfile) => p.genderCount == GenderCount.three) && allProfiles.any fun (p : GenderProfile) => p.genderCount == GenderCount.four) && decide ((allProfiles.any fun (p : GenderProfile) => p.genderCount == GenderCount.fivePlus) = true)) = true

Generalization 10: Gender-bearing languages always show some agreement.

A gender system without any agreement is not a gender system -- genders are precisely the categories that trigger agreement. In our sample, every language with gender has at least one agreement target, and every language without gender has none.

theorem Phenomena.Gender.Typology.gender_implies_agreement : (allProfiles.all fun (p : GenderProfile) => if (p.genderCount != GenderCount.none) = true then p.hasAgreement else !p.hasAgreement) = true

def Phenomena.Gender.Typology.GenderProfile.isCanonicalGender (p : GenderProfile) : Bool

Whether a gender system is "canonical" in Corbett's sense: sex-based, with 2 or 3 genders, and semantic + formal assignment.

Equations

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

theorem Phenomena.Gender.Typology.european_canonical : (french.isCanonicalGender && spanish.isCanonicalGender && german.isCanonicalGender && russian.isCanonicalGender && latin.isCanonicalGender && decide (romanian.isCanonicalGender = true)) = true

The European languages in our sample all have canonical gender systems.

theorem Phenomena.Gender.Typology.hindiUrdu_canonical : hindiUrdu.isCanonicalGender = true

Hindi-Urdu also has a canonical gender system.

theorem Phenomena.Gender.Typology.non_canonical_non_european : (allProfiles.all fun (p : GenderProfile) => if (p.genderCount != GenderCount.none && !p.isCanonicalGender) = true then p.iso639 == "dbl" || p.iso639 == "kat" || p.iso639 == "swh" || p.iso639 == "zul" || p.iso639 == "ful" || p.iso639 == "gle" else true) = true

Non-canonical gender systems (noun class, non-sex-based) are all non-European in our sample.

theorem Phenomena.Gender.Typology.gender_scale_range : (((((allProfiles.any fun (p : GenderProfile) => p.rawGenderCount == 0) && allProfiles.any fun (p : GenderProfile) => p.rawGenderCount == 2) && allProfiles.any fun (p : GenderProfile) => p.rawGenderCount == 3) && allProfiles.any fun (p : GenderProfile) => p.rawGenderCount == 4) && decide ((allProfiles.any fun (p : GenderProfile) => decide (p.rawGenderCount ≥ 15)) = true)) = true

The gender-number scale: languages can be ordered from no gender (0 categories) through systems with progressively more categories. In our sample, the scale spans from 0 (English) to 20 (Fula).

theorem Phenomena.Gender.Typology.max_gender_count_is_fula : ((allProfiles.all fun (p : GenderProfile) => decide (p.rawGenderCount ≤ 20)) && decide ((allProfiles.any fun (p : GenderProfile) => p.rawGenderCount == 20) = true)) = true

The maximum raw gender count in our sample.

theorem Phenomena.Gender.Typology.all_iso_nonempty : (allProfiles.all fun (p : GenderProfile) => decide (p.iso639.length > 0)) = true

All ISO 639-3 codes are non-empty.

theorem Phenomena.Gender.Typology.all_iso_length_3 : (allProfiles.all fun (p : GenderProfile) => p.iso639.length == 3) = true

All ISO 639-3 codes are exactly 3 characters (standard length).

theorem Phenomena.Gender.Typology.iso_codes_unique : (List.map (fun (x : GenderProfile) => x.iso639) allProfiles).eraseDups.length = allProfiles.length

No duplicate ISO codes (each language appears once).

def Phenomena.Gender.Typology.noGenderCount : Nat

Number of no-gender languages in our sample.

Equations

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

def Phenomena.Gender.Typology.sexBasedCount : Nat

Number of sex-based gender languages in our sample.

Equations

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

def Phenomena.Gender.Typology.nonSexBasedCount : Nat

Number of non-sex-based gender languages in our sample.

Equations

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

def Phenomena.Gender.Typology.semanticOnlyCount : Nat

Number of semantic-only assignment languages.

Equations

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

def Phenomena.Gender.Typology.semanticFormalCount : Nat

Number of semantic-and-formal assignment languages.

Equations

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

def Phenomena.Gender.Typology.nounClassCount : Nat

Number of noun class systems (5+).

Equations

• Phenomena.Gender.Typology.nounClassCount = (List.filter (fun (p : Phenomena.Gender.Typology.GenderProfile) => p.isNounClassSystem) Phenomena.Gender.Typology.allProfiles).length

theorem Phenomena.Gender.Typology.noGender_is_7 : noGenderCount = 7

theorem Phenomena.Gender.Typology.sexBased_is_9 : sexBasedCount = 9

theorem Phenomena.Gender.Typology.nonSexBased_is_5 : nonSexBasedCount = 5

theorem Phenomena.Gender.Typology.semanticOnly_is_2 : semanticOnlyCount = 2

theorem Phenomena.Gender.Typology.semanticFormal_is_12 : semanticFormalCount = 12

theorem Phenomena.Gender.Typology.nounClass_is_3 : nounClassCount = 3

theorem Phenomena.Gender.Typology.agreement_hierarchy_verb_implies_higher : (allProfiles.all fun (p : GenderProfile) => if hasTarget p.agreementTargets Core.AgreementTarget.verbTarget = true then hasTarget p.agreementTargets Core.AgreementTarget.attributive || hasTarget p.agreementTargets Core.AgreementTarget.predicate || hasTarget p.agreementTargets Core.AgreementTarget.personalPronoun else true) = true

Corbett's Agreement Hierarchy predicts: if a language shows gender agreement on a lower target, it agrees on all higher targets.

We check: for every pair of targets in a language's agreement list, if a lower-ranked target is present, all higher-ranked targets that the language might show agreement on are consistent with the hierarchy.

Specifically: verb agreement (rank 0) implies at least one higher target (pronoun, predicate, or attributive) is also present.

theorem Phenomena.Gender.Typology.no_verb_only_agreement : (allProfiles.all fun (p : GenderProfile) => if (p.agreementTargets == [Core.AgreementTarget.verbTarget]) = true then false else true) = true

No language in our sample agrees only on verbs.

theorem Phenomena.Gender.Typology.no_pronoun_only_agreement : (allProfiles.all fun (p : GenderProfile) => if (p.genderCount != GenderCount.none && hasTarget p.agreementTargets Core.AgreementTarget.personalPronoun) = true then hasTarget p.agreementTargets Core.AgreementTarget.attributive || hasTarget p.agreementTargets Core.AgreementTarget.predicate || hasTarget p.agreementTargets Core.AgreementTarget.verbTarget else true) = true

No language in our sample has gender agreement only on pronouns: pronoun agreement always co-occurs with at least one other target (attributive, predicate, or verb).

theorem Phenomena.Gender.Typology.semantic_only_is_non_sex_based : (allProfiles.all fun (p : GenderProfile) => if (p.assignment == AssignmentSystem.semanticOnly) = true then p.basis == GenderBasis.nonSexBased else true) = true

Semantic-only assignment is restricted to languages with non-sex-based systems in our sample. This makes sense: sex-based systems typically have formal correlates (declension class, phonological patterns) that supplement the semantic core.

theorem Phenomena.Gender.Typology.sex_based_always_formal : (allProfiles.all fun (p : GenderProfile) => if (p.basis == GenderBasis.sexBased) = true then p.assignment == AssignmentSystem.semanticAndFormal else true) = true

All sex-based systems in our sample use semantic + formal assignment.

theorem Phenomena.Gender.Typology.all_bases_attested : (((allProfiles.any fun (p : GenderProfile) => p.basis == GenderBasis.noGender) && allProfiles.any fun (p : GenderProfile) => p.basis == GenderBasis.sexBased) && decide ((allProfiles.any fun (p : GenderProfile) => p.basis == GenderBasis.nonSexBased) = true)) = true

All three GenderBasis values are attested.

theorem Phenomena.Gender.Typology.all_assignments_attested : (((allProfiles.any fun (p : GenderProfile) => p.assignment == AssignmentSystem.noGender) && allProfiles.any fun (p : GenderProfile) => p.assignment == AssignmentSystem.semanticOnly) && decide ((allProfiles.any fun (p : GenderProfile) => p.assignment == AssignmentSystem.semanticAndFormal) = true)) = true

All three AssignmentSystem values are attested.

theorem Phenomena.Gender.Typology.sample_diversity : (List.filter (fun (p : GenderProfile) => p.genderCount == GenderCount.none) allProfiles).length ≥ 5 ∧ (List.filter (fun (p : GenderProfile) => p.genderCount != GenderCount.none) allProfiles).length ≥ 5

The sample spans at least 5 distinct ISO codes in each category (gender-bearing vs genderless).

Per-language grounding theorems verify that each profile's field values agree with the corresponding WALS chapter data via the converter functions.

Languages with known discrepancies between our profile classifications and WALS are skipped on the discrepant chapter:

• English: WALS F30A records 3 genders (pronominal he/she/it), but our profile treats English as genderless (no gender agreement on nouns/adjectives).
• Georgian: WALS F30A records no gender, but our profile follows analyses that posit 4 categories (rational/non-rational × older masc/fem trace).
• Dyirbal: WALS F31A records sex-based, but our profile classifies the system as non-sex-based (the 4-way system includes edibility/natural-force categories beyond biological sex).

theorem Phenomena.Gender.Typology.mandarin_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "mnd") = some mandarin.genderCount

theorem Phenomena.Gender.Typology.turkish_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "tur") = some turkish.genderCount

theorem Phenomena.Gender.Typology.finnish_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "fin") = some finnish.genderCount

theorem Phenomena.Gender.Typology.french_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "fre") = some french.genderCount

theorem Phenomena.Gender.Typology.spanish_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "spa") = some spanish.genderCount

theorem Phenomena.Gender.Typology.hindiUrdu_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "hin") = some hindiUrdu.genderCount

theorem Phenomena.Gender.Typology.hebrew_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "heb") = some hebrew.genderCount

theorem Phenomena.Gender.Typology.german_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "ger") = some german.genderCount

theorem Phenomena.Gender.Typology.russian_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "rus") = some russian.genderCount

theorem Phenomena.Gender.Typology.dyirbal_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "dyi") = some dyirbal.genderCount

theorem Phenomena.Gender.Typology.swahili_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "swa") = some swahili.genderCount

theorem Phenomena.Gender.Typology.zulu_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "zul") = some zulu.genderCount

theorem Phenomena.Gender.Typology.fula_ch30 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F30A.GenderCount) => Phenomena.Gender.Typology.fromWALS30A✝ x.value) (Core.WALS.F30A.lookup "fgu") = some fula.genderCount

theorem Phenomena.Gender.Typology.mandarin_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "mnd") = some mandarin.basis

theorem Phenomena.Gender.Typology.turkish_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "tur") = some turkish.basis

theorem Phenomena.Gender.Typology.finnish_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "fin") = some finnish.basis

theorem Phenomena.Gender.Typology.french_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "fre") = some french.basis

theorem Phenomena.Gender.Typology.spanish_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "spa") = some spanish.basis

theorem Phenomena.Gender.Typology.hindiUrdu_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "hin") = some hindiUrdu.basis

theorem Phenomena.Gender.Typology.hebrew_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "heb") = some hebrew.basis

theorem Phenomena.Gender.Typology.german_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "ger") = some german.basis

theorem Phenomena.Gender.Typology.russian_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "rus") = some russian.basis

theorem Phenomena.Gender.Typology.swahili_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "swa") = some swahili.basis

theorem Phenomena.Gender.Typology.zulu_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "zul") = some zulu.basis

theorem Phenomena.Gender.Typology.fula_ch31 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F31A.GenderBasis) => Phenomena.Gender.Typology.fromWALS31A✝ x.value) (Core.WALS.F31A.lookup "fgu") = some fula.basis

theorem Phenomena.Gender.Typology.mandarin_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "mnd") = some mandarin.assignment

theorem Phenomena.Gender.Typology.turkish_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "tur") = some turkish.assignment

theorem Phenomena.Gender.Typology.finnish_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "fin") = some finnish.assignment

theorem Phenomena.Gender.Typology.french_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "fre") = some french.assignment

theorem Phenomena.Gender.Typology.spanish_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "spa") = some spanish.assignment

theorem Phenomena.Gender.Typology.hindiUrdu_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "hin") = some hindiUrdu.assignment

theorem Phenomena.Gender.Typology.hebrew_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "heb") = some hebrew.assignment

theorem Phenomena.Gender.Typology.german_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "ger") = some german.assignment

theorem Phenomena.Gender.Typology.russian_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "rus") = some russian.assignment

theorem Phenomena.Gender.Typology.dyirbal_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "dyi") = some dyirbal.assignment

theorem Phenomena.Gender.Typology.swahili_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "swa") = some swahili.assignment

theorem Phenomena.Gender.Typology.zulu_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "zul") = some zulu.assignment

theorem Phenomena.Gender.Typology.fula_ch32 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F32A.SystemsOfGenderAssignment) => Phenomena.Gender.Typology.fromWALS32A✝ x.value) (Core.WALS.F32A.lookup "fgu") = some fula.assignment