K'iche' Agreement Fragment @cite{mondloch-2017}

Agreement morphology for K'iche' (K'ichean Mayan), following @cite{mondloch-2017} Lessons 4, 7–8, 9, 15.

The System

K'iche' has an ergative-absolutive alignment system realized through two agreement paradigms on the verb:

• Set B (ABS): absolutive markers that cross-reference the sole argument of intransitives (S) and the object of transitives (P). These appear between the aspect marker and the verb root.
• Set A (ERG): ergative markers that cross-reference the subject of transitives (A). These appear between the object marker and the root. Set A markers are identical to the possessive pronouns used before consonant-initial nouns (Lesson 7).

Paradigms

Set B (Absolutive) — Lesson 9

Person	Singular	Plural
1	in-	oj-
2	at-	ix-
3	Ø-	ee-
2.FORM	la (postverbal)	alaq (postverbal)

Set A (Ergative, preconsonantal) — Lessons 7, 15

Person	Singular	Plural
1	nu‑ / in‑	qa-
2	a-	i-
3	u-	ki-
2.FORM	la (postverbal)	alaq (postverbal)

Set A (Ergative, prevocalic) — Lesson 8

Person	Singular	Plural
1	w-	q-
2	aw-	iw-
3	r-	k-
2.FORM	la (postverbal)	alaq (postverbal)

Alignment

The alignment is ergative-absolutive: Set B groups S and P together (both trigger the same paradigm), while A triggers a distinct paradigm (Set A). This contrasts with Mam, which shows morphologically tripartite alignment (S, A, and P each trigger distinct patterns; @cite{scott-2023}).

Formal address

K'iche' has two levels of formality for 2nd person: informal and formal. The formal forms (laal SG, alaq PL) are syntactically postverbal and do not participate in the prefix paradigm.

inductive Fragments.Mayan.Kiche.Person : Type

Grammatical person in K'iche'.

• first : Person
• second : Person
• third : Person

instance Fragments.Mayan.Kiche.instDecidableEqPerson : DecidableEq Person

Equations

• Fragments.Mayan.Kiche.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Mayan.Kiche.instBEqPerson : BEq Person

Equations

• Fragments.Mayan.Kiche.instBEqPerson = { beq := Fragments.Mayan.Kiche.instBEqPerson.beq }

def Fragments.Mayan.Kiche.instBEqPerson.beq : Person → Person → Bool

Equations

• Fragments.Mayan.Kiche.instBEqPerson.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kiche.instReprPerson : Repr Person

Equations

• Fragments.Mayan.Kiche.instReprPerson = { reprPrec := Fragments.Mayan.Kiche.instReprPerson.repr }

def Fragments.Mayan.Kiche.instReprPerson.repr : Person → Nat → Std.Format

Equations

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

inductive Fragments.Mayan.Kiche.Formality : Type

Formality level for 2nd person.

• informal : Formality
• formal : Formality

instance Fragments.Mayan.Kiche.instDecidableEqFormality : DecidableEq Formality

Equations

• Fragments.Mayan.Kiche.instDecidableEqFormality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Mayan.Kiche.instBEqFormality : BEq Formality

Equations

• Fragments.Mayan.Kiche.instBEqFormality = { beq := Fragments.Mayan.Kiche.instBEqFormality.beq }

def Fragments.Mayan.Kiche.instBEqFormality.beq : Formality → Formality → Bool

Equations

• Fragments.Mayan.Kiche.instBEqFormality.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kiche.instReprFormality : Repr Formality

Equations

• Fragments.Mayan.Kiche.instReprFormality = { reprPrec := Fragments.Mayan.Kiche.instReprFormality.repr }

def Fragments.Mayan.Kiche.instReprFormality.repr : Formality → Nat → Std.Format

Equations

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

structure Fragments.Mayan.Kiche.PhiFeatures : Type

A person/number/formality specification.

• person : Person
• number : Number
• formality : Formality

instance Fragments.Mayan.Kiche.instDecidableEqPhiFeatures : DecidableEq PhiFeatures

Equations

• Fragments.Mayan.Kiche.instDecidableEqPhiFeatures = Fragments.Mayan.Kiche.instDecidableEqPhiFeatures.decEq

def Fragments.Mayan.Kiche.instDecidableEqPhiFeatures.decEq (x✝ x✝¹ : PhiFeatures) : Decidable (x✝ = x✝¹)

Equations

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

instance Fragments.Mayan.Kiche.instBEqPhiFeatures : BEq PhiFeatures

Equations

• Fragments.Mayan.Kiche.instBEqPhiFeatures = { beq := Fragments.Mayan.Kiche.instBEqPhiFeatures.beq }

def Fragments.Mayan.Kiche.instBEqPhiFeatures.beq : PhiFeatures → PhiFeatures → Bool

Equations

• Fragments.Mayan.Kiche.instBEqPhiFeatures.beq { person := a, number := a_1, formality := a_2 } { person := b, number := b_1, formality := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Fragments.Mayan.Kiche.instBEqPhiFeatures.beq x✝¹ x✝ = false

instance Fragments.Mayan.Kiche.instReprPhiFeatures : Repr PhiFeatures

Equations

• Fragments.Mayan.Kiche.instReprPhiFeatures = { reprPrec := Fragments.Mayan.Kiche.instReprPhiFeatures.repr }

def Fragments.Mayan.Kiche.instReprPhiFeatures.repr : PhiFeatures → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Fragments.Mayan.Kiche.phi (p : Person) (n : Number) : PhiFeatures

Shorthand for informal phi features.

Equations

• Fragments.Mayan.Kiche.phi p n = { person := p, number := n, formality := Fragments.Mayan.Kiche.Formality.informal }

def Fragments.Mayan.Kiche.setBMarker : PhiFeatures → String

Set B (absolutive) agreement markers. These are verbal prefixes (or postverbal particles for formal forms) that cross-reference S (intransitive subject) and P (transitive object). @cite{mondloch-2017}, Lessons 9, 15.

Equations

• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.first, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "in-"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "at-"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.third, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "Ø"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.first, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "oj-"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "ix-"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.third, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "ee-"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.formal } = "la"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.formal } = "alaq"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.first, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "oj-"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.second, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "ix-"
• Fragments.Mayan.Kiche.setBMarker { person := Fragments.Mayan.Kiche.Person.third, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "ee-"
• Fragments.Mayan.Kiche.setBMarker { person := person, number := number, formality := Fragments.Mayan.Kiche.Formality.formal } = "Ø"

def Fragments.Mayan.Kiche.setAPreC : PhiFeatures → String

Set A (ergative) markers before consonant-initial roots. These cross-reference A (transitive subject) and are identical to possessive pronouns before consonant-initial nouns. @cite{mondloch-2017}, Lessons 7, 15.

Equations

• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.first, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "nu-/in-"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "a-"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.third, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "u-"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.first, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "qa-"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "i-"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.third, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "ki-"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.formal } = "la"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.formal } = "alaq"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.first, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "qa-"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.second, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "i-"
• Fragments.Mayan.Kiche.setAPreC { person := Fragments.Mayan.Kiche.Person.third, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "ki-"
• Fragments.Mayan.Kiche.setAPreC { person := person, number := number, formality := Fragments.Mayan.Kiche.Formality.formal } = "Ø"

def Fragments.Mayan.Kiche.setAPreV : PhiFeatures → String

Set A (ergative) markers before vowel-initial roots. @cite{mondloch-2017}, Lesson 8.

Equations

• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.first, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "w-"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "aw-"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.third, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "r-"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.first, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "q-"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "iw-"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.third, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "k-"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.formal } = "la"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.formal } = "alaq"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.first, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "q-"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.second, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "iw-"
• Fragments.Mayan.Kiche.setAPreV { person := Fragments.Mayan.Kiche.Person.third, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "k-"
• Fragments.Mayan.Kiche.setAPreV { person := person, number := number, formality := Fragments.Mayan.Kiche.Formality.formal } = "Ø"

def Fragments.Mayan.Kiche.setBIsPrefix (φ : PhiFeatures) : Bool

Is a Set B marker a prefix (appearing before the root) or a postverbal particle? Formal forms are postverbal; all others are prefixes. @cite{mondloch-2017}, Lesson 9.

Equations

• Fragments.Mayan.Kiche.setBIsPrefix φ = (φ.formality == Fragments.Mayan.Kiche.Formality.informal)

def Fragments.Mayan.Kiche.setAIsPrefix (φ : PhiFeatures) : Bool

Is a Set A marker a prefix or postverbal? Same distribution as Set B: formal forms are postverbal.

Equations

• Fragments.Mayan.Kiche.setAIsPrefix φ = (φ.formality == Fragments.Mayan.Kiche.Formality.informal)

inductive Fragments.Mayan.Kiche.KicheArgPosition : Type

Argument positions in a K'iche' clause.

• agent : KicheArgPosition
• patient : KicheArgPosition
• intranS : KicheArgPosition

instance Fragments.Mayan.Kiche.instDecidableEqKicheArgPosition : DecidableEq KicheArgPosition

Equations

• Fragments.Mayan.Kiche.instDecidableEqKicheArgPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mayan.Kiche.instBEqKicheArgPosition.beq : KicheArgPosition → KicheArgPosition → Bool

Equations

• Fragments.Mayan.Kiche.instBEqKicheArgPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kiche.instBEqKicheArgPosition : BEq KicheArgPosition

Equations

• Fragments.Mayan.Kiche.instBEqKicheArgPosition = { beq := Fragments.Mayan.Kiche.instBEqKicheArgPosition.beq }

instance Fragments.Mayan.Kiche.instReprKicheArgPosition : Repr KicheArgPosition

Equations

• Fragments.Mayan.Kiche.instReprKicheArgPosition = { reprPrec := Fragments.Mayan.Kiche.instReprKicheArgPosition.repr }

def Fragments.Mayan.Kiche.instReprKicheArgPosition.repr : KicheArgPosition → Nat → Std.Format

Equations

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

inductive Fragments.Mayan.Kiche.AgreementSet : Type

Which agreement set cross-references each argument position?

• setA : AgreementSet
• setB : AgreementSet

instance Fragments.Mayan.Kiche.instDecidableEqAgreementSet : DecidableEq AgreementSet

Equations

• Fragments.Mayan.Kiche.instDecidableEqAgreementSet x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mayan.Kiche.instBEqAgreementSet.beq : AgreementSet → AgreementSet → Bool

Equations

• Fragments.Mayan.Kiche.instBEqAgreementSet.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kiche.instBEqAgreementSet : BEq AgreementSet

Equations

• Fragments.Mayan.Kiche.instBEqAgreementSet = { beq := Fragments.Mayan.Kiche.instBEqAgreementSet.beq }

instance Fragments.Mayan.Kiche.instReprAgreementSet : Repr AgreementSet

Equations

• Fragments.Mayan.Kiche.instReprAgreementSet = { reprPrec := Fragments.Mayan.Kiche.instReprAgreementSet.repr }

def Fragments.Mayan.Kiche.instReprAgreementSet.repr : AgreementSet → Nat → Std.Format

Equations

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

def Fragments.Mayan.Kiche.KicheArgPosition.agreementSet : KicheArgPosition → AgreementSet

The agreement set triggered by each argument position. S and P both trigger Set B (= absolutive grouping). A triggers Set A (= ergative).

Equations

• Fragments.Mayan.Kiche.KicheArgPosition.agent.agreementSet = Fragments.Mayan.Kiche.AgreementSet.setA
• Fragments.Mayan.Kiche.KicheArgPosition.patient.agreementSet = Fragments.Mayan.Kiche.AgreementSet.setB
• Fragments.Mayan.Kiche.KicheArgPosition.intranS.agreementSet = Fragments.Mayan.Kiche.AgreementSet.setB

def Fragments.Mayan.Kiche.KicheArgPosition.case : KicheArgPosition → Core.Case

The case associated with each argument position.

Equations

• Fragments.Mayan.Kiche.KicheArgPosition.agent.case = Core.Case.erg
• Fragments.Mayan.Kiche.KicheArgPosition.patient.case = Core.Case.abs
• Fragments.Mayan.Kiche.KicheArgPosition.intranS.case = Core.Case.abs

theorem Fragments.Mayan.Kiche.ergative_absolutive_alignment : KicheArgPosition.intranS.agreementSet = KicheArgPosition.patient.agreementSet ∧ KicheArgPosition.agent.agreementSet ≠ KicheArgPosition.patient.agreementSet

K'iche' groups S and P together (both trigger Set B): ergative-absolutive alignment.

theorem Fragments.Mayan.Kiche.s_p_same_case : KicheArgPosition.intranS.case = KicheArgPosition.patient.case

S and P receive the same case (ABS).

theorem Fragments.Mayan.Kiche.a_different_case : KicheArgPosition.agent.case ≠ KicheArgPosition.intranS.case

A receives a different case (ERG) from S/P (ABS).

theorem Fragments.Mayan.Kiche.kiche_not_tripartite : KicheArgPosition.intranS.case = KicheArgPosition.patient.case

K'iche' alignment contrast with Mam: K'iche' is ergative-absolutive (S = P ≠ A), while Mam is tripartite (S ≠ A ≠ P, all three receive distinct cases). In K'iche', both P and S trigger Set B; in Mam, P triggers no agreement at all.

theorem Fragments.Mayan.Kiche.setB_1sg : setBMarker (phi Person.first Number.sg) = "in-"

1SG absolutive: in-

theorem Fragments.Mayan.Kiche.setB_2sg : setBMarker (phi Person.second Number.sg) = "at-"

2SG absolutive: at-

theorem Fragments.Mayan.Kiche.setB_3sg : setBMarker (phi Person.third Number.sg) = "Ø"

3SG absolutive: Ø

theorem Fragments.Mayan.Kiche.setB_1pl : setBMarker (phi Person.first Number.pl) = "oj-"

1PL absolutive: oj-

theorem Fragments.Mayan.Kiche.setB_2pl : setBMarker (phi Person.second Number.pl) = "ix-"

2PL absolutive: ix-

theorem Fragments.Mayan.Kiche.setB_3pl : setBMarker (phi Person.third Number.pl) = "ee-"

3PL absolutive: ee-

theorem Fragments.Mayan.Kiche.setB_2sg_form : setBMarker { person := Person.second, number := Number.sg, formality := Formality.formal } = "la"

2SG.FORM: la (postverbal)

theorem Fragments.Mayan.Kiche.setB_2pl_form : setBMarker { person := Person.second, number := Number.pl, formality := Formality.formal } = "alaq"

2PL.FORM: alaq (postverbal)

theorem Fragments.Mayan.Kiche.setA_1sg : setAPreC (phi Person.first Number.sg) = "nu-/in-"

1SG ergative (preC): nu‑ or in‑

theorem Fragments.Mayan.Kiche.setA_2sg : setAPreC (phi Person.second Number.sg) = "a-"

2SG ergative (preC): a-

theorem Fragments.Mayan.Kiche.setA_3sg : setAPreC (phi Person.third Number.sg) = "u-"

3SG ergative (preC): u-

theorem Fragments.Mayan.Kiche.setA_1pl : setAPreC (phi Person.first Number.pl) = "qa-"

1PL ergative (preC): qa-

theorem Fragments.Mayan.Kiche.setA_2pl : setAPreC (phi Person.second Number.pl) = "i-"

2PL ergative (preC): i-

theorem Fragments.Mayan.Kiche.setA_3pl : setAPreC (phi Person.third Number.pl) = "ki-"

3PL ergative (preC): ki-

theorem Fragments.Mayan.Kiche.setA_preV_1sg : setAPreV (phi Person.first Number.sg) = "w-"

1SG ergative (preV): w-

theorem Fragments.Mayan.Kiche.setA_preV_2sg : setAPreV (phi Person.second Number.sg) = "aw-"

2SG ergative (preV): aw-

theorem Fragments.Mayan.Kiche.setA_preV_3sg : setAPreV (phi Person.third Number.sg) = "r-"

3SG ergative (preV): r-

theorem Fragments.Mayan.Kiche.possessives_equal_setA : setAPreC (phi Person.first Number.pl) = "qa-" ∧ setAPreC (phi Person.second Number.sg) = "a-" ∧ setAPreC (phi Person.third Number.sg) = "u-" ∧ setAPreC (phi Person.third Number.pl) = "ki-"

Set A markers are identical to possessive pronouns: the transitive subject markers (Lesson 15) are the same forms as the possessive prefixes (Lessons 7–8). This is a hallmark of ergative-absolutive languages, where ERG agreement and possession share the same morphological paradigm. @cite{mondloch-2017}, Lesson 15 explicitly notes this identity.

theorem Fragments.Mayan.Kiche.setB_informal_prefix : setBIsPrefix (phi Person.first Number.sg) = true ∧ setBIsPrefix (phi Person.second Number.sg) = true ∧ setBIsPrefix (phi Person.third Number.sg) = true ∧ setBIsPrefix (phi Person.first Number.pl) = true ∧ setBIsPrefix (phi Person.second Number.pl) = true ∧ setBIsPrefix (phi Person.third Number.pl) = true

All informal Set B markers are prefixes.

theorem Fragments.Mayan.Kiche.setB_formal_postverbal : setBIsPrefix { person := Person.second, number := Number.sg, formality := Formality.formal } = false ∧ setBIsPrefix { person := Person.second, number := Number.pl, formality := Formality.formal } = false

Formal Set B markers are NOT prefixes (they're postverbal).

def Fragments.Mayan.Kiche.independentPronoun : PhiFeatures → String

Independent (free) personal pronouns. These are used in nonverbal sentences and as emphatic/contrastive pronouns in verbal sentences. @cite{mondloch-2017}, Lesson 4.

Equations

• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.first, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "in"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "at"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.third, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "are'"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.first, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "oj"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "ix"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.third, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "a're'"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.formal } = "laal"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.formal } = "alaq"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.first, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "oj"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.second, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "ix"
• Fragments.Mayan.Kiche.independentPronoun { person := Fragments.Mayan.Kiche.Person.third, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "a're'"
• Fragments.Mayan.Kiche.independentPronoun { person := person, number := number, formality := Fragments.Mayan.Kiche.Formality.formal } = "are'"

theorem Fragments.Mayan.Kiche.pronoun_setB_correspondence : independentPronoun (phi Person.first Number.sg) = "in" ∧ independentPronoun (phi Person.second Number.sg) = "at" ∧ independentPronoun (phi Person.first Number.pl) = "oj" ∧ independentPronoun (phi Person.second Number.pl) = "ix"

Independent pronouns correspond to Set B (absolutive) markers in form: 1SG in = Set B in-, 2SG at = Set B at-, etc. This is expected for an ergative language where the independent pronouns pattern with absolutive agreement.