The case-bearing capability

HasCase equips a carrier with the grammatical case it bears; HasCase.Compatible is the induced case-concord relation, slot compatibility in the flat information order: symmetric NP-internal agreement in case, not the asymmetric government/assignment by which case enters an NP (Syntax/Case/Dependent.lean, Syntax/Case/Licensing.lean). Case is a non-canonical agreement feature ([Cor06]); [Bla94b]'s treatment of assignment and concord is the typological anchor. The carrier is single-valued, so syncretism, case-stacking, and coordinate case resolution are out of scope.

class HasCase (α : Type u_1) : Type u_1

A carrier of grammatical case. ⊥ = the carrier does not mark case.

• caseOf : α → Flat Case

  The case value the carrier bears, if marked.

@[instance_reducible]

instance instHasCaseMorphFeatures : HasCase UD.MorphFeatures

Equations

• instHasCaseMorphFeatures = { caseOf := fun (mf : UD.MorphFeatures) => Option.map Case.fromUD mf.case_ }

@[instance_reducible]

instance instHasCaseCase : HasCase Case

Equations

• instHasCaseCase = { caseOf := fun (x : Case) => ↑x }

@[instance_reducible]

instance instHasCaseOptionCase : HasCase (Option Case)

Option Case is the free case-bearer: some c bears c, none is caseless.

Equations

• instHasCaseOptionCase = { caseOf := id }

@[reducible, inline]

abbrev HasCase.Compatible {α : Type u_1} {β : Type u_2} [HasCase α] [HasCase β] (a : α) (b : β) : Prop

Case compatibility (concord): valued cases coincide, an unvalued carrier is a wildcard.

Equations

• HasCase.Compatible a b = Compat (caseOf a) (caseOf b)

theorem UD.MorphFeatures.compatible_hasCase {f1 f2 : MorphFeatures} (h : f1.compatible f2 = true) : HasCase.Compatible f1 f2

φ-compatibility of UD bundles entails case compatibility.