Documentation

Linglib.Fragments.Mayan.Kaqchikel.Agreement

Kaqchikel Agreement Fragment #

Typological metadata for Kaqchikel (K'ichean, Mayan) agreement morphology, following [Pre14]: paradigm exponents, person-number cells, and argument positions.

Kaqchikel cross-references both transitive arguments. Set A (ERG) prefixes index the transitive agent; Set B (ABS) pre-stem markers index the absolutive argument (transitive patient or intransitive S); morpheme order is aspect–ABS–ERG–stem, so Set B precedes Set A ([Pre14] (12)). In Agent Focus constructions the two slots collapse to a single marker drawn from the Set B paradigm.

Main declarations #

Implementation notes #

Hosting Set A on Voice/v and Set B on Infl/T follows the standard high-abs analysis (consistent with [Pre14] and [CMPP14]). Kaqchikel indexes every core argument, in contrast with San Juan Atitán Mam, where Infl's φ-probe is blocked in transitives and the patient goes unagreed ([Sco23]; see Mam/Agreement.lean) — the non-differential/differential pair consumed by Studies/Aissen2003Agreement.lean. The AF agreement table ([Pre14] §3.2, table (22)) and the choice rule that predicts it live in Studies/Preminger2014.lean. The non-perfective accCase records [Ima14]'s analysis of the progressive ajin construction — an analysis, not consensus typology; the derivation lives with Mayan.accCaseKaqchikel in Fragments/Mayan/Params.lean. Parenthesized exponent segments drop in certain phonological contexts. Person-number cells come from the canonical Agreement.Cell (Syntax/Agreement/Paradigm.lean).

ABS position (HIGH-ABS) #

source
def Kaqchikel.absPosition :
Mayan.ABSPosition

HIGH-ABS: the absolutive markers sit between the aspect marker and the stem.

Equations
Instances For

    Set A (ERG) exponents #

    source
    def Kaqchikel.setAExponent :
    Mayan.ExponentTable

    Set A (ERG) markers ([Pre14] table (29)).

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

      Set B (ABS) exponents #

      source
      def Kaqchikel.setBExponent :
      Mayan.ExponentTable

      Set B (ABS) markers; ∅ 3SG doubles as the Elsewhere default ([Pre14] table (29), Ch. 5).

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

        Argument positions #

        source
        @[reducible, inline]
        abbrev Kaqchikel.ArgPosition :
        Type

        Argument positions, aliased to the canonical Features.Prominence.ArgumentRole (S/A/P/R/T).

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Kaqchikel.ArgPosition.case :
          ArgPosition → Case

          Perfective (ergative) case assignment: Mayan.ergCaseKaqchikel (A → ERG, S/P → ABS).

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Kaqchikel.ArgPosition.accCase :
            ArgPosition → Case

            Non-perfective (PROG ajin) case assignment: Mayan.accCaseKaqchikel (S/A → ABS, P → ERG/GEN, per [Ima14]).

            Equations
            Instances For
              source
              def Kaqchikel.ArgPosition.IsPhiAgreed :
              ArgPosition → Prop

              Every position triggers φ-agreement — Kaqchikel is non-differential (contrast Mam.ArgPosition.IsPhiAgreed); R/T default to participating.

              Equations
              Instances For
                source
                @[implicit_reducible]
                instance Kaqchikel.instDecidablePredArgPositionIsPhiAgreed :
                DecidablePred ArgPosition.IsPhiAgreed
                Equations

                Verification: argument positions #

                Each fact below re-exports its Alignment.ergative lemma; the family-level statement is CoonMateoPedroPreminger2014.mayan_perfective_ergative.

                source
                theorem Kaqchikel.A_case :
                ArgPosition.case Features.Prominence.ArgumentRole.A = Case.erg

                Agent gets ERG (from Voice).

                source
                theorem Kaqchikel.P_case :
                ArgPosition.case Features.Prominence.ArgumentRole.P = Case.abs

                Patient gets ABS (from Infl).

                source
                theorem Kaqchikel.S_case :
                ArgPosition.case Features.Prominence.ArgumentRole.S = Case.abs

                Intransitive S gets ABS (from Infl).

                source
                theorem Kaqchikel.erg_abs_alignment :
                ArgPosition.case Features.Prominence.ArgumentRole.A ≠ ArgPosition.case Features.Prominence.ArgumentRole.P ∧ ArgPosition.case Features.Prominence.ArgumentRole.P = ArgPosition.case Features.Prominence.ArgumentRole.S

                Ergative-absolutive alignment: the agent is distinguished (ERG) while patient and intranS share a case value (ABS).

                source
                theorem Kaqchikel.all_positions_agreed (p : ArgPosition) :
                p ∈ Features.Prominence.ArgumentRole.core → p.IsPhiAgreed

                All core argument positions trigger φ-agreement.

                Case inventory ([Bla94b]) #

                source
                def Kaqchikel.caseInventory :
                Finset Case

                The case inventory realized by the core positions: {ERG, ABS}.

                Equations
                Instances For
                  source
                  theorem Kaqchikel.inventory_covers_positions (p : Features.Prominence.ArgumentRole) :
                  p ∈ Features.Prominence.ArgumentRole.core → ArgPosition.case p ∈ caseInventory

                  The inventory covers all argument positions: every position's case is in the inventory.