Yorùbá Focus Particles @cite{aremu-2026}

@cite{biberauer-roberts-2014}

Focus-marking morphemes across Yorùbá dialects. Standard Yorùbá uses clause-initial ni for ex-situ focus; south-eastern dialects (Ìkálẹ̀, Oǹdó, Òkìtìpupa) use clause-final ín — giving opposite head directions for FocP within a single language family.

The head-direction contrast

• Standard Yorùbá: [FocP Foc(ni) [TP...]] — head-initial FocP
• Ìkálẹ̀: [FocP XP_F [TP...] Foc(ín)] — head-final FocP

The Ìkálẹ̀ pattern places a head-final FocP over a head-initial TP, creating an apparent FOFC violation.

In-situ focus

All dialects also permit in-situ focus, marked by high tone (H%) on the focused constituent without movement or a focus particle.

inductive Fragments.Yoruba.FocusParticles.Dialect : Type

Yorùbá dialect grouping relevant to focus marking.

• standard : Dialect
• ikale : Dialect
• ondo : Dialect
• okitipupa : Dialect

instance Fragments.Yoruba.FocusParticles.instDecidableEqDialect : DecidableEq Dialect

Equations

• Fragments.Yoruba.FocusParticles.instDecidableEqDialect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Yoruba.FocusParticles.instBEqDialect.beq : Dialect → Dialect → Bool

Equations

• Fragments.Yoruba.FocusParticles.instBEqDialect.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Yoruba.FocusParticles.instBEqDialect : BEq Dialect

Equations

• Fragments.Yoruba.FocusParticles.instBEqDialect = { beq := Fragments.Yoruba.FocusParticles.instBEqDialect.beq }

def Fragments.Yoruba.FocusParticles.instReprDialect.repr : Dialect → Nat → Std.Format

Equations

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

instance Fragments.Yoruba.FocusParticles.instReprDialect : Repr Dialect

Equations

• Fragments.Yoruba.FocusParticles.instReprDialect = { reprPrec := Fragments.Yoruba.FocusParticles.instReprDialect.repr }

inductive Fragments.Yoruba.FocusParticles.FocusStrategy : Type

How focus is realized.

• exSitu : FocusStrategy
• inSitu : FocusStrategy

instance Fragments.Yoruba.FocusParticles.instDecidableEqFocusStrategy : DecidableEq FocusStrategy

Equations

• Fragments.Yoruba.FocusParticles.instDecidableEqFocusStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Yoruba.FocusParticles.instBEqFocusStrategy.beq : FocusStrategy → FocusStrategy → Bool

Equations

• Fragments.Yoruba.FocusParticles.instBEqFocusStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Yoruba.FocusParticles.instBEqFocusStrategy : BEq FocusStrategy

Equations

• Fragments.Yoruba.FocusParticles.instBEqFocusStrategy = { beq := Fragments.Yoruba.FocusParticles.instBEqFocusStrategy.beq }

def Fragments.Yoruba.FocusParticles.instReprFocusStrategy.repr : FocusStrategy → Nat → Std.Format

Equations

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

instance Fragments.Yoruba.FocusParticles.instReprFocusStrategy : Repr FocusStrategy

Equations

• Fragments.Yoruba.FocusParticles.instReprFocusStrategy = { reprPrec := Fragments.Yoruba.FocusParticles.instReprFocusStrategy.repr }

structure Fragments.Yoruba.FocusParticles.FocusParticleEntry : Type

A Yorùbá focus particle lexical entry.

• form : String

  Surface form

• dialects : List Dialect

  Dialect(s) where this particle is attested

• headDir : HeadDirection

  Head direction of FocP when this particle is used

• strategy : FocusStrategy

  Focus strategy

• triggersMovement : Bool

  Does the focused XP move to Spec-FocP?

• requiredForSubjectFocus : Bool

  Whether subject focus requires this strategy (vs in-situ)

• note : String

  Notes

instance Fragments.Yoruba.FocusParticles.instReprFocusParticleEntry : Repr FocusParticleEntry

Equations

• Fragments.Yoruba.FocusParticles.instReprFocusParticleEntry = { reprPrec := Fragments.Yoruba.FocusParticles.instReprFocusParticleEntry.repr }

def Fragments.Yoruba.FocusParticles.instReprFocusParticleEntry.repr : FocusParticleEntry → Nat → Std.Format

Equations

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

def Fragments.Yoruba.FocusParticles.instBEqFocusParticleEntry.beq : FocusParticleEntry → FocusParticleEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Yoruba.FocusParticles.instBEqFocusParticleEntry.beq x✝¹ x✝ = false

instance Fragments.Yoruba.FocusParticles.instBEqFocusParticleEntry : BEq FocusParticleEntry

Equations

• Fragments.Yoruba.FocusParticles.instBEqFocusParticleEntry = { beq := Fragments.Yoruba.FocusParticles.instBEqFocusParticleEntry.beq }

def Fragments.Yoruba.FocusParticles.ni : FocusParticleEntry

Standard Yorùbá ni — clause-initial focus marker. "Olú ni ó ra ìwé" = "It is Olú that bought a book."

Equations

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

def Fragments.Yoruba.FocusParticles.in_ : FocusParticleEntry

Ìkálẹ̀ ín — clause-final focus marker. "Olú ó rà ìwé ín" = "It is Olú that bought a book." @cite{aremu-2026} ex. (5): head-final Foc⁰.

Equations

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

def Fragments.Yoruba.FocusParticles.allParticles : List FocusParticleEntry

Equations

• Fragments.Yoruba.FocusParticles.allParticles = [Fragments.Yoruba.FocusParticles.ni, Fragments.Yoruba.FocusParticles.in_]

theorem Fragments.Yoruba.FocusParticles.opposite_head_directions : ni.headDir ≠ in_.headDir

The two particles have opposite head directions.

theorem Fragments.Yoruba.FocusParticles.both_trigger_movement : (allParticles.all fun (x : FocusParticleEntry) => x.triggersMovement) = true

Both particles trigger movement to Spec-FocP.

theorem Fragments.Yoruba.FocusParticles.both_required_for_subject : (allParticles.all fun (x : FocusParticleEntry) => x.requiredForSubjectFocus) = true

Both particles are required for subject focus.

theorem Fragments.Yoruba.FocusParticles.standard_head_initial : ni.headDir = HeadDirection.headInitial

Standard Yorùbá uses head-initial FocP.

theorem Fragments.Yoruba.FocusParticles.ikale_head_final : in_.headDir = HeadDirection.headFinal

Ìkálẹ̀ uses head-final FocP.