Pronoun typology — substrate types

@cite{wals-2013} (Chs 39, 39B, 40, 44–48)

Type-level enums + per-language profile struct for pronoun systems across @cite{wals-2013} chapters 39–40 and 44–48: inclusive/exclusive distinctions, gender, politeness, indefinite-pronoun strategy, intensifier–reflexive relationship, person marking on adpositions.

Schema

• InclusiveExclusive (Ch 39): incl/excl in independent pronouns
• InclusiveExclusivePamaNyungan (Ch 39B): areal sub-feature for Pama-Nyungan
• InclusiveExclusiveVerbal (Ch 40): incl/excl in verbal inflection
• GenderInPronouns (Ch 44): gender distinctions in personal pronouns
• PolitenessDistinction (Ch 45): T/V and broader politeness contrasts
• IndefinitePronounType (Ch 46): morphological source of indefinites
• IntensifierReflexive (Ch 47): intensifier ↔ reflexive identity
• PersonMarkingOnAdpositions (Ch 48): adpositional person marking
• PronounProfile: per-language bundle (all WALS chapters as Option fields)

inductive Typology.InclusiveExclusive : Type

WALS Ch 39: inclusive/exclusive distinction in independent pronouns.

• noWe : InclusiveExclusive

  No first-person plural pronoun at all.

• weEqualsI : InclusiveExclusive

  'We' = 'I' (no number distinction in 1st person).

• noDistinction : InclusiveExclusive

  1st-pl exists but no incl/excl distinction.

• onlyInclusive : InclusiveExclusive

  Only inclusive form; no dedicated exclusive pronoun.

• inclusiveExclusive : InclusiveExclusive

  Full inclusive/exclusive distinction in 1st-pl.

@[implicit_reducible]

instance Typology.instDecidableEqInclusiveExclusive : DecidableEq InclusiveExclusive

Equations

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

@[implicit_reducible]

instance Typology.instReprInclusiveExclusive : Repr InclusiveExclusive

Equations

• Typology.instReprInclusiveExclusive = { reprPrec := Typology.instReprInclusiveExclusive.repr }

def Typology.instReprInclusiveExclusive.repr : InclusiveExclusive → ℕ → Std.Format

Equations

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

inductive Typology.InclusiveExclusivePamaNyungan : Type

WALS Ch 39B: incl/excl forms in Pama-Nyungan languages (areal sub-feature).

• noOpposition : InclusiveExclusivePamaNyungan

  No incl/excl opposition in 1st-pl.

• differentiated : InclusiveExclusivePamaNyungan

  Inclusive and exclusive forms differentiated.

@[implicit_reducible]

instance Typology.instDecidableEqInclusiveExclusivePamaNyungan : DecidableEq InclusiveExclusivePamaNyungan

Equations

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

@[implicit_reducible]

instance Typology.instReprInclusiveExclusivePamaNyungan : Repr InclusiveExclusivePamaNyungan

Equations

• Typology.instReprInclusiveExclusivePamaNyungan = { reprPrec := Typology.instReprInclusiveExclusivePamaNyungan.repr }

def Typology.instReprInclusiveExclusivePamaNyungan.repr : InclusiveExclusivePamaNyungan → ℕ → Std.Format

Equations

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

inductive Typology.InclusiveExclusiveVerbal : Type

WALS Ch 40: incl/excl distinction in verbal inflection.

• noPersonMarking : InclusiveExclusiveVerbal

  No person marking on verbs at all.

• weEqualsI : InclusiveExclusiveVerbal

  'We' verbal form = 'I' form.

• noDistinction : InclusiveExclusiveVerbal

  Person marking exists but no incl/excl.

• onlyInclusive : InclusiveExclusiveVerbal

  Only inclusive marking in verbal inflection.

• inclusiveExclusive : InclusiveExclusiveVerbal

  Full incl/excl distinction in verbal inflection.

@[implicit_reducible]

instance Typology.instDecidableEqInclusiveExclusiveVerbal : DecidableEq InclusiveExclusiveVerbal

Equations

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

@[implicit_reducible]

instance Typology.instReprInclusiveExclusiveVerbal : Repr InclusiveExclusiveVerbal

Equations

• Typology.instReprInclusiveExclusiveVerbal = { reprPrec := Typology.instReprInclusiveExclusiveVerbal.repr }

def Typology.instReprInclusiveExclusiveVerbal.repr : InclusiveExclusiveVerbal → ℕ → Std.Format

Equations

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

inductive Typology.GenderInPronouns : Type

WALS Ch 44: where gender distinctions appear in the pronoun paradigm.

• in3rdAndOtherPersons : GenderInPronouns

  Gender in 3rd person AND in 1st/2nd person (e.g., Arabic, Hebrew).

• in3rdPersonIncludingNonSg : GenderInPronouns

  Gender in 3rd person only, including non-singular forms (e.g., Polish, Albanian).

• in3rdPersonSgOnly : GenderInPronouns

  Gender in 3rd person singular only (e.g., English he/she/it).

• in1stOr2ndOnly : GenderInPronouns

  Gender in 1st or 2nd person but not 3rd (rare; e.g., Iraqw).

• in3rdPersonNonSgOnly : GenderInPronouns

  Gender in 3rd person non-singular only (extremely rare).

• noGenderDistinctions : GenderInPronouns

  No gender distinctions in pronouns (e.g., Finnish, Turkish, Japanese).

@[implicit_reducible]

instance Typology.instDecidableEqGenderInPronouns : DecidableEq GenderInPronouns

Equations

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

def Typology.instReprGenderInPronouns.repr : GenderInPronouns → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprGenderInPronouns : Repr GenderInPronouns

Equations

• Typology.instReprGenderInPronouns = { reprPrec := Typology.instReprGenderInPronouns.repr }

inductive Typology.PolitenessDistinction : Type

WALS Ch 45: politeness (honorific/formality) distinctions in pronouns.

• none : PolitenessDistinction

  No politeness distinction (e.g., English).

• binary : PolitenessDistinction

  Binary T/V distinction (e.g., French tu/vous, German du/Sie).

• multiple : PolitenessDistinction

  Multiple levels (e.g., Japanese, Hindi, Tagalog).

• pronounsAvoided : PolitenessDistinction

  Pronouns avoided entirely for politeness; titles/kin terms used instead (e.g., Korean, Thai).

@[implicit_reducible]

instance Typology.instDecidableEqPolitenessDistinction : DecidableEq PolitenessDistinction

Equations

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

def Typology.instReprPolitenessDistinction.repr : PolitenessDistinction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprPolitenessDistinction : Repr PolitenessDistinction

Equations

• Typology.instReprPolitenessDistinction = { reprPrec := Typology.instReprPolitenessDistinction.repr }

inductive Typology.IndefinitePronounType : Type

WALS Ch 46: morphological source of indefinite pronouns.

• interrogativeBased : IndefinitePronounType

  Based on interrogative forms (e.g., Japanese dare-ka 'who-Q' = 'someone').

• genericNounBased : IndefinitePronounType

  Based on generic nouns (e.g., English 'somebody' = 'some' + 'body').

• special : IndefinitePronounType

  Special, dedicated forms unrelated to interrogatives or generic nouns.

• mixed : IndefinitePronounType

  Mixed: some interrogative-based, others generic-noun-based.

• existentialConstruction : IndefinitePronounType

  Existential construction used instead of indefinite pronouns.

@[implicit_reducible]

instance Typology.instDecidableEqIndefinitePronounType : DecidableEq IndefinitePronounType

Equations

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

@[implicit_reducible]

instance Typology.instReprIndefinitePronounType : Repr IndefinitePronounType

Equations

• Typology.instReprIndefinitePronounType = { reprPrec := Typology.instReprIndefinitePronounType.repr }

def Typology.instReprIndefinitePronounType.repr : IndefinitePronounType → ℕ → Std.Format

Equations

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

inductive Typology.IntensifierReflexive : Type

WALS Ch 47: relationship between intensifiers and reflexives.

• identical : IntensifierReflexive

  Identical forms ('she herself did it' / 'she saw herself').

• differentiated : IntensifierReflexive

  Different, morphologically unrelated forms.

@[implicit_reducible]

instance Typology.instDecidableEqIntensifierReflexive : DecidableEq IntensifierReflexive

Equations

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

def Typology.instReprIntensifierReflexive.repr : IntensifierReflexive → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprIntensifierReflexive : Repr IntensifierReflexive

Equations

• Typology.instReprIntensifierReflexive = { reprPrec := Typology.instReprIntensifierReflexive.repr }

inductive Typology.PersonMarkingOnAdpositions : Type

WALS Ch 48: whether adpositions bear person-marking morphology.

• noAdpositions : PersonMarkingOnAdpositions

  Language has no adpositions (head-marking or caseless).

• noPersonMarking : PersonMarkingOnAdpositions

  Adpositions exist but bear no person marking.

• pronounsOnly : PersonMarkingOnAdpositions

  Only pronominal complements trigger person marking (e.g., Hebrew be-xa 'in-you').

• pronounsAndNouns : PersonMarkingOnAdpositions

  Both pronominal and nominal complements trigger person marking.

@[implicit_reducible]

instance Typology.instDecidableEqPersonMarkingOnAdpositions : DecidableEq PersonMarkingOnAdpositions

Equations

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

@[implicit_reducible]

instance Typology.instReprPersonMarkingOnAdpositions : Repr PersonMarkingOnAdpositions

Equations

• Typology.instReprPersonMarkingOnAdpositions = { reprPrec := Typology.instReprPersonMarkingOnAdpositions.repr }

def Typology.instReprPersonMarkingOnAdpositions.repr : PersonMarkingOnAdpositions → ℕ → Std.Format

Equations

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

structure Typology.PronounProfile : Type

A language's pronoun-system profile across WALS Chs 39–40, 44–48. Not all chapters have data for every language (sample varies by chapter), so each field is Option.

• language : String
• family : String
• iso : String
• inclusiveExclusive : Option InclusiveExclusive

  Ch 39: incl/excl in independent pronouns.

• inclusiveExclusiveVerbal : Option InclusiveExclusiveVerbal

  Ch 40: incl/excl in verbal inflection.

• genderInPronouns : Option GenderInPronouns

  Ch 44: gender distinctions.

• politeness : Option PolitenessDistinction

  Ch 45: politeness distinctions.

• indefiniteType : Option IndefinitePronounType

  Ch 46: indefinite pronoun strategy.

• intensifierReflexive : Option IntensifierReflexive

  Ch 47: intensifier-reflexive relationship.

• personMarkingAdpositions : Option PersonMarkingOnAdpositions

  Ch 48: person marking on adpositions.

def Typology.instReprPronounProfile.repr : PronounProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprPronounProfile : Repr PronounProfile

Equations

• Typology.instReprPronounProfile = { reprPrec := Typology.instReprPronounProfile.repr }

def Typology.instDecidableEqPronounProfile.decEq (x✝ x✝¹ : PronounProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Typology.instDecidableEqPronounProfile : DecidableEq PronounProfile

Equations

• Typology.instDecidableEqPronounProfile = Typology.instDecidableEqPronounProfile.decEq

def Typology.fromWALS39A : Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns → InclusiveExclusive

Equations

• Typology.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.noWe = Typology.InclusiveExclusive.noWe
• Typology.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.weTheSameAsI = Typology.InclusiveExclusive.weEqualsI
• Typology.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.noInclusiveExclusive = Typology.InclusiveExclusive.noDistinction
• Typology.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.onlyInclusive = Typology.InclusiveExclusive.onlyInclusive
• Typology.fromWALS39A Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.inclusiveExclusive = Typology.InclusiveExclusive.inclusiveExclusive

def Typology.fromWALS39B : Data.WALS.F39B.InclusiveExclusiveFormsInPamaNyungan → InclusiveExclusivePamaNyungan

Equations

• Typology.fromWALS39B Data.WALS.F39B.InclusiveExclusiveFormsInPamaNyungan.noInclusiveExclusiveOpposition = Typology.InclusiveExclusivePamaNyungan.noOpposition
• Typology.fromWALS39B Data.WALS.F39B.InclusiveExclusiveFormsInPamaNyungan.inclusiveAndExclusiveDifferentiated = Typology.InclusiveExclusivePamaNyungan.differentiated

def Typology.fromWALS40A : Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection → InclusiveExclusiveVerbal

Equations

• Typology.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.noPersonMarking = Typology.InclusiveExclusiveVerbal.noPersonMarking
• Typology.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.weTheSameAsI = Typology.InclusiveExclusiveVerbal.weEqualsI
• Typology.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.noInclusiveExclusive = Typology.InclusiveExclusiveVerbal.noDistinction
• Typology.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.onlyInclusive = Typology.InclusiveExclusiveVerbal.onlyInclusive
• Typology.fromWALS40A Data.WALS.F40A.InclusiveExclusiveDistinctionInVerbalInflection.inclusiveExclusive = Typology.InclusiveExclusiveVerbal.inclusiveExclusive

def Typology.fromWALS44A : Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns → GenderInPronouns

Equations

• Typology.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.in3rdPerson1stAndOr2ndPerson = Typology.GenderInPronouns.in3rdAndOtherPersons
• Typology.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonOnlyButAlsoNonSingular = Typology.GenderInPronouns.in3rdPersonIncludingNonSg
• Typology.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonSingularOnly = Typology.GenderInPronouns.in3rdPersonSgOnly
• Typology.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v1stOr2ndPersonButNot3rd = Typology.GenderInPronouns.in1stOr2ndOnly
• Typology.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonNonSingularOnly = Typology.GenderInPronouns.in3rdPersonNonSgOnly
• Typology.fromWALS44A Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.noGenderDistinctions = Typology.GenderInPronouns.noGenderDistinctions

def Typology.fromWALS45A : Data.WALS.F45A.PolitenessDistinctionsInPronouns → PolitenessDistinction

Equations

• Typology.fromWALS45A Data.WALS.F45A.PolitenessDistinctionsInPronouns.noPolitenessDistinction = Typology.PolitenessDistinction.none
• Typology.fromWALS45A Data.WALS.F45A.PolitenessDistinctionsInPronouns.binaryPolitenessDistinction = Typology.PolitenessDistinction.binary
• Typology.fromWALS45A Data.WALS.F45A.PolitenessDistinctionsInPronouns.multiplePolitenessDistinctions = Typology.PolitenessDistinction.multiple
• Typology.fromWALS45A Data.WALS.F45A.PolitenessDistinctionsInPronouns.pronounsAvoidedForPoliteness = Typology.PolitenessDistinction.pronounsAvoided

def Typology.fromWALS46A : Data.WALS.F46A.IndefinitePronouns → IndefinitePronounType

Equations

• Typology.fromWALS46A Data.WALS.F46A.IndefinitePronouns.interrogativeBased = Typology.IndefinitePronounType.interrogativeBased
• Typology.fromWALS46A Data.WALS.F46A.IndefinitePronouns.genericNounBased = Typology.IndefinitePronounType.genericNounBased
• Typology.fromWALS46A Data.WALS.F46A.IndefinitePronouns.special = Typology.IndefinitePronounType.special
• Typology.fromWALS46A Data.WALS.F46A.IndefinitePronouns.mixed = Typology.IndefinitePronounType.mixed
• Typology.fromWALS46A Data.WALS.F46A.IndefinitePronouns.existentialConstruction = Typology.IndefinitePronounType.existentialConstruction

def Typology.fromWALS47A : Data.WALS.F47A.IntensifierReflexive → IntensifierReflexive

Equations

• Typology.fromWALS47A Data.WALS.F47A.IntensifierReflexive.identical = Typology.IntensifierReflexive.identical
• Typology.fromWALS47A Data.WALS.F47A.IntensifierReflexive.differentiated = Typology.IntensifierReflexive.differentiated

def Typology.fromWALS48A : Data.WALS.F48A.PersonMarkingOnAdpositions → PersonMarkingOnAdpositions

Equations

• Typology.fromWALS48A Data.WALS.F48A.PersonMarkingOnAdpositions.noAdpositions = Typology.PersonMarkingOnAdpositions.noAdpositions
• Typology.fromWALS48A Data.WALS.F48A.PersonMarkingOnAdpositions.noPersonMarking = Typology.PersonMarkingOnAdpositions.noPersonMarking
• Typology.fromWALS48A Data.WALS.F48A.PersonMarkingOnAdpositions.pronounsOnly = Typology.PersonMarkingOnAdpositions.pronounsOnly
• Typology.fromWALS48A Data.WALS.F48A.PersonMarkingOnAdpositions.pronounsAndNouns = Typology.PersonMarkingOnAdpositions.pronounsAndNouns

theorem Typology.noDistinction_is_majority_ch39 : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns) => x.value == Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.noInclusiveExclusive) Typology.ch39✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns) => x.value == Data.WALS.F39A.InclusiveExclusiveDistinctionInIndependentPronouns.inclusiveExclusive) Typology.ch39✝).length

Majority of languages (120/200) make no inclusive/exclusive distinction in independent pronouns.

theorem Typology.noGender_is_majority_ch44 : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns) => x.value == Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.noGenderDistinctions) Typology.ch44✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns) => x.value == Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonSingularOnly) Typology.ch44✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns) => x.value == Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.v3rdPersonOnlyButAlsoNonSingular) Typology.ch44✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns) => x.value == Data.WALS.F44A.GenderDistinctionsInIndependentPersonalPronouns.in3rdPerson1stAndOr2ndPerson) Typology.ch44✝).length

No gender distinctions in pronouns is the majority pattern (254/378 = 67.2%).

theorem Typology.noPoliteness_is_majority_ch45 : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => x.value == Data.WALS.F45A.PolitenessDistinctionsInPronouns.noPolitenessDistinction) Typology.ch45✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => x.value == Data.WALS.F45A.PolitenessDistinctionsInPronouns.binaryPolitenessDistinction) Typology.ch45✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => x.value == Data.WALS.F45A.PolitenessDistinctionsInPronouns.multiplePolitenessDistinctions) Typology.ch45✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F45A.PolitenessDistinctionsInPronouns) => x.value == Data.WALS.F45A.PolitenessDistinctionsInPronouns.pronounsAvoidedForPoliteness) Typology.ch45✝).length

Most languages lack politeness distinctions in pronouns (136/207 = 65.7%).

inductive Typology.MTPronounPattern : Type

M-T pronoun pattern (WALS Ch 136A, @cite{nichols-peterson-2013}): whether 1SG has /m/ and 2SG has /t/, a widespread cross-linguistic pattern hypothesized to reflect deep genealogical signal.

• absent : MTPronounPattern

  No M-T pattern in the pronoun paradigm.

• paradigmatic : MTPronounPattern

  M-T pattern is paradigmatic (systematic across forms).

• nonParadigmatic : MTPronounPattern

  M-T pattern is non-paradigmatic (sporadic).

@[implicit_reducible]

instance Typology.instDecidableEqMTPronounPattern : DecidableEq MTPronounPattern

Equations

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

@[implicit_reducible]

instance Typology.instReprMTPronounPattern : Repr MTPronounPattern

Equations

• Typology.instReprMTPronounPattern = { reprPrec := Typology.instReprMTPronounPattern.repr }

def Typology.instReprMTPronounPattern.repr : MTPronounPattern → ℕ → Std.Format

Equations

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

inductive Typology.MIn1SG : Type

Whether 1SG has an m-initial or m-containing form (WALS Ch 136B).

• absent : MIn1SG
• present : MIn1SG

@[implicit_reducible]

instance Typology.instDecidableEqMIn1SG : DecidableEq MIn1SG

Equations

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

def Typology.instReprMIn1SG.repr : MIn1SG → ℕ → Std.Format

Equations

• Typology.instReprMIn1SG.repr Typology.MIn1SG.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.MIn1SG.absent")).group prec✝
• Typology.instReprMIn1SG.repr Typology.MIn1SG.present prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.MIn1SG.present")).group prec✝

@[implicit_reducible]

instance Typology.instReprMIn1SG : Repr MIn1SG

Equations

• Typology.instReprMIn1SG = { reprPrec := Typology.instReprMIn1SG.repr }

inductive Typology.NMPronounPattern : Type

N-M pronoun pattern (WALS Ch 137A, @cite{nichols-peterson-2013}): whether 1SG has /n/ and 2SG has /m/.

• absent : NMPronounPattern
• paradigmatic : NMPronounPattern
• nonParadigmatic : NMPronounPattern

@[implicit_reducible]

instance Typology.instDecidableEqNMPronounPattern : DecidableEq NMPronounPattern

Equations

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

def Typology.instReprNMPronounPattern.repr : NMPronounPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprNMPronounPattern : Repr NMPronounPattern

Equations

• Typology.instReprNMPronounPattern = { reprPrec := Typology.instReprNMPronounPattern.repr }

inductive Typology.MIn2SG : Type

Whether 2SG has an m-initial or m-containing form (WALS Ch 137B).

• absent : MIn2SG
• present : MIn2SG

@[implicit_reducible]

instance Typology.instDecidableEqMIn2SG : DecidableEq MIn2SG

Equations

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

def Typology.instReprMIn2SG.repr : MIn2SG → ℕ → Std.Format

Equations

• Typology.instReprMIn2SG.repr Typology.MIn2SG.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.MIn2SG.absent")).group prec✝
• Typology.instReprMIn2SG.repr Typology.MIn2SG.present prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.MIn2SG.present")).group prec✝

@[implicit_reducible]

instance Typology.instReprMIn2SG : Repr MIn2SG

Equations

• Typology.instReprMIn2SG = { reprPrec := Typology.instReprMIn2SG.repr }

structure Typology.PronounShapeProfile : Type

A language's pronoun-shape profile across @cite{wals-2013} Chs 136–137. Sister to PronounProfile (Chs 39–48). Kept as a separate struct to avoid contaminating the feature-system bundle with phonological-shape fields.

• language : String
• iso : String
• mtPronouns : Option MTPronounPattern

  Ch 136A: M-T pronoun pattern.

• mIn1sg : Option MIn1SG

  Ch 136B: M in 1SG.

• nmPronouns : Option NMPronounPattern

  Ch 137A: N-M pronoun pattern.

• mIn2sg : Option MIn2SG

  Ch 137B: M in 2SG.

@[implicit_reducible]

instance Typology.instReprPronounShapeProfile : Repr PronounShapeProfile

Equations

• Typology.instReprPronounShapeProfile = { reprPrec := Typology.instReprPronounShapeProfile.repr }

def Typology.instReprPronounShapeProfile.repr : PronounShapeProfile → ℕ → Std.Format

Equations

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

def Typology.fromWALS136A : Data.WALS.F136A.MTPronouns → MTPronounPattern

Equations

• Typology.fromWALS136A Data.WALS.F136A.MTPronouns.noMTPronouns = Typology.MTPronounPattern.absent
• Typology.fromWALS136A Data.WALS.F136A.MTPronouns.mTPronounsParadigmatic = Typology.MTPronounPattern.paradigmatic
• Typology.fromWALS136A Data.WALS.F136A.MTPronouns.mTPronounsNonParadigmatic = Typology.MTPronounPattern.nonParadigmatic

def Typology.fromWALS136B : Data.WALS.F136B.MInFirstPersonSingular → MIn1SG

Equations

• Typology.fromWALS136B Data.WALS.F136B.MInFirstPersonSingular.noMInFirstPersonSingular = Typology.MIn1SG.absent
• Typology.fromWALS136B Data.WALS.F136B.MInFirstPersonSingular.mInFirstPersonSingular = Typology.MIn1SG.present

def Typology.fromWALS137A : Data.WALS.F137A.NMPronouns → NMPronounPattern

Equations

• Typology.fromWALS137A Data.WALS.F137A.NMPronouns.noNMPronouns = Typology.NMPronounPattern.absent
• Typology.fromWALS137A Data.WALS.F137A.NMPronouns.nMPronounsParadigmatic = Typology.NMPronounPattern.paradigmatic
• Typology.fromWALS137A Data.WALS.F137A.NMPronouns.nMPronounsNonParadigmatic = Typology.NMPronounPattern.nonParadigmatic

def Typology.fromWALS137B : Data.WALS.F137B.MInSecondPersonSingular → MIn2SG

Equations

• Typology.fromWALS137B Data.WALS.F137B.MInSecondPersonSingular.noMInSecondPersonSingular = Typology.MIn2SG.absent
• Typology.fromWALS137B Data.WALS.F137B.MInSecondPersonSingular.mInSecondPersonSingular = Typology.MIn2SG.present

structure Typology.MTCounts : Type

WALS Ch 136A distribution: M-T pronoun patterns (@cite{nichols-peterson-2013}, n = 230).

• absent : ℕ
• paradigmatic : ℕ
• nonParadigmatic : ℕ

@[implicit_reducible]

instance Typology.instReprMTCounts : Repr MTCounts

Equations

• Typology.instReprMTCounts = { reprPrec := Typology.instReprMTCounts.repr }

def Typology.instReprMTCounts.repr : MTCounts → ℕ → Std.Format

Equations

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

def Typology.MTCounts.total (c : MTCounts) : ℕ

Equations

• c.total = c.absent + c.paradigmatic + c.nonParadigmatic

def Typology.walsMT : MTCounts

WALS Ch 136A counts (230 languages).

Equations

• Typology.walsMT = { absent := 200, paradigmatic := 27, nonParadigmatic := 3 }

theorem Typology.mt_pronouns_minority : walsMT.absent > walsMT.paradigmatic + walsMT.nonParadigmatic

The M-T pronoun pattern is a clear minority cross-linguistically: only 30/230 languages (~13%) show any form of it; 200/230 lack it entirely. Despite its visibility in Indo-European, it is not a typological default.

Cross-linguistic pronoun and allocutive entry schemas

@cite{alok-bhalla-2026} @cite{arnold-2026}

Cross-linguistic structures for pronoun inventories and allocutive markers, shared across all Fragments/{Lang}/Pronouns.lean files.

Moved here from Core/Lexical/Pronouns.lean in the cleanup that dissolved Core/Lexical/. The 21-consumer footprint (20 Fragments + 1 Phenomena study) is precisely the per-language entry-schema pattern this file already serves for WALS-anchored substrate enums.

PronounEntry

Covers the union of fields needed by all language fragments:

• Core: form, person, number (all fragments)
• Morphosyntactic: case_, gender (Galician, English, French, etc.)
• Sociolinguistic: register (all SA-based fragments)
• Orthographic: script (Korean hangul, Japanese kanji)

PronounSpec

Personal pronoun specification — which pronouns a person uses. A social-linguistic fact independent of grammatical gender. @cite{arnold-2026}'s pragmatic condition for personal singular they: referent's pronouns are known to be they/them.

AllocutiveEntry

Verbal suffixes (Hindi, Magahi, Maithili, Punjabi, Tamil, Basque), particles (Korean, Japanese), or clitics (Galician) realising speaker-addressee agreement.

inductive Typology.PronounSpec : Type

Personal pronoun specification — which pronouns a person uses.

A social-linguistic fact that may or may not be in common ground. Independent of grammatical gender: a person with known feminine gender may use she/her, they/them, or neopronouns. @cite{arnold-2026}: the pragmatic condition for personal singular they is knowing that the referent's personal pronouns are they/them.

• heHim : PronounSpec
• sheHer : PronounSpec
• theyThem : PronounSpec

@[implicit_reducible]

instance Typology.instDecidableEqPronounSpec : DecidableEq PronounSpec

Equations

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

def Typology.instReprPronounSpec.repr : PronounSpec → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprPronounSpec : Repr PronounSpec

Equations

• Typology.instReprPronounSpec = { reprPrec := Typology.instReprPronounSpec.repr }

@[implicit_reducible]

instance Typology.instBEqPronounSpec : BEq PronounSpec

Equations

• Typology.instBEqPronounSpec = { beq := Typology.instBEqPronounSpec.beq }

def Typology.instBEqPronounSpec.beq : PronounSpec → PronounSpec → Bool

Equations

• Typology.instBEqPronounSpec.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Typology.PronounEntry : Type

Cross-linguistic pronoun entry.

Covers personal pronouns across all Fragment languages. Language-specific extensions (e.g., English PronounType/wh) remain in their respective Fragment files.

• form : String

  Surface form (romanization or orthographic)

• person : Option Person

  Grammatical person (UD.Person via Core.Word abbrev)

• number : Option Number

  Grammatical number

• case_ : Option Case

  Grammatical case

• gender : Option Features.SurfaceGender

  Grammatical gender. For 3rd-person pronouns in gendered languages (French il/elle, German er/sie/es, etc.). 1st/2nd-person pronouns and languages without pronominal gender leave this as none.

• register : Features.Register.Level

  Register level (formality/honorifics). Binary T/V systems use .informal/.formal; ternary honorific systems (Hindi, Magahi, Maithili, Korean) use all three levels.

• referentialPerson : Option Features.Prominence.PersonLevel

  Referential person — who the pronoun refers to in terms of discourse role — when it diverges from formal/agreement person. For polite pronouns (Italian LEI, Spanish USTED, German SIE), the formal person field is 3rd (governing agreement, clitic allomorphy, reflexive binding), while referentialPerson is 2nd (governing the PCC, Fancy Constraint, resolved agreement). For ordinary pronouns, leave as none — referential person coincides with formal person. @cite{adamson-zompi-2025}

• script : Option String

  Native script form (hangul, kanji, Devanagari, etc.)

@[implicit_reducible]

instance Typology.instReprPronounEntry : Repr PronounEntry

Equations

• Typology.instReprPronounEntry = { reprPrec := Typology.instReprPronounEntry.repr }

def Typology.instReprPronounEntry.repr : PronounEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instBEqPronounEntry : BEq PronounEntry

Equations

• Typology.instBEqPronounEntry = { beq := Typology.instBEqPronounEntry.beq }

def Typology.instBEqPronounEntry.beq : PronounEntry → PronounEntry → Bool

Equations

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

structure Typology.AllocutiveEntry : Type

Cross-linguistic allocutive marker entry.

Covers verbal suffixes, particles, and clitics that realize allocutive agreement across all Fragment languages.

• form : String

  Surface form of the marker

• register : Features.Register.Level

  Register level (matching PronounEntry.register scale)

• gloss : String

  Gloss string (e.g., "IMP.NH", "POL", "2sg.DAT.fam")

@[implicit_reducible]

instance Typology.instReprAllocutiveEntry : Repr AllocutiveEntry

Equations

• Typology.instReprAllocutiveEntry = { reprPrec := Typology.instReprAllocutiveEntry.repr }

def Typology.instReprAllocutiveEntry.repr : AllocutiveEntry → ℕ → Std.Format

Equations

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

def Typology.instBEqAllocutiveEntry.beq : AllocutiveEntry → AllocutiveEntry → Bool

Equations

• Typology.instBEqAllocutiveEntry.beq { form := a, register := a_1, gloss := a_2 } { form := b, register := b_1, gloss := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Typology.instBEqAllocutiveEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Typology.instBEqAllocutiveEntry : BEq AllocutiveEntry

Equations

• Typology.instBEqAllocutiveEntry = { beq := Typology.instBEqAllocutiveEntry.beq }

def Typology.InclusiveExclusive.fromClusivity : Features.Clusivity.System → InclusiveExclusive

WALS Ch 39 image of a Cysouw clusivity system (Features.Clusivity.System): WALS Ch 39 collapses Cysouw's .inclExcl, .minimalAugmented, and .unitAugmented into the single value .inclusiveExclusive. The function is therefore many-to-one: given a WALS Ch 39 value, the Cysouw value is underdetermined.

Equations

• Typology.InclusiveExclusive.fromClusivity Features.Clusivity.System.noClusivity = Typology.InclusiveExclusive.noDistinction
• Typology.InclusiveExclusive.fromClusivity Features.Clusivity.System.inclExcl = Typology.InclusiveExclusive.inclusiveExclusive
• Typology.InclusiveExclusive.fromClusivity Features.Clusivity.System.minimalAugmented = Typology.InclusiveExclusive.inclusiveExclusive
• Typology.InclusiveExclusive.fromClusivity Features.Clusivity.System.unitAugmented = Typology.InclusiveExclusive.inclusiveExclusive
• Typology.InclusiveExclusive.fromClusivity Features.Clusivity.System.numberIndifferent = Typology.InclusiveExclusive.weEqualsI