Typed Knowledge over Constructive Institutions
Hans-Martin Will
cs.LO
Nov 5, 2026 · v1
cs.AI cs.DB
TL;DR
The type-theory metatheory (consistency, conversion, NbE, bidirectional checking) is formalized in Lean 4, with an appendix mapping each definition and theorem to the code.
Abstract
Type theories designed for mathematics or program verification need only that a proposition holds; proof irrelevance in conversion erases, at the kernel level, how a claim was established. A persistent knowledge store, by contrast, must retain that record: who established a claim, by which derivation or external tool, and under which assumptions. This volume 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 cumulative universes, an impredicative universe of propositions, inductive families, and an intensional identity type. Proof irrelevance is an axiom with an explicit witness rather than a conversion rule, so proofs of a proposition are provably equal yet remain distinct terms. Definitional equality is joinability under an orthogonal rewriting system—confluent, injective on type formers, and decidable by a type-free test—while a separate subsumption judgment covers universe cumulativity, codomain-covariant function types, and declared class inclusions. We prove consistency via a set-theoretic model; develop a justification logic over the kernel's propositions to track evidence and support; organize environments as an institution so that store extensions are signature morphisms and external verdicts enter via comorphisms; formulate a typed knowledge-graph theory with records, classes, and refinements; and prove the correctness of conversion, normalization by evaluation, and bidirectional type checking relative to termination. A Lean 4 formalization accompanies the volume.
Problem
A persistent knowledge store must record how a claim was established: by whom, by which derivation or tool, and under which assumptions. Type theories whose conversion builds in proof irrelevance erase this information at the kernel level.
Approach
Defines a dependent type theory with cumulative universes, an impredicative Prop, inductive families, and an intensional identity type. Proof irrelevance is an explicit axiom rather than a conversion rule, and a separate subsumption judgment handles universe cumulativity and class inclusions. Builds on this kernel a justification logic, an institution-theoretic organization of environments, and a typed knowledge-graph theory, and proves correctness of the conversion, normalization-by-evaluation, and bidirectional type-checking algorithms. The results are formalized in Lean 4.
Results
Proves consistency via a set-theoretic model and proves the decision algorithms correct relative to termination of reduction. The Lean 4 formalization is published at github.com/eigenius/theory, and an appendix maps the volume's results to it.
