Kaqchikel Agent Focus Fragment @cite{erlewine-2016}

Empirical data and Minimalist infrastructure for Agent Focus (AF) in Kaqchikel, a K'ichean (Mayan) language. When the transitive agent is Ā-extracted clause-locally, the verb obligatorily appears in a special AF form: Set A (ergative) agreement is lost and the suffix -Vn appears.

The Paradigm

Extracted arg	Verb form	Agreement
None (declarative)	Transitive	Set A + Set B
Patient/Abs	Transitive	Set A + Set B
Agent/Erg (local)	AF (-Vn)	Set B only
Agent/Erg (long)	Transitive	Set A + Set B

AF is obligatory for clause-local agent extraction and ungrammatical for patient extraction or long-distance agent extraction — it is not a free alternation but a locality-sensitive, structurally conditioned repair.

Clause Structures

Both derivations share the same clausal spine (CP > TP > vP > VP). The difference is in the v head and the agent's movement path:

1. Normal transitive: Transitive v introduces agent in Spec,vP. A-probe on T attracts agent to Spec,TP, establishing Set A (ergative) agreement. For Ā-extraction, agent must then move from Spec,TP to Spec,CP — but this violates SSAL because CP immediately dominates TP.

2. AF structure: Intransitive-like v does NOT introduce agent in Spec,vP. Agent extracts directly to Spec,CP without passing through Spec,TP. This satisfies SSAL (no too-local step), but skipping Spec,TP means no A-agreement — hence no Set A, and AF morphology (-Vn) surfaces.

The grammar selects AF as optimal via OT competition (§5): SSAL >> XRef means avoiding the too-local movement outranks maintaining cross-referencing agreement.

inductive Fragments.Mayan.Kaqchikel.VerbForm : Type

Verbal morphology in a Kaqchikel clause: either the normal transitive form (with Set A ergative agreement) or Agent Focus (with -Vn and no Set A).

• transitive : VerbForm

  Normal transitive: Set A (erg) + Set B (abs) agreement.

• agentFocus : VerbForm

  Agent Focus: suffix -Vn, Set B only, no Set A (erg).

instance Fragments.Mayan.Kaqchikel.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

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

def Fragments.Mayan.Kaqchikel.instBEqVerbForm.beq : VerbForm → VerbForm → Bool

Equations

• Fragments.Mayan.Kaqchikel.instBEqVerbForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kaqchikel.instBEqVerbForm : BEq VerbForm

Equations

• Fragments.Mayan.Kaqchikel.instBEqVerbForm = { beq := Fragments.Mayan.Kaqchikel.instBEqVerbForm.beq }

def Fragments.Mayan.Kaqchikel.instReprVerbForm.repr : VerbForm → ℕ → Std.Format

Equations

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

instance Fragments.Mayan.Kaqchikel.instReprVerbForm : Repr VerbForm

Equations

• Fragments.Mayan.Kaqchikel.instReprVerbForm = { reprPrec := Fragments.Mayan.Kaqchikel.instReprVerbForm.repr }

def Fragments.Mayan.Kaqchikel.VerbForm.hasSetA : VerbForm → Bool

Does this verb form bear ergative (Set A) agreement?

Equations

• Fragments.Mayan.Kaqchikel.VerbForm.transitive.hasSetA = true
• Fragments.Mayan.Kaqchikel.VerbForm.agentFocus.hasSetA = false

def Fragments.Mayan.Kaqchikel.VerbForm.hasAFSuffix : VerbForm → Bool

Does this verb form bear the AF suffix -Vn?

Equations

• Fragments.Mayan.Kaqchikel.VerbForm.transitive.hasAFSuffix = false
• Fragments.Mayan.Kaqchikel.VerbForm.agentFocus.hasAFSuffix = true

structure Fragments.Mayan.Kaqchikel.ExtractionDatum : Type

An extraction datum: which argument is extracted and which verb form surfaces.

• extracted : Interfaces.ArgumentRole
• verbForm : VerbForm
• judgment : Interfaces.ExtractionMarkingStrategy

instance Fragments.Mayan.Kaqchikel.instReprExtractionDatum : Repr ExtractionDatum

Equations

• Fragments.Mayan.Kaqchikel.instReprExtractionDatum = { reprPrec := Fragments.Mayan.Kaqchikel.instReprExtractionDatum.repr }

def Fragments.Mayan.Kaqchikel.instReprExtractionDatum.repr : ExtractionDatum → ℕ → Std.Format

Equations

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

def Fragments.Mayan.Kaqchikel.agentExtractionAF : ExtractionDatum

Agent extraction (clause-local) requires AF.

Equations

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

def Fragments.Mayan.Kaqchikel.agentExtractionTrans : ExtractionDatum

Agent extraction with normal transitive (clause-local) is ungrammatical.

Equations

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

def Fragments.Mayan.Kaqchikel.patientExtractionTrans : ExtractionDatum

Patient extraction uses normal transitive.

Equations

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

def Fragments.Mayan.Kaqchikel.longDistanceAgentExtraction : ExtractionDatum

Long-distance agent extraction uses normal transitive, NOT AF. When the agent extracts from an embedded clause, it passes through intermediate Spec,CP positions via successive-cyclic movement. Each step crosses enough structure to satisfy SSAL — the too-local Spec,TP → Spec,CP step within the embedded clause is avoided.

This is the key evidence that AF is triggered by locality of movement, not simply by agent extraction (@cite{erlewine-2016}, §2.3, examples 21–22).

Equations

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

inductive Fragments.Mayan.Kaqchikel.AFCandidate : Type

A candidate derivation for clause-local transitive agent extraction.

The OT competition evaluates these: which structure best satisfies the ranked constraints? Both candidates share the same clausal spine (CP > TP > vP > VP); they differ in the v head and the agent's movement path.

• transitiveExtraction : AFCandidate

  Normal transitive derivation: transitive v introduces agent in Spec,vP. A-probe on T attracts agent to Spec,TP (triggering Set A agreement). Subsequent Ā-extraction from Spec,TP to Spec,CP violates SSAL because CP immediately dominates TP.

• agentFocusExtraction : AFCandidate

  Agent Focus derivation: intransitive-like v, agent NOT in Spec,vP. Agent extracts directly to Spec,CP without passing through Spec,TP. No SSAL violation, but cross-referencing is incomplete: no Set A (ergative) agreement because the agent never enters Spec,TP.

instance Fragments.Mayan.Kaqchikel.instDecidableEqAFCandidate : DecidableEq AFCandidate

Equations

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

def Fragments.Mayan.Kaqchikel.instBEqAFCandidate.beq : AFCandidate → AFCandidate → Bool

Equations

• Fragments.Mayan.Kaqchikel.instBEqAFCandidate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kaqchikel.instBEqAFCandidate : BEq AFCandidate

Equations

• Fragments.Mayan.Kaqchikel.instBEqAFCandidate = { beq := Fragments.Mayan.Kaqchikel.instBEqAFCandidate.beq }

def Fragments.Mayan.Kaqchikel.instReprAFCandidate.repr : AFCandidate → ℕ → Std.Format

Equations

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

instance Fragments.Mayan.Kaqchikel.instReprAFCandidate : Repr AFCandidate

Equations

• Fragments.Mayan.Kaqchikel.instReprAFCandidate = { reprPrec := Fragments.Mayan.Kaqchikel.instReprAFCandidate.repr }

def Fragments.Mayan.Kaqchikel.AFCandidate.verbForm : AFCandidate → VerbForm

The verb form that surfaces for each candidate.

Equations

• Fragments.Mayan.Kaqchikel.AFCandidate.transitiveExtraction.verbForm = Fragments.Mayan.Kaqchikel.VerbForm.transitive
• Fragments.Mayan.Kaqchikel.AFCandidate.agentFocusExtraction.verbForm = Fragments.Mayan.Kaqchikel.VerbForm.agentFocus

def Fragments.Mayan.Kaqchikel.AFCandidate.violatesAntiLocality : AFCandidate → Bool

Does this candidate violate Spec-to-Spec Anti-Locality (SSAL)? The transitive derivation does: the step Spec,TP → Spec,CP crosses no intervening maximal projection (CP immediately dominates TP).

Equations

• Fragments.Mayan.Kaqchikel.AFCandidate.transitiveExtraction.violatesAntiLocality = true
• Fragments.Mayan.Kaqchikel.AFCandidate.agentFocusExtraction.violatesAntiLocality = false

def Fragments.Mayan.Kaqchikel.AFCandidate.violatesXRef : AFCandidate → Bool

Does this candidate violate the XRef (cross-referencing) constraint? AF loses Set A agreement because the agent never enters Spec,TP where the A-probe resides. The transitive candidate maintains full cross-referencing (Set A + Set B).

Equations

• Fragments.Mayan.Kaqchikel.AFCandidate.transitiveExtraction.violatesXRef = false
• Fragments.Mayan.Kaqchikel.AFCandidate.agentFocusExtraction.violatesXRef = true

inductive Fragments.Mayan.Kaqchikel.AFConstraint : Type

Constraints for Kaqchikel AF, ranked from highest to lowest:

1. SSAL (highest): Spec-to-Spec Anti-Locality. Movement from Spec,XP to Spec,YP is banned when YP immediately dominates XP.
2. XRef (lower): Cross-referencing agreement. Every argument DP must be cross-referenced by a pronominal morpheme on the verb (Set A for ergative, Set B for absolutive).

SSAL dominates XRef: it is better to lose agreement (AF) than to violate anti-locality (crash).

• antiLocality : AFConstraint
• xref : AFConstraint

instance Fragments.Mayan.Kaqchikel.instDecidableEqAFConstraint : DecidableEq AFConstraint

Equations

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

instance Fragments.Mayan.Kaqchikel.instBEqAFConstraint : BEq AFConstraint

Equations

• Fragments.Mayan.Kaqchikel.instBEqAFConstraint = { beq := Fragments.Mayan.Kaqchikel.instBEqAFConstraint.beq }

def Fragments.Mayan.Kaqchikel.instBEqAFConstraint.beq : AFConstraint → AFConstraint → Bool

Equations

• Fragments.Mayan.Kaqchikel.instBEqAFConstraint.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Kaqchikel.instReprAFConstraint : Repr AFConstraint

Equations

• Fragments.Mayan.Kaqchikel.instReprAFConstraint = { reprPrec := Fragments.Mayan.Kaqchikel.instReprAFConstraint.repr }

def Fragments.Mayan.Kaqchikel.instReprAFConstraint.repr : AFConstraint → ℕ → Std.Format

Equations

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

def Fragments.Mayan.Kaqchikel.AFCandidate.violations : AFCandidate → List ℕ

Violation profile for each candidate.

Position 0 = highest-ranked constraint (SSAL / AntiLocality). Position 1 = lower-ranked constraint (XRef).

• Transitive extraction: [1, 0] — violates SSAL, satisfies XRef
• AF extraction: [0, 1] — satisfies SSAL, violates XRef

Equations

• Fragments.Mayan.Kaqchikel.AFCandidate.transitiveExtraction.violations = [1, 0]
• Fragments.Mayan.Kaqchikel.AFCandidate.agentFocusExtraction.violations = [0, 1]

def Fragments.Mayan.Kaqchikel.agentExtractionTableau : Core.ConstraintEvaluation.OTTableau AFCandidate

The OT tableau for Kaqchikel clause-local agent extraction.

Equations

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

def Fragments.Mayan.Kaqchikel.kaqClauseSpine : Minimalism.ClauseSpine

Both the transitive and AF derivations project the same clausal spine (CP > TP > vP > VP). The difference is in the v head: transitive v introduces the agent in Spec,vP; AF v does not.

Equations

• Fragments.Mayan.Kaqchikel.kaqClauseSpine = Minimalism.ClauseSpine.cP

def Fragments.Mayan.Kaqchikel.kaqVoice : Minimalism.VoiceHead

Kaqchikel agentive Voice/v head (parallel to Mam's Voice). Present in the transitive derivation; absent or altered in AF.

Equations

• Fragments.Mayan.Kaqchikel.kaqVoice = { flavor := Minimalism.VoiceFlavor.agentive, hasD := true, phaseHead := true }

def Fragments.Mayan.Kaqchikel.kaqExtractionProfile : Interfaces.ExtractionProfile

Kaqchikel's extraction morphology profile: agent focus alternation.

Equations

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

inductive Fragments.Mayan.Kaqchikel.MayanAFType : Type

Mayan languages vary in whether AF is available, depending on the ranking of SSAL vs XRef. This produces a two-way typological split:

• AF languages: SSAL >> XRef. Anti-locality violation is repaired by switching to AF morphology. E.g., Kaqchikel, Q'anjob'al.
• Extraction-gap languages: XRef >> SSAL. No AF repair available; clause-local agent extraction is simply ungrammatical. E.g., Chol.

Both types share the same underlying problem (SSAL blocks clause-local agent extraction); they differ only in whether the grammar provides a repair strategy.

• afLanguage : MayanAFType

  SSAL >> XRef: AF available as repair for anti-locality.

• extractionGap : MayanAFType

  XRef >> SSAL: no repair; extraction gap.

instance Fragments.Mayan.Kaqchikel.instDecidableEqMayanAFType : DecidableEq MayanAFType

Equations

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

instance Fragments.Mayan.Kaqchikel.instBEqMayanAFType : BEq MayanAFType

Equations

• Fragments.Mayan.Kaqchikel.instBEqMayanAFType = { beq := Fragments.Mayan.Kaqchikel.instBEqMayanAFType.beq }

def Fragments.Mayan.Kaqchikel.instBEqMayanAFType.beq : MayanAFType → MayanAFType → Bool

Equations

• Fragments.Mayan.Kaqchikel.instBEqMayanAFType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Mayan.Kaqchikel.instReprMayanAFType.repr : MayanAFType → ℕ → Std.Format

Equations

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

instance Fragments.Mayan.Kaqchikel.instReprMayanAFType : Repr MayanAFType

Equations

• Fragments.Mayan.Kaqchikel.instReprMayanAFType = { reprPrec := Fragments.Mayan.Kaqchikel.instReprMayanAFType.repr }

def Fragments.Mayan.Kaqchikel.kaqAFType : MayanAFType

Kaqchikel is an AF language (SSAL >> XRef).

Equations

• Fragments.Mayan.Kaqchikel.kaqAFType = Fragments.Mayan.Kaqchikel.MayanAFType.afLanguage

theorem Fragments.Mayan.Kaqchikel.af_no_set_a : VerbForm.agentFocus.hasSetA = false

AF does not bear Set A (ergative) agreement.

theorem Fragments.Mayan.Kaqchikel.trans_has_set_a : VerbForm.transitive.hasSetA = true

Normal transitive does bear Set A agreement.

theorem Fragments.Mayan.Kaqchikel.af_has_suffix : VerbForm.agentFocus.hasAFSuffix = true

AF bears the -Vn suffix.

theorem Fragments.Mayan.Kaqchikel.candidates_differ : AFCandidate.transitiveExtraction.violations ≠ AFCandidate.agentFocusExtraction.violations

The two candidates have different violation profiles.

theorem Fragments.Mayan.Kaqchikel.trans_violates_antilocality : AFCandidate.transitiveExtraction.violatesAntiLocality = true

The transitive derivation violates SSAL.

theorem Fragments.Mayan.Kaqchikel.af_obeys_antilocality : AFCandidate.agentFocusExtraction.violatesAntiLocality = false

The AF derivation does NOT violate SSAL.

theorem Fragments.Mayan.Kaqchikel.af_is_optimal : agentExtractionTableau.optimal = [AFCandidate.agentFocusExtraction]

AF is lexicographically optimal: it satisfies the higher-ranked constraint (SSAL) at the cost of the lower-ranked one (XRef). This is the central result of @cite{erlewine-2016}.

theorem Fragments.Mayan.Kaqchikel.satisfaction_ordering_incomparable : agentExtractionTableau.satOptimal = []

Under satisfaction ordering (subset inclusion), the two candidates would be incomparable — each satisfies a constraint the other violates. OT's strict ranking is what breaks the tie in favor of AF.

theorem Fragments.Mayan.Kaqchikel.kaq_has_voice : kaqClauseSpine.projects Minimalism.Cat.Voice = true

Kaqchikel clause projects Voice.

theorem Fragments.Mayan.Kaqchikel.kaq_voice_is_agentive : kaqVoice.flavor = Minimalism.VoiceFlavor.agentive

Kaqchikel Voice is agentive and a phase head.

theorem Fragments.Mayan.Kaqchikel.af_locality_sensitive : agentExtractionAF.verbForm = VerbForm.agentFocus ∧ longDistanceAgentExtraction.verbForm = VerbForm.transitive

AF is locality-sensitive: clause-local agent extraction triggers AF, but long-distance agent extraction does NOT. The paper's deepest empirical claim: AF is about the locality of movement, not about agent extraction per se.

def Fragments.Mayan.Kaqchikel.kaqVoiceSystem : Interfaces.VoiceSystemProfile

Kaqchikel voice system: two-way asymmetrical (transitive/AF).

Not a true pivot system — AF is a locality-sensitive repair for clause-local agent extraction, not a symmetric voice alternation. Transitive is the basic form; AF is derived (triggered by SSAL).

Equations

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

theorem Fragments.Mayan.Kaqchikel.kaq_voice_system_asymmetrical : kaqVoiceSystem.symmetry = Interfaces.VoiceSystemSymmetry.asymmetrical

theorem Fragments.Mayan.Kaqchikel.kaq_voice_count : kaqVoiceSystem.voiceCount = 2

theorem Fragments.Mayan.Kaqchikel.kaq_both_promote_agent : (kaqVoiceSystem.voices.all fun (x : Interfaces.VoiceEntry) => x.promotes == Interfaces.PivotTarget.agent) = true

Both Kaqchikel voices promote agent — AF is not a patient-promoting voice but an alternative agent-extracting structure.

theorem Fragments.Mayan.Kaqchikel.kaq_not_active_passive : kaqVoiceSystem.isActivePassive = false

Kaqchikel is NOT an active/passive system: it lacks a patient-promoting voice.