Higher kinds, packages, and self-representation

Constructors have kinds generated by $\mathsf{Ty}$ and arrows. They include variables, $\mathbb{N}$, arrows, products, universal and existential constructors, constructor abstraction, and constructor application. The terms of chapter 9 are the annotated $F_{\omega }$ term forms, products, and naturals. Chapter 10 conservatively adds existential pack and unpack.

Constructor equality is the congruence generated by constructor beta. Constructor reduction is compatible under every constructor former. Pure term call-by-value has term beta, type beta, and projection roots. The package extension adds value-package opening. Compatible term beta is a separate relation used for logical relations. Constructor equality is not record width subtyping.

Kinding is unique, constructor reduction is strongly normalizing and confluent, and constructor equality is equality of normal forms by lemma 7.9, theorem 7.21, theorem 7.23, theorem 7.25. Hence constructor conversion is decidable and has the head-injectivity facts of corollary 7.26. Fully annotated term checking is syntax directed modulo that decision; no Curry-style reconstruction or principal-inference result is claimed.

Canonical forms for the package-free grammar are given in lemma 11.36. Preservation, progress, and safety are theorem 11.37, theorem 11.38, corollary 11.39. The term context is empty in progress and safety; the constructor context may remain open.

Package substitution, preservation, progress, and safety are proved in lemma 7.33, theorem 7.38, theorem 7.39, corollary 7.40. The higher-kind abstraction theorem and existential counter representation independence are theorem 7.48, theorem 7.51.

Typed self-representation is developed in the explicitly restricted pure $F_{\omega }$ fragment. Strong shallow and deep unquotation and the three inspection folds are theorem 7.60, theorem 7.68, theorem 7.70, theorem 7.71, theorem 7.74; the diagonal application remains untypable by proposition 7.57.

No executable artifact is used as evidence for kinding normalization, package safety, representation independence, dictionary coherence, or typed self-representation.