The φ-bundle capability

HasPhi equips a carrier with its agreement features as an Agreement.Bundle; HasPhi.Agree is the induced agreement relation, compatibility of the bundles, an unspecified dimension acting as a wildcard.

class HasPhi (α : Type u_1) : Type u_1

A φ-bearer is an expression that exposes its agreement features as a bundle.

• phi : α → Agreement.Bundle

  The agreement features.

@[instance_reducible]

instance instHasPhiBundle : HasPhi Agreement.Bundle

A bundle bears itself.

Equations

• instHasPhiBundle = { phi := id }

@[instance_reducible]

instance instHasPhiFeatures : HasPhi Morphology.Features

A token's features bear their agreement dimensions.

Equations

• instHasPhiFeatures = { phi := Agreement.Bundle.ofFeatures }

def HasPhi.Agree {α : Type u_1} {β : Type u_2} [HasPhi α] [HasPhi β] (a : α) (b : β) : Prop

Two φ-bearers agree when their bundles are compatible, an unspecified dimension acting as a wildcard.

Equations

• HasPhi.Agree a b = Compat (phi a) (phi b)

@[instance_reducible]

instance instDecidableAgree {α : Type u_1} {β : Type u_2} [HasPhi α] [HasPhi β] (a : α) (b : β) : Decidable (HasPhi.Agree a b)

Equations

• instDecidableAgree a b = id inferInstance