Typed Knowledge over Constructive Institutions

Type theories designed as foundations for mathematics or for program verification need only that a proposition holds, and a theory with proof irrelevance in conversion erases, at the kernel, how it was established. A persistent knowledge store must keep that: who established a claim, by which derivation or external tool, and under which assumptions. This book, the first volume of a series on Eigenius, presents the theory of Eigenius, a store of typed knowledge over constructive institutions, and develops its metatheory from that requirement. The kernel theory is a dependent type theory with a cumulative universe hierarchy, an impredicative universe of propositions, inductive families with recursors, and an intensional identity type. It departs from the theories of current proof assistants in two ways. Proof irrelevance is a provable fact with a witness and not a rule of conversion, so that proofs of one proposition are provably equal and remain distinct terms. Definitional equality is joinability under an orthogonal rewriting system, so that it is confluent, injective on type formers, and decidable by a type-free test, and a subsumption judgment, separate from it, covers universe cumulativity, function types covariant in their codomains, and declared class inclusions. The metatheory is developed in five parts. A set-theoretic model that interprets terms directly proves consistency, relative to one obligation on the global environment, for two bidirectional fragments that the kernel implements and, by translation, for the declarative theory. A justification logic over the kernel's propositions records evidence with its support. The theory of an environment is organized as an institution, so that an extension of the store is a signature morphism and a verdict obtained in another system enters as a sentence of a comorphism. A typed knowledge-graph theory with record types and width subtyping gives the store its classes, resources, and refinements. The procedures that decide the bidirectional fragments, conversion by reduction to weak-head normal form and normalization by evaluation, are stated with their correctness relative to the termination of reduction. A Lean 4 formalization accompanies the theory, and an appendix maps it to the definitions and results. The later volumes of the series treat the implementation, the language pipeline, and the system.