Documentation

Linglib.Fragments.Mayan.Tseltalan

Shared Tseltalan Infrastructure #

@cite{aissen-polian-2025} @cite{polian-2013}

Descriptive types shared across the Tseltalan subgroup (Tsotsil, Tseltal). Both languages share agreement paradigm assignment and grammatical function classification. They differ in agreement exponents and Set B marker position (Tsotsil: prefixal/suffixal; Tseltal: consistently suffixal).

Agreement System (Table 1 of @cite{aissen-polian-2025}) #

FormFunctionTseltalTsotsil
Set AA, Psrprefixalprefixal
Set BS and Osuffixalprefixal/suffixal
source
inductive Fragments.Mayan.Tseltalan.GramFunction :
Type

Grammatical functions in Tseltalan, determining which agreement marker set cross-references each argument.

These are traditional Mayanist descriptive categories (footnote 9 of @cite{aissen-polian-2025}).

FunctionMarker Set
A (transitive subject)Set A
S_A (agentive intransitive subject)Set B
S_O (patientive intransitive subj)Set B
O (transitive/ditransitive object)Set B
G (applied argument)Set B
Possessor (genitive)Set A
Instances For
    source
    @[implicit_reducible]
    instance Fragments.Mayan.Tseltalan.instDecidableEqGramFunction :
    DecidableEq GramFunction
    Equations
    source
    def Fragments.Mayan.Tseltalan.instReprGramFunction.repr :
    GramFunction → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Fragments.Mayan.Tseltalan.instReprGramFunction :
      Repr GramFunction
      Equations
      source
      def Fragments.Mayan.Tseltalan.GramFunction.markerSet :
      GramFunction → MarkerSet

      The marker set that cross-references each grammatical function. Set A = ergative/genitive; Set B = absolutive. Shared across Tseltalan (@cite{aissen-polian-2025}, @cite{polian-2013}).

      Equations
      Instances For
        source
        theorem Fragments.Mayan.Tseltalan.erg_gen_homophonous :
        GramFunction.A.markerSet = GramFunction.psr.markerSet

        Ergative-genitive homophony: Set A cross-references both transitive agents and possessors. A pan-Mayan pattern.

        source
        theorem Fragments.Mayan.Tseltalan.abs_uniform :
        GramFunction.S_A.markerSet = MarkerSet.setB ∧ GramFunction.S_O.markerSet = MarkerSet.setB ∧ GramFunction.O.markerSet = MarkerSet.setB ∧ GramFunction.G.markerSet = MarkerSet.setB

        All absolutive arguments (S_A, S_O, O, G) use Set B.

        source
        def Fragments.Mayan.Tseltalan.absPosition :
        ABSPosition

        Tseltalan absolutive morphemes appear in low (post-stem) position. Both Tsotsil and Tseltal share this LOW-ABS classification — see Fragments.Mayan.Tsotsil.absPosition and Fragments.Mayan.Tseltal.absPosition for the per-language definitions, which are definitionally equal to this subgroup-level constant. The LOW-ABS classification refers to the structural position of the licensing head, not the linear position of every Set B exponent (which varies by language and context). @cite{aissen-polian-2025} p. 97; @cite{polian-2013}.

        Equations
        Instances For
          source
          def Fragments.Mayan.Tseltalan.GramFunction.toArgumentRole? :
          GramFunction → Option Features.Prominence.ArgumentRole

          Project the Tseltalan-specific Split-S grammatical function down to the canonical pan-linguistic ArgumentRole (S/A/P/R/T) used across linglib. The projection is partial (Option-valued):

          • .A → .A, .O → .P, .G → .R: verbal arguments map cleanly.
          • .S_A, .S_O → .S: agentivity distinction is collapsed (lossy but expected for cross-Mayan typology theorems that don't track Split-S granularity).
          • .psr → none: possessors are DP-internal, with no ArgumentRole analog. Cross-Mayan typology theorems quantify over verbal arguments only.

          Tseltal/Tsotsil consumers of cross-Mayan theorems use this projection to feed Tseltalan agreement data into the canonical inventory; the Aissen-Polian possessor-extraction analysis continues to use GramFunction directly for its DP-internal claims.

          Equations
          Instances For