Q'anjob'al Agent Focus and Extraction Fragment

Morphological data on Q'anjob'al (Q'anjob'alan, Mayan) extraction asymmetries, Agent Focus, and the Crazy Antipassive, following [CMPP14]. Q'anjob'al shows an extraction asymmetry: the intransitive subject (S) and transitive object (P) extract freely, but the transitive subject (A) cannot be extracted without Agent Focus. Agent Focus replaces the regular transitive form with a verb bearing the AF suffix -on, the intransitive status suffix -i (not transitive -V'), and no Set A agreement — used for wh-questions, focus, and relativization targeting the agent.

Main declarations

• Qanjobal.StatusSuffix with .form: the ITV and TV status suffixes.
• Qanjobal.VerbMorphology with regularTransitive, agentFocusForm: the AF-suffix, status-suffix, and Set A properties of a verb form.
• Qanjobal.VerbMorphology.toMayanVerbForm: projection to the pan-Mayan Mayan.VerbForm for cross-Mayan typology.
• Qanjobal.crazyAntipassiveForm: the Crazy Antipassive, morphologically identical to Agent Focus.
• Qanjobal.PersonRestriction with .requiresAF, .requiresCrazyAP: the 3rd-person restriction on Agent Focus.
• Qanjobal.Extraction.realize: the AF-based extraction marking, with Qanjobal.Extraction.strategy as the WALS-style label.

Implementation notes

Q'anjob'al head-marks two agreement paradigms on the predicate: Set A (ERG) prefixes with pre-consonantal and pre-vocalic allomorphs, and Set B (ABS) suffixes with null 3rd person (∅); the tables live in Qanjobal/Agreement.lean. The verb stem's final suffix encodes transitivity (intransitive ITV -i, transitive TV -V') and surfaces only phrase-finally. Morpheme order is ASP-ABS-ERG-ROOT-(DERIV)-SUFFIX, with the absolutive immediately after the aspect marker (pre-stem), confirming Q'anjob'al as HIGH-ABS. In Agent Focus, absolutive agreement co-indexes the notional object rather than the subject. The Crazy Antipassive reuses the same -on morpheme in non-finite embedded transitives (where Infl⁰ is absent), analyzed as the same case-assigning mechanism. Tables and examples cite [CMPP14] tables (13) and (14).

Status suffixes

inductive Qanjobal.StatusSuffix : Type

Verb status suffixes encode transitivity. Surface only phrase-finally.

• itv : StatusSuffix
• tv : StatusSuffix

@[implicit_reducible]

instance Qanjobal.instDecidableEqStatusSuffix : DecidableEq StatusSuffix

Equations

• Qanjobal.instDecidableEqStatusSuffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Qanjobal.instReprStatusSuffix : Repr StatusSuffix

Equations

• Qanjobal.instReprStatusSuffix = { reprPrec := Qanjobal.instReprStatusSuffix.repr }

def Qanjobal.instReprStatusSuffix.repr : StatusSuffix → ℕ → Std.Format

Equations

• Qanjobal.instReprStatusSuffix.repr Qanjobal.StatusSuffix.itv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Qanjobal.StatusSuffix.itv")).group prec✝
• Qanjobal.instReprStatusSuffix.repr Qanjobal.StatusSuffix.tv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Qanjobal.StatusSuffix.tv")).group prec✝

def Qanjobal.StatusSuffix.form : StatusSuffix → String

Equations

• Qanjobal.StatusSuffix.itv.form = "-i"
• Qanjobal.StatusSuffix.tv.form = "-V'"

Agent Focus construction

structure Qanjobal.VerbMorphology : Type

Morphological properties of a Q'anjob'al verb form.

• hasAFSuffix : Bool

  Does the verb bear the AF suffix -on?

• statusSuffix : StatusSuffix

  Which status suffix: ITV or TV?

• hasSetA : Bool

  Does the verb bear Set A (ergative) agreement?

@[implicit_reducible]

instance Qanjobal.instDecidableEqVerbMorphology : DecidableEq VerbMorphology

Equations

• Qanjobal.instDecidableEqVerbMorphology = Qanjobal.instDecidableEqVerbMorphology.decEq

def Qanjobal.instDecidableEqVerbMorphology.decEq (x✝ x✝¹ : VerbMorphology) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Qanjobal.instReprVerbMorphology : Repr VerbMorphology

Equations

• Qanjobal.instReprVerbMorphology = { reprPrec := Qanjobal.instReprVerbMorphology.repr }

def Qanjobal.instReprVerbMorphology.repr : VerbMorphology → ℕ → Std.Format

Equations

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

def Qanjobal.regularTransitive : VerbMorphology

Regular transitive verb form.

Equations

• Qanjobal.regularTransitive = { hasAFSuffix := false, statusSuffix := Qanjobal.StatusSuffix.tv, hasSetA := true }

def Qanjobal.agentFocusForm : VerbMorphology

Agent Focus verb form.

Equations

• Qanjobal.agentFocusForm = { hasAFSuffix := true, statusSuffix := Qanjobal.StatusSuffix.itv, hasSetA := false }

theorem Qanjobal.af_has_itv_suffix : agentFocusForm.statusSuffix = StatusSuffix.itv

AF carries the intransitive status suffix -i, not -V'. This is the morphological reflex of AF Voice being non-phasal (intransitive v⁰). Despite the clause having two non-oblique core arguments, the verb's status suffix signals intransitivity.

theorem Qanjobal.af_no_set_a : agentFocusForm.hasSetA = false

AF lacks Set A (ergative) agreement.

theorem Qanjobal.trans_has_set_a : regularTransitive.hasSetA = true

Regular transitives have Set A agreement.

def Qanjobal.VerbMorphology.permitsAgentExtraction (v : VerbMorphology) : Bool

Can the agent be extracted with this verb form?

Equations

• v.permitsAgentExtraction = v.hasAFSuffix

theorem Qanjobal.af_permits_extraction : agentFocusForm.permitsAgentExtraction = true ∧ regularTransitive.permitsAgentExtraction = false

AF permits agent extraction; regular transitive does not.

def Qanjobal.VerbMorphology.toMayanVerbForm (v : VerbMorphology) : Mayan.VerbForm

Project VerbMorphology down to the pan-Mayan Mayan.VerbForm for cross-Mayan typology; the hasAFSuffix flag discriminates AF form from transitive.

Equations

• v.toMayanVerbForm = if v.hasAFSuffix = true then Mayan.VerbForm.agentFocus else Mayan.VerbForm.transitive

theorem Qanjobal.toMayanVerbForm_canonical : agentFocusForm.toMayanVerbForm = Mayan.VerbForm.agentFocus ∧ regularTransitive.toMayanVerbForm = Mayan.VerbForm.transitive

AF morphology projects to .agentFocus; regular transitive to .transitive.

theorem Qanjobal.hasSetA_consistent_with_projection : agentFocusForm.toMayanVerbForm.hasSetA = agentFocusForm.hasSetA ∧ regularTransitive.toMayanVerbForm.hasSetA = regularTransitive.hasSetA

Cross-Mayan consistency: Q'anjob'al's AF form lacks Set A under both the language-internal hasSetA field and the projected Mayan.VerbForm.hasSetA predicate.

Crazy Antipassive

def Qanjobal.crazyAntipassiveForm : VerbMorphology

The Crazy Antipassive uses the same -on morpheme as AF, but in non-finite embedded transitives rather than extraction contexts. Both carry the intransitive status suffix -i.

Chi uj [hin y-il-on-i] ix Malin 'Maria can see me.' Lanan [hach hin-laq'-on-i] 'I am hugging you.'

Equations

• Qanjobal.crazyAntipassiveForm = { hasAFSuffix := true, statusSuffix := Qanjobal.StatusSuffix.itv, hasSetA := false }

theorem Qanjobal.crazy_ap_is_af_form : crazyAntipassiveForm = agentFocusForm

The Crazy Antipassive is morphologically identical to AF.

Person restriction on Agent Focus

inductive Qanjobal.PersonRestriction : Type

In Q'anjob'al, AF is restricted to clauses with 3rd person agents. 1st and 2nd person agents use the regular transitive form even when focused or extracted. Compare (72a-b) of [CMPP14]:

• 3rd person: A Juan max maq'-on[-i] no tx'i'. (AF required)
• 1st person: Ay-in max hin-maq'[-a'] no tx'i'. (regular transitive)

The tentative account: 1st/2nd person agents may be base-generated in a high clausal position (Spec,CP), so no extraction through the vP phase edge is needed — the trapping problem never arises.

• first : PersonRestriction
• second : PersonRestriction
• third : PersonRestriction

@[implicit_reducible]

instance Qanjobal.instDecidableEqPersonRestriction : DecidableEq PersonRestriction

Equations

• Qanjobal.instDecidableEqPersonRestriction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Qanjobal.instReprPersonRestriction.repr : PersonRestriction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Qanjobal.instReprPersonRestriction : Repr PersonRestriction

Equations

• Qanjobal.instReprPersonRestriction = { reprPrec := Qanjobal.instReprPersonRestriction.repr }

def Qanjobal.PersonRestriction.requiresAF : PersonRestriction → Bool

Does AF apply for this person of agent? Only 3rd person.

Equations

• Qanjobal.PersonRestriction.first.requiresAF = false
• Qanjobal.PersonRestriction.second.requiresAF = false
• Qanjobal.PersonRestriction.third.requiresAF = true

theorem Qanjobal.af_only_third_person : PersonRestriction.third.requiresAF = true ∧ PersonRestriction.first.requiresAF = false ∧ PersonRestriction.second.requiresAF = false

def Qanjobal.PersonRestriction.requiresCrazyAP (_p : PersonRestriction) : Bool

The Crazy Antipassive does NOT have this person restriction: it appears with all persons in non-finite embedded transitives. This is expected because the Crazy Antipassive is triggered by the absence of Infl⁰ (a property of the embedded clause), not by extraction through a phase edge.

Equations

• _p.requiresCrazyAP = true

theorem Qanjobal.crazy_ap_all_persons : PersonRestriction.first.requiresCrazyAP = true ∧ PersonRestriction.second.requiresCrazyAP = true ∧ PersonRestriction.third.requiresCrazyAP = true

Extraction marking

inductive Qanjobal.Extraction.Site : Type

Reflex hosts for Q'anjob'al extraction marking.

• verb : Site

@[implicit_reducible]

instance Qanjobal.Extraction.instDecidableEqSite : DecidableEq Site

Equations

• Qanjobal.Extraction.instDecidableEqSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Qanjobal.Extraction.instReprSite.repr : Site → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Qanjobal.Extraction.instReprSite : Repr Site

Equations

• Qanjobal.Extraction.instReprSite = { reprPrec := Qanjobal.Extraction.instReprSite.repr }

def Qanjobal.Extraction.realize : Extraction.ExtractionTarget → List (Features.Reflex Site)

3rd-person agent (subject) extraction switches the verb to AF (the suffix -on, [CMPP14]); nothing else is marked.

Equations

• Qanjobal.Extraction.realize Extraction.ExtractionTarget.subject = [Features.Reflex.morpheme Qanjobal.Extraction.Site.verb]
• Qanjobal.Extraction.realize x✝ = []

def Qanjobal.Extraction.strategy : Extraction.ExtractionMarkingStrategy

WALS-style label: a dedicated morpheme marks extraction.

Equations

• Qanjobal.Extraction.strategy = Extraction.ExtractionMarkingStrategy.dedicatedMorpheme