Symbol Reference: Type — Kind of Types / Conglomerates (Predicates on Classes)

Type \(\mathsf{Type}\) — Kind of Types / Conglomerates (Predicates on Classes)

The kind of all types T : Type. Semantically, each type in Type corresponds to a conglomerate (a predicate on the conglomerate of all classes).

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	Type \(\mathsf{Type}\)
Category	Foundational Types & Sorts
SML AST Constructor	`Kernel AST Symbol / Sort Constructor in typetheory.ML (Class_p / Truth_p / EXP / UCol)`
Constructor Arguments	Typed arguments as specified by the Signature / Sort field above
Metatype / Signature	`Super-Kind of Types`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathsf{Type}`
How to Understand It	How to Understand `Type` in MKTD1 & MKTD2: In our foundational setting, terms are classes and types are conglomerates (predicates on classes). When an entry quantifies over `(A : Type)` or a type family `(B : A → Type)` (Entries DefClassConditional (3.22)–DefTightClass (3.47)): `A : Type` ranges over conglomerate predicates on classes (including `Class`, `Bool`, `Prop`, dependent product types `Π(x:A). B(x)`, and dependent sum types `Σ(x:A). B(x)`). `B : A → Type` is an `A`-indexed family of conglomerates (dependent type family).
Canonical Law / Usage	`∀(A:Type). ∀(B:(A → Type)). Type`
Related Symbols & Kernel Entries	Default Domain Type Class Propositions Prop and Booleans Bool Definition DefSigmaModel (3.38): “Dependent Sum (Sigma-Type)” model over a family Theorem DefPiPredicateModel (3.39): “Dependent Product (Pi-Type)” predicate and section model