Shawi Agreement Fragment @cite{clem-deal-2024}

Shawi (Chayahuita; ISO 639-3: cbt; Glottocode: chay1248) is a Kawapanan language spoken in Peru. The data formalized here are based on @cite{clem-deal-2024}, drawing on the corpus and descriptive work of Bourdeau (2015), Barraza de García (2005), Hart (1988), and Ulloa (in preparation).

What this fragment captures (theory-neutral)

• Subject and object agreement paradigms as suffix tables (@cite{clem-deal-2024} Tables 1–2). Number is "minimal/augmented", following Ulloa's treatment of the system; we abbreviate as min and aug (≈ singular/plural for non-inclusive persons).
• Ergative case marker -ri, attaching to some transitive subjects (@cite{clem-deal-2024} (4)).
• "Object agreement on subject" (OAgr-on-S) morpheme, the suffix doubling object φ-features on the subject right after -ri (@cite{clem-deal-2024} (12), (32)). It uses the same forms as ordinary object agreement, hence reuses objectMarkers.
• 3rd-person object syntactic position (high vs low) as a binary parameter that any analysis of the optional -ri with 3rd-person objects must consume (@cite{clem-deal-2024} §3.2 around (30)).
• External object syntax (overt-postverbal vs. fronted vs. pro-dropped). Paper (9), (21): when -ri surfaces, the object cannot remain overt-postverbal — it must be either fronted (OSV) or pro-dropped.

This file imports only Core/. All theoretical analysis — the mapping of ergative distribution to a particular Agree configuration — lives in Phenomena/Agreement/Studies/ClemDeal2024.lean.

inductive Fragments.Kawapanan.Shawi.Number : Type

Shawi uses a minimal/augmented number system rather than singular/plural; 1INCL "minimal" picks out the speaker+hearer dyad, etc. (@cite{clem-deal-2024} fn. 4, after Corbett 2000). For non-inclusive persons min/aug correspond closely to singular/plural.

• min : Number
• aug : Number

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instDecidableEqNumber : DecidableEq Number

Equations

• Fragments.Kawapanan.Shawi.instDecidableEqNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instReprNumber : Repr Number

Equations

• Fragments.Kawapanan.Shawi.instReprNumber = { reprPrec := Fragments.Kawapanan.Shawi.instReprNumber.repr }

def Fragments.Kawapanan.Shawi.instReprNumber.repr : Number → ℕ → Std.Format

Equations

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

inductive Fragments.Kawapanan.Shawi.Clusivity : Type

Inclusivity dimension orthogonal to PersonLevel; only relevant for 1st person (1INCL vs 1EXCL).

• excl : Clusivity
• incl : Clusivity
• na : Clusivity

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instDecidableEqClusivity : DecidableEq Clusivity

Equations

• Fragments.Kawapanan.Shawi.instDecidableEqClusivity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instReprClusivity : Repr Clusivity

Equations

• Fragments.Kawapanan.Shawi.instReprClusivity = { reprPrec := Fragments.Kawapanan.Shawi.instReprClusivity.repr }

def Fragments.Kawapanan.Shawi.instReprClusivity.repr : Clusivity → ℕ → Std.Format

Equations

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

structure Fragments.Kawapanan.Shawi.Phi : Type

A φ-feature bundle for a Shawi argument. Field order matches the subjectMarkers / objectMarkers row layout: person, clusivity, number.

• person : Features.Prominence.PersonLevel
• clusivity : Clusivity
• number : Number

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instDecidableEqPhi : DecidableEq Phi

Equations

• Fragments.Kawapanan.Shawi.instDecidableEqPhi = Fragments.Kawapanan.Shawi.instDecidableEqPhi.decEq

def Fragments.Kawapanan.Shawi.instDecidableEqPhi.decEq (x✝ x✝¹ : Phi) : Decidable (x✝ = x✝¹)

Equations

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

def Fragments.Kawapanan.Shawi.instReprPhi.repr : Phi → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instReprPhi : Repr Phi

Equations

• Fragments.Kawapanan.Shawi.instReprPhi = { reprPrec := Fragments.Kawapanan.Shawi.instReprPhi.repr }

def Fragments.Kawapanan.Shawi.subjectMarkers : List (Features.Prominence.PersonLevel × Clusivity × Number × Option String)

Subject agreement suffixes, indicative mood (@cite{clem-deal-2024} Table 1, after Hart 1988, Barraza de García 2005, Ulloa to appear). Glottal stop is written '; optional (a) reflects source variation.

Equations

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

def Fragments.Kawapanan.Shawi.objectMarkers : List (Features.Prominence.PersonLevel × Clusivity × Number × Option String)

Object agreement suffixes (@cite{clem-deal-2024} Table 2). 3rd person objects show no overt agreement (∅); we encode this directly with none rather than an empty-string sentinel.

Equations

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

def Fragments.Kawapanan.Shawi.lookupMarker (paradigm : List (Features.Prominence.PersonLevel × Clusivity × Number × Option String)) (φ : Phi) : Option String

Lookup an agreement suffix; returns none if the row is absent or the cell itself is null (3rd-person object).

Equations

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

def Fragments.Kawapanan.Shawi.subjectMarker (φ : Phi) : Option String

Equations

• Fragments.Kawapanan.Shawi.subjectMarker φ = Fragments.Kawapanan.Shawi.lookupMarker Fragments.Kawapanan.Shawi.subjectMarkers φ

def Fragments.Kawapanan.Shawi.objectMarker (φ : Phi) : Option String

Equations

• Fragments.Kawapanan.Shawi.objectMarker φ = Fragments.Kawapanan.Shawi.lookupMarker Fragments.Kawapanan.Shawi.objectMarkers φ

def Fragments.Kawapanan.Shawi.ergativeMarker : String

The ergative case suffix (@cite{clem-deal-2024} (4)). Attaches to some transitive subjects; the -(*ri) notation in the paper indicates that the form is -ri when present and ungrammatical when absent in the relevant configurations.

Equations

• Fragments.Kawapanan.Shawi.ergativeMarker = "-ri"

def Fragments.Kawapanan.Shawi.oagrOnSMarker (objectPhi : Phi) : Option String

"Object agreement on subject" exponent, doubling the object's φ on the subject immediately after -ri (@cite{clem-deal-2024} (12), (32)). Reuses the object-agreement paradigm.

Equations

• Fragments.Kawapanan.Shawi.oagrOnSMarker objectPhi = Fragments.Kawapanan.Shawi.objectMarker objectPhi

inductive Fragments.Kawapanan.Shawi.ObjectPosition : Type

Position of an object inside the vP (@cite{clem-deal-2024} §3.2, (30)). low = inside the inner v_cat phase, invisible to the v probe; high = outside the inner phase (Spec,v_cat or higher), visible.

• low : ObjectPosition
• high : ObjectPosition

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instDecidableEqObjectPosition : DecidableEq ObjectPosition

Equations

• Fragments.Kawapanan.Shawi.instDecidableEqObjectPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Kawapanan.Shawi.instReprObjectPosition.repr : ObjectPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instReprObjectPosition : Repr ObjectPosition

Equations

• Fragments.Kawapanan.Shawi.instReprObjectPosition = { reprPrec := Fragments.Kawapanan.Shawi.instReprObjectPosition.repr }

def Fragments.Kawapanan.Shawi.mustBeHigh : Features.Prominence.PersonLevel → Bool

Local-person (1/2) objects obligatorily move to the high position (@cite{clem-deal-2024} §3.2). 3rd-person objects may but need not.

Equations

• Fragments.Kawapanan.Shawi.mustBeHigh Features.Prominence.PersonLevel.first = true
• Fragments.Kawapanan.Shawi.mustBeHigh Features.Prominence.PersonLevel.second = true
• Fragments.Kawapanan.Shawi.mustBeHigh Features.Prominence.PersonLevel.third = false

inductive Fragments.Kawapanan.Shawi.ObjectSyntax : Type

External-syntax options for an object in a transitive clause. The surface order is determined by which option is realized: overt-postverbal corresponds to canonical SVO; fronted to OSV; pro-dropped to subject-only surface form (@cite{clem-deal-2024} (9), (20)–(21), (26)).

• overtPostverbal : ObjectSyntax
• overtFronted : ObjectSyntax
• proDropped : ObjectSyntax

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instDecidableEqObjectSyntax : DecidableEq ObjectSyntax

Equations

• Fragments.Kawapanan.Shawi.instDecidableEqObjectSyntax x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Kawapanan.Shawi.instReprObjectSyntax : Repr ObjectSyntax

Equations

• Fragments.Kawapanan.Shawi.instReprObjectSyntax = { reprPrec := Fragments.Kawapanan.Shawi.instReprObjectSyntax.repr }

def Fragments.Kawapanan.Shawi.instReprObjectSyntax.repr : ObjectSyntax → ℕ → Std.Format

Equations

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

def Fragments.Kawapanan.Shawi.objectSyntaxLicit (subjBearsErg : Bool) : ObjectSyntax → Bool

When the subject bears -ri, the object cannot remain overt-postverbal: it must be either fronted (OSV) or pro-dropped (@cite{clem-deal-2024} (9), (21)). When the subject does not bear -ri, all three options are available.

Equations

• Fragments.Kawapanan.Shawi.objectSyntaxLicit subjBearsErg Fragments.Kawapanan.Shawi.ObjectSyntax.overtPostverbal = !subjBearsErg
• Fragments.Kawapanan.Shawi.objectSyntaxLicit subjBearsErg Fragments.Kawapanan.Shawi.ObjectSyntax.overtFronted = true
• Fragments.Kawapanan.Shawi.objectSyntaxLicit subjBearsErg Fragments.Kawapanan.Shawi.ObjectSyntax.proDropped = true

def Fragments.Kawapanan.Shawi.caseInventory : Finset Core.Case

Shawi's morphological case inventory: nominative (unmarked) and ergative (-ri). No accusative; objects are unmarked.

Equations

• Fragments.Kawapanan.Shawi.caseInventory = {UD.Case.nom, UD.Case.erg}