inductive PropertyKindCalculus.Specializes (E : KindOfProperty → KindOfProperty → Prop) : KindOfProperty → KindOfProperty → Prop

Reflexive–transitive closure of a direct-parent edge relation E.

• refl {E : KindOfProperty → KindOfProperty → Prop} (a : KindOfProperty) : Specializes E a a

  Reflexivity of the closure: every kind specializes itself.

• step {E : KindOfProperty → KindOfProperty → Prop} {a b c : KindOfProperty} : E a b → Specializes E b c → Specializes E a c

  Prepend a direct-parent edge E a b to a specialization b ⊑ c.

theorem PropertyKindCalculus.Specializes.of_edge {E : KindOfProperty → KindOfProperty → Prop} {a b : KindOfProperty} (h : E a b) : Specializes E a b

A single parent edge specializes.

theorem PropertyKindCalculus.Specializes.trans {E : KindOfProperty → KindOfProperty → Prop} {a b c : KindOfProperty} (h₁ : Specializes E a b) (h₂ : Specializes E b c) : Specializes E a c

Specialization is transitive (it is a preorder, together with refl).

def PropertyKindCalculus.MutuallyComparable (E : KindOfProperty → KindOfProperty → Prop) (a b : KindOfProperty) : Prop

Dybkær §6 / VIM4 2CD 1.2 (quantities of the same kind) — two kinds are mutually comparable (belong to one broad kind) iff they share a common super-kind. This is how width and height remain comparable as lengths even though they are distinct sub-kinds.

Equations

• PropertyKindCalculus.MutuallyComparable E a b = ∃ (p : PropertyKindCalculus.KindOfProperty), PropertyKindCalculus.Specializes E a p ∧ PropertyKindCalculus.Specializes E b p

theorem PropertyKindCalculus.MutuallyComparable.refl {E : KindOfProperty → KindOfProperty → Prop} (a : KindOfProperty) : MutuallyComparable E a a

theorem PropertyKindCalculus.MutuallyComparable.symm {E : KindOfProperty → KindOfProperty → Prop} {a b : KindOfProperty} (h : MutuallyComparable E a b) : MutuallyComparable E b a

theorem PropertyKindCalculus.MutuallyComparable.of_specializes {E : KindOfProperty → KindOfProperty → Prop} {a b : KindOfProperty} (h : Specializes E a b) : MutuallyComparable E a b

If a specializes b, they are mutually comparable (witness b).