Category of QUD Partitions

Category of QUD (Question Under Discussion) partitions over a fixed type M, with refinement witnesses as morphisms.

This is a thin category (at most one morphism between any two objects): refinement is a preorder on partitions, and all refinement proofs between the same QUDs are equal by proof irrelevance.

QUD.refines_refl and QUD.refines_trans from Partition.lean provide the categorical identity and composition.

structure Core.Categorical.BundledQUD (M : Type u_1) : Type u_1

Bundled QUD: an object in the partition category for a fixed meaning type.

• qud : QUD M

  The underlying QUD partition.

def Core.Categorical.QUDHom {M : Type u_1} (q q' : BundledQUD M) : Type

Hom type for the QUD category: a refinement witness lifted to Type.

QUD.refines is Prop-valued; PLift promotes it to Type 0 so it can serve as a CategoryTheory.Category hom type. The category is thin (at most one morphism between any two objects).

Equations

• Core.Categorical.QUDHom q q' = PLift (q.qud.refines q'.qud)

instance Core.Categorical.instSubsingletonQUDHom {M : Type u_1} {q q' : BundledQUD M} : Subsingleton (QUDHom q q')

QUDHom is proof-irrelevant: at most one morphism between any two objects.

instance Core.Categorical.instCategoryBundledQUD (M : Type u_1) : CategoryTheory.Category.{0, u_1} (BundledQUD M)

Equations

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

def Core.Categorical.QUDHom.toTrivial {M : Type u_1} (q : BundledQUD M) : QUDHom q { qud := QUD.trivial }

The trivial partition is terminal: every QUD refines it.

Equations

• Core.Categorical.QUDHom.toTrivial q = { down := ⋯ }

def Core.Categorical.QUDHom.composeLeft {M : Type u_1} (q₁ q₂ : BundledQUD M) : QUDHom { qud := q₁.qud * q₂.qud } q₁

Compose of two QUDs refines the left factor.

Equations

• Core.Categorical.QUDHom.composeLeft q₁ q₂ = { down := ⋯ }