Typed Knowledge over Constructive Institutions

Hans-Martin Will

cs.LONov 5, 2026

Typed Knowledge over Constructive Institutions

Authors: Hans-Martin Will

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.

Figures & tables

\frac{}{\cdot\ \mathsf{ctx}}\quad\textsc{right={C-Empty}}\frac{\Gamma\vdash A:\mathrm{Sort}\,\ell\quad x\notin\mathrm{dom}(\Gamma)}{\Gamma,x{:}A\ \mathsf{ctx}}\quad\textsc{right={C-Ext}}\frac{\Gamma\ \mathsf{ctx}\quad(x{:}A)\in\Gamma}{\Gamma\vdash x:A}\quad\textsc{right={Var}}\frac{\Gamma\vdash a:A\quad A\equiv B\quad\Gamma\vdash B:\mathrm{Sort}\,\ell}{\Gamma\vdash a:B}\quad\textsc{right={Conv}}\frac{\Gamma\vdash a:A\quad\Gamma\vdash A\leq B\quad\Gamma\vdash B:\mathrm{Sort}\,\ell}{\Gamma\vdash a:B}\quad\textsc{right={Sub}}

Figure 1: Contexts, variables, conversion, and subsumption.

Connective	Type	Universe of the type
$P\to Q$	$\Pi x{:}P.\,Q$ , $x\notin\mathrm{FV}(Q)$	$\mathrm{Prop}$
$\forall x{:}A.\,P$	$\Pi x{:}A.\,P$	$\mathrm{Prop}$ , for every $A$ (impredicativity)
$P\wedge Q$	$\Sigma x{:}P.\,Q$ , $x\notin\mathrm{FV}(Q)$	$\mathrm{Prop}$
$\exists x{:}A.\,P$	$\mathsf{Exists}\,A\,(\lambda x{:}A.\,P)$ , inductive	$\mathrm{Prop}$
$P\vee Q$	$\mathsf{Or}\,P\,Q$ , inductive	$\mathrm{Prop}$
$\bot$	$\mathsf{False}$ , inductive without constructors	$\mathrm{Prop}$

Table 1: The propositional connectives as types.

\frac{\Gamma\vdash A:\mathrm{Sort}\,\ell_{1}\quad\Gamma,x{:}A\vdash B:\mathrm{Sort}\,\ell_{2}}{\Gamma\vdash\Pi x{:}A.\,B:\mathrm{Sort}\,(\mathsf{imax}\,\ell_{1}\,\ell_{2})}\quad\textsc{right={

\Pi

-F}}\frac{\Gamma,x{:}A\vdash b:B}{\Gamma\vdash\lambda x{:}A.\,b:\Pi x{:}A.\,B}\quad\textsc{right={

\Pi

-I}}\frac{\Gamma\vdash f:\Pi x{:}A.\,B\quad\Gamma\vdash a:A}{\Gamma\vdash f\,a:B[a/x]}\quad\textsc{right={

\Pi

-E}}\\ \frac{}{(\lambda x{:}A.\,b)\,a\longrightarrow b[a/x]}\quad\textsc{right={

\Pi

-

\beta

}}\\ \frac{\Gamma\vdash A:\mathrm{Sort}\,\ell_{1}\quad\Gamma,x{:}A\vdash B:\mathrm{Sort}\,\ell_{2}}{\Gamma\vdash\Sigma x{:}A.\,B:\mathrm{Sort}\,(\mathsf{max}\,\ell_{1}\,\ell_{2})}\quad\textsc{right={

\Sigma

-F}}\frac{\Gamma\vdash a:A\quad\Gamma\vdash b:B[a/x]\quad\Gamma,x{:}A\vdash B:\mathrm{Sort}\,\ell}{\Gamma\vdash\langle a,b\rangle:\Sigma x{:}A.\,B}\quad\textsc{right={

\Sigma

-I}}\\ \frac{\Gamma\vdash p:\Sigma x{:}A.\,B}{\Gamma\vdash\mathsf{fst}\,p:A}\quad\textsc{right={

\Sigma

-E

{}{1} $}}\frac{\Gamma\vdash p:\Sigma x{:}A.\,B}{\Gamma\vdash\mathsf{snd}\,p:B[\mathsf{fst}\,p/x]}\quad\textsc{right={$ \Sigma $-E$ {}{2}

}}\\ \frac{}{\mathsf{fst}\,\langle a,b\rangle\longrightarrow a\\ \mathsf{snd}\,\langle a,b\rangle\longrightarrow b}\quad\textsc{right={

\Sigma

-

\beta

}}

Figure 2: Dependent functions and dependent pairs. The

\mathsf{max}

\Sigma

-F makes

\Sigma

predicative; the

\mathsf{imax}

\Pi

-F makes

\Pi

impredicative at

\mathrm{Prop}

\frac{(x{:}A)\in\Gamma}{\Gamma\vdash x\Rightarrow A}\quad\textsc{right={Inf-Var}}\frac{\Gamma\vdash f\Rightarrow C\quad\Gamma\vdash C\equiv\Pi x{:}A.\,B:\mathrm{Sort}\,\ell\quad\Gamma\vdash a\Leftarrow A}{\Gamma\vdash f\,a\Rightarrow B[a/x]}\quad\textsc{right={Inf-App}}\\ \frac{\Gamma\vdash A\Rightarrow\mathrm{Sort}\,\ell\quad\Gamma,x{:}A\vdash b\Rightarrow B}{\Gamma\vdash\lambda x{:}A.\,b\Rightarrow\Pi x{:}A.\,B}\quad\textsc{right={Inf-Lam}}\frac{\Gamma\vdash C\equiv\Pi x{:}A^{\prime}.\,B:\mathrm{Sort}\,\ell\quad\Gamma\vdash A\Rightarrow\mathrm{Sort}\,\ell^{\prime}\quad A\equiv A^{\prime}\quad\Gamma,x{:}A\vdash b\Leftarrow B}{\Gamma\vdash\lambda x{:}A.\,b\Leftarrow C}\quad\textsc{right={Chk-Lam}}\\ \frac{\Gamma\vdash C\equiv\Sigma x{:}A.\,B:\mathrm{Sort}\,\ell\quad\Gamma\vdash a\Leftarrow A\quad\Gamma\vdash b\Leftarrow B[a/x]}{\Gamma\vdash\langle a,b\rangle\Leftarrow C}\quad\textsc{right={Chk-Pair}}\\ \frac{\Gamma\vdash A\Rightarrow\mathrm{Sort}\,\ell\quad\Gamma\vdash a\Leftarrow A}{\Gamma\vdash(a:A)\Rightarrow A}\quad\textsc{right={Inf-Ann}}\frac{\Gamma\vdash a\Rightarrow A\quad\Gamma\vdash A\leq B}{\Gamma\vdash a\Leftarrow B}\quad\textsc{right={Chk-Sub}}

Figure 3: Mode-relevant bidirectional rules. Chk-Lam checks that the domain of the abstraction is definitionally equal to the domain of the expected

\Pi

-type. The remaining term formers infer their types, placing premises in checking mode wherever the corresponding rule of Figure 2 specifies an expected type. A premise written

\Gamma\vdash C\equiv D:\mathrm{Sort}\,\ell

abbreviates the conjunction of

C\equiv D

(Definition 2.5 ) and

\Gamma\vdash D\Rightarrow\mathrm{Sort}\,\ell

; it is not a typed equality judgment.

\frac{\Gamma\ \mathsf{ctx}\quad\mathrm{FV}_{\mathrm{lvl}}(\ell)\subseteq\bar{u}}{\Gamma\vdash\mathrm{Sort}\,\ell:\mathrm{Sort}\,(\mathsf{s}\,\ell)}\quad\textsc{right={Sort}}\frac{\ell\simeq\ell^{\prime}}{\mathrm{Sort}\,\ell\equiv\mathrm{Sort}\,\ell^{\prime}}\quad\textsc{right={Sort-

\equiv

}}\frac{\Gamma\vdash A:\mathrm{Sort}\,\ell\quad\Gamma,x{:}A\vdash P:\mathrm{Prop}}{\Gamma\vdash\Pi x{:}A.\,P:\mathrm{Prop}}\quad\textsc{right={

\Pi

-Prop}}

Figure 4: Universe rules.

\bar{u}

are the level parameters in scope (Section 11 ).

\Pi

-Prop is the special case

\ell_{2}=\mathsf{0}

\Pi

-F , displayed separately for reference.

\frac{A\equiv B\quad\Gamma\vdash A:\mathrm{Sort}\,\ell\quad\Gamma\vdash B:\mathrm{Sort}\,\ell^{\prime}}{\Gamma\vdash A\leq B}\quad\textsc{right={S-Conv}}\frac{\Gamma\ \mathsf{ctx}\quad m\leq_{\mathrm{c}}n\quad\mathrm{FV}_{\mathrm{lvl}}(m,n)\subseteq\bar{u}}{\Gamma\vdash\mathrm{Sort}\,m\leq\mathrm{Sort}\,n}\quad\textsc{right={S-Cum}}\\ \frac{\Gamma\vdash A\leq B\quad\Gamma\vdash B:\mathrm{Sort}\,\ell\quad\Gamma\vdash B\leq C}{\Gamma\vdash A\leq C}\quad\textsc{right={S-Trans}}\\ \frac{A\equiv A^{\prime}\quad\Gamma,x{:}A^{\prime}\vdash B\leq B^{\prime}\quad\quad\Gamma\vdash\Pi x{:}A.\,B:\mathrm{Sort}\,\ell\quad\Gamma\vdash\Pi x{:}A^{\prime}.\,B^{\prime}:\mathrm{Sort}\,\ell^{\prime}}{\Gamma\vdash\Pi x{:}A.\,B\leq\Pi x{:}A^{\prime}.\,B^{\prime}}\quad\textsc{right={S-

\Pi

}}

Figure 5: The subsumption judgment. S-

\Pi

requires definitionally equal domains and is covariant in the codomain. The typing premises ensure that both sides of every subsumption, as well as the intermediate type in S-Trans , are well-formed types.

\frac{\Gamma\vdash A:\mathrm{Sort}\,\ell\quad\Gamma\vdash a:A\quad\Gamma\vdash b:A}{\Gamma\vdash\mathsf{Id}\,A\,a\,b:\mathrm{Prop}}\quad\textsc{right={Id-F}}\frac{\Gamma\vdash a:A}{\Gamma\vdash\mathsf{refl}\,a:\mathsf{Id}\,A\,a\,a}\quad\textsc{right={Id-I}}\\ \frac{\Gamma\vdash C:\Pi y{:}A.\,\mathsf{Id}\,A\,a\,y\to\mathrm{Sort}\,v\quad\Gamma\vdash d:C\,a\,(\mathsf{refl}\,a)\quad\Gamma\vdash b:A\quad\Gamma\vdash p:\mathsf{Id}\,A\,a\,b}{\Gamma\vdash\mathsf{J}\,a\,C\,d\,b\,p:C\,b\,p}\quad\textsc{right={Id-E}}\\ \frac{}{\mathsf{J}\,a\,C\,d\,b\,(\mathsf{refl}\,a^{\prime})\longrightarrow d}\quad\textsc{right={Id-

\iota

}}

Figure 6: The identity type. The base point

a

is an explicit argument of

\mathsf{J}

, as in the recursor for equality in Lean’s kernel theory, so a type checker reads

a

directly from the term rather than extracting it from the type of

C

. Rule Id-

\iota

matches the base point

a

, the target endpoint

b

, and the argument

a^{\prime}

\mathsf{refl}

as independent pattern variables and is therefore left-linear; when

\mathsf{J}\,a\,C\,d\,b\,(\mathsf{refl}\,a^{\prime})

is well typed, Rule Id-I ensures

a\equiv a^{\prime}\equiv b

, so the reduct

d

has the type of the redex up to

\equiv

\frac{\Gamma\vdash\bar{a}:\Delta_{P}[\bar{\ell}/\bar{u}]\quad\Gamma\vdash\bar{i}:\Delta_{I}[\bar{\ell}/\bar{u}][\bar{a}/\bar{p}]}{\Gamma\vdash D.\{\bar{\ell}\}\,\bar{a}\,\bar{i}:\mathrm{Sort}\,(\ell[\bar{\ell}/\bar{u}])}\quad\textsc{right={Ind-F}}\frac{\Gamma\vdash\bar{a}:\Delta_{P}[\bar{\ell}/\bar{u}]\quad\Gamma\vdash\bar{b}:\Delta_{k}[\bar{\ell}/\bar{u}][\bar{a}/\bar{p}]}{\Gamma\vdash c_{k}.\{\bar{\ell}\}\,\bar{a}\,\bar{b}:D.\{\bar{\ell}\}\,\bar{a}\,\bar{t}_{k}[\bar{a}/\bar{p},\bar{b}/\bar{y}]}\quad\textsc{right={Ind-I}}

Figure 7: Formation and introduction for a declared family

D

. Elimination is given by the typing of the constant

\mathsf{rec}_{D}

(Definition 2.18 ) and computation by Rule

\iota

. The notation

\Gamma\vdash\bar{a}:\Delta

abbreviates typing each term in the list against the corresponding entry of the telescope instantiated at the preceding terms.

\frac{}{\cdot\ \mathsf{wf}}\quad\textsc{right={E-Empty}}\frac{\mathcal{S}\ \mathsf{wf}\quad c\notin\mathcal{S}\quad\mathcal{S};\cdot\vdash_{\bar{u}}A:\mathrm{Sort}\,\ell}{\mathcal{S},\mathsf{axiom}\ c.\{\bar{u}\}:A\ \mathsf{wf}}\quad\textsc{right={E-Ax}}\frac{\mathcal{S}\ \mathsf{wf}\quad c\notin\mathcal{S}\quad\mathcal{S};\cdot\vdash_{\bar{u}}A:\mathrm{Sort}\,\ell\quad\mathcal{S};\cdot\vdash_{\bar{u}}t:A}{\mathcal{S},\mathsf{def}\ c.\{\bar{u}\}:A:=t\ \mathsf{wf}}\quad\textsc{right={E-Def}}\frac{\mathcal{S}\ \mathsf{wf}\quad D,\bar{c},\mathsf{rec}_{D}\notin\mathcal{S}\quad\text{the declaration is admissible in }\mathcal{S}}{\mathcal{S},\mathsf{inductive}\ D.\{\bar{u}\}\ldots\ \mathsf{wf}}\quad\textsc{right={E-Ind}}\\ \frac{\Gamma\ \mathsf{ctx}\quad(c.\{\bar{u}\}:A)\in\mathcal{S}\quad|\bar{\ell}|=|\bar{u}|\quad\mathrm{FV}_{\mathrm{lvl}}(\bar{\ell})\subseteq\bar{v}}{\Gamma\vdash_{\bar{v}}c.\{\bar{\ell}\}:A[\bar{\ell}/\bar{u}]}\quad\textsc{right={Const}}\frac{(\mathsf{def}\ c.\{\bar{u}\}:A:=t)\in\mathcal{S}\text{ transparent}}{c.\{\bar{\ell}\}\longrightarrow t[\bar{\ell}/\bar{u}]}\quad\textsc{right={

\delta

}}

Figure 8: Well-formed environments, constants, and

\delta

-unfolding. The subscript

\vdash_{\bar{u}}

records the level parameters in scope; in Const ,

\bar{u}

are the level parameters of the declaration and

\bar{v}

are those in scope at the call site. Rule E-Def applies to both transparent and opaque definitions.

\frac{\Gamma\vdash P:\mathrm{Prop}\quad\Gamma\vdash p:P\quad\Gamma\vdash q:P}{\Gamma\vdash\mathsf{irrel}\,P\,p\,q:\mathsf{Id}\,P\,p\,q}\quad\textsc{right={PI}}

Figure 9: Proof irrelevance, derived from the axiom

\mathsf{irrel}

	MLTT (1984)	ECC	CIC (Coq)	Lean 4 kernel	This chapter
Impredicative $\mathrm{Prop}$	no	yes	yes	yes	yes
Cumulativity	yes ( $U_{n}$ )	yes, $\mathrm{Prop}\preceq\mathrm{Type}_{0}$	yes	no	yes, from $\mathrm{Set}$ upward
Structural subsumption	none	$\Pi$ codomain; $\Sigma$ both	$\Pi$ codomain; cumulative inductives	none	$\Pi$ codomain; no $\Sigma$
Universe polymorphism	no	no	yes	yes	yes
Inductive families	fixed set formers, W-types	no	yes	yes	yes, strictly positive, not nested
Identity type	primitive, extensional	none (Leibniz equality)	inductive, in $\mathrm{Prop}$	inductive, in $\mathrm{Prop}$	primitive, in $\mathrm{Prop}$

Table 2: Differences between the theory of this chapter and the theories it draws on.

Left out	Constructs	Treated in
Program constructs	component calls, mapping and reduction combinators, templates, institution invocation	Volume IV (ESL, the runtime)
Knowledge-graph types	record types, refinement types, class types, primitive types and literals, property access, record construction, native decision procedures, apartness	Chapter 5
Institution-facing references	axioms anchored on the chain, references to externally checked propositions	Chapter 4 ; Volume II
General recursion	recursive definitions not reducible to recursors	excluded from the theory
Coercive subtyping with computing coercions	dot-types, changes of representation	Volume III, as an elaboration-level extension

Table 3: Constructs outside the theory of this chapter.

Obligation	Status	Where
Kernel signature morphisms preserve all judgments	proved	Lemma 4.12
Reflexivity, monotonicity, transitivity, $\vdash$ -translation	proved	Lemmas 4.16 – 4.19
$P_{\mathbb{K}}$ functorial on $\mathbf{Th}_{0}$ ; $\pi$ natural	proved	Lemma 4.20
The kernel is a compact proof calculus with Tarskian $\vdash$	proved	Theorem 4.21
Weakening, substitution, level instantiation	cited	Chapter 2
Quotienting witnesses by provable identity collapses to $\mathbb{E}^{\natural}$	proved	Proposition 4.22

Table 13

#	Definition	Source	Used in
1	type system; witness judgment	App. A2.1 cl. 1–4; A3.2; Ch. 1 §1.3	KG, P
2	basic types	App. A2.1; A3.2 cl. 1–3	KG, P
3	ptypes	App. A3.1; A3.2 cl. 5–8	P; KG (§ 41 )
4	record types	App. A1; A11.2 cl. 1, 3, 5, 7	KG, P
5	records; membership	App. A11.1; A11.2 cl. 2, 4, 6, 8	KG, P
6	dependent fields; dependency families	App. A11.2 (dependent) cl. 1–2; A11.6	KG, P

Table 5: The TTR definitions used in the book, with their sources in Cooper (2023) and their uses.

Typed feature structures	TTR	Knowledge graph
type hierarchy (bounded-complete partial order)	subtyping between named types	class hierarchy $\sqsubseteq^{*}$ (a preorder)
appropriateness $\mathrm{Approp}(f,t)$	the record type of a named type	$R_{C}$ : required properties and their field types
feature introduction	width inheritance along $\sqsubseteq$	requirement inheritance (Definition 5.23 )
well-typed; totally well-typed	$r:T$ for record types	structural membership; totality: all required fields present
subsumption $F\sqsubseteq_{\mathrm{fs}}F^{\prime}$ , the more general structure on the left	subtyping $T^{\prime}\sqsubseteq T$ , the more specific type on the left	width subtyping
unification; failure	meet of record types; uninhabited meet	refinement (Definition 5.34 )

Table 6: Typed feature structures, TTR, and the knowledge graph.

	join of singletons $\mathrm{En}(V)$	labeled sum $E_{V}$ (inductive)
values	the IRIs themselves	new constructors $c_{i}$
relation to $\mathsf{IRI}$	subtype, identity coercion	separate type; $g$ computes
$V\subseteq V^{\prime}$	$\mathrm{En}(V)\leq\mathrm{En}(V^{\prime})$	$E_{V}$ , $E_{V^{\prime}}$ unrelated
distinctness	Lemma 5.41 , from $\mathsf{eqb}$	built in (no confusion)
elimination	$\mathsf{eqb}$ tests and Theorem 5.43	recursor, match

Table 7: Join of singletons and labeled sum, for an enumeration

V

Level	Judgment or proposition	Character
declared	$\exists D\in S_{r}.\ D\sqsubseteq^{*}C$	intensional; decidable
structural	$\rho_{r}:_{\nu\Phi}R_{C}$	extensional over fields; decidable (Proposition 5.31 )
propositional	$\mathsf{is\_a}(r,C)$ , $\mathsf{subclass\_of}(C,D)$	a claim: can be hypothesized, proved, grounded

Table 8: Three levels of membership.

Framework	Shared	Deltas
TTR	records, record types, singletons, meets, joins, dependent fields, intensional types (Section 35 )	embedded in a dependent type theory with $\mathrm{Prop}$ ; record types as canonical telescopes; width and depth as subsumption rules; membership as a greatest fixed point over a graph
Typed feature structures; HPSG	appropriateness, feature introduction, total well-typedness, unification as meet (Section 36 )	reversed naming of the order; open, not closed; no depth refinement per class; reentrancy only by reference
Luo: common nouns as types; coercive subtyping; dependent record types	classes as types; subsumption between classes; $\Sigma$ -like records	identity-coercion fragment only; no computing coercions
RDF, RDFS, OWL; description logic	$\sqsubseteq$ as concept inclusion; EquivalentClasses as concept equivalence; a required property $p$ as $C\sqsubseteq\exists p.\tau_{p}$ ; open world as width membership	domain rejects a field instead of inferring membership; membership requires a declaration; no property-level reasoning (Appendix 5.A )
SHACL	required properties as minimum cardinality one; value types; validation that rejects	shapes are separate from classes; here the class is the shape
Barlatier–Dapoigny	ontologies on dependent record types	classes are named (intensional) types; membership has a declared component

Table 9: Related frameworks: shared constructions and deltas.

\frac{(x{:}T)\in\Gamma}{\Gamma\vdash x\Rightarrow_{\mathsf{a}}T}\quad\textsc{right={A-Var}}\frac{\mathrm{FV}_{\mathrm{lvl}}(\ell)\subseteq\bar{u}}{\Gamma\vdash\mathrm{Sort}\,\ell\Rightarrow_{\mathsf{a}}\mathrm{Sort}\,(\mathsf{s}\,\ell)}\quad\textsc{right={A-Sort}}\frac{(c.\{\bar{u}\}:A)\in\mathcal{S}\quad|\bar{\ell}|=|\bar{u}|\quad\mathrm{FV}_{\mathrm{lvl}}(\bar{\ell})\subseteq\bar{v}}{\Gamma\vdash c.\{\bar{\ell}\}\Rightarrow_{\mathsf{a}}|A|[\bar{\ell}/\bar{u}]}\quad\textsc{right={A-Const}}\\ \frac{\Gamma\vdash A\Rightarrow_{\mathsf{a}}C_{1}\quad C_{1}\searrow\mathrm{Sort}\,\ell_{1}\quad\Gamma,x{:}|A|\vdash B\Rightarrow_{\mathsf{a}}C_{2}\quad C_{2}\searrow\mathrm{Sort}\,\ell_{2}}{\Gamma\vdash\Pi x{:}A.\,B\Rightarrow_{\mathsf{a}}\mathrm{Sort}\,(\mathsf{imax}\,\ell_{1}\,\ell_{2})}\quad\textsc{right={A-

\Pi

}}\frac{\Gamma\vdash A\Rightarrow_{\mathsf{a}}C\quad C\searrow\mathrm{Sort}\,\ell\quad\Gamma,x{:}|A|\vdash b\Rightarrow_{\mathsf{a}}B}{\Gamma\vdash\lambda x{:}A.\,b\Rightarrow_{\mathsf{a}}\Pi x{:}|A|.\,B}\quad\textsc{right={A-Lam}}\\ \frac{\Gamma\vdash f\Rightarrow_{\mathsf{a}}C\quad C\searrow\Pi x{:}A.\,B\quad\Gamma\vdash a\Leftarrow_{\mathsf{a}}A}{\Gamma\vdash f\,a\Rightarrow_{\mathsf{a}}B[|a|/x]}\quad\textsc{right={A-App}}\frac{\Gamma\vdash p\Rightarrow_{\mathsf{a}}C\quad C\searrow\Sigma x{:}A.\,B}{\Gamma\vdash\mathsf{fst}\,p\Rightarrow_{\mathsf{a}}A}\quad\textsc{right={A-Fst}}\frac{\Gamma\vdash p\Rightarrow_{\mathsf{a}}C\quad C\searrow\Sigma x{:}A.\,B}{\Gamma\vdash\mathsf{snd}\,p\Rightarrow_{\mathsf{a}}B[\mathsf{fst}\,|p|/x]}\quad\textsc{right={A-Snd}}\\ \frac{\Gamma\vdash A\Rightarrow_{\mathsf{a}}C\quad C\searrow\mathrm{Sort}\,\ell\quad\Gamma\vdash a\Leftarrow_{\mathsf{a}}|A|\quad\Gamma\vdash b\Leftarrow_{\mathsf{a}}|A|}{\Gamma\vdash\mathsf{Id}\,A\,a\,b\Rightarrow_{\mathsf{a}}\mathrm{Prop}}\quad\textsc{right={A-Id}}\frac{\Gamma\vdash A\Rightarrow_{\mathsf{a}}C\quad C\searrow\mathrm{Sort}\,\ell\quad\Gamma\vdash a\Leftarrow_{\mathsf{a}}|A|}{\Gamma\vdash(a:A)\Rightarrow_{\mathsf{a}}|A|}\quad\textsc{right={A-Ann}}\\ \frac{\Gamma\vdash C\Rightarrow_{\mathsf{a}}T\quad T\searrow\Pi y{:}A.\,T_{1}\quad T_{1}\searrow\Pi z{:}T_{2}.\,T_{3}\quad\quad T_{2}\searrow\mathsf{Id}\,A^{\prime}\,a^{\prime}\,y^{\prime}\quad T_{3}\searrow\mathrm{Sort}\,v\quad A^{\prime}\Leftrightarrow_{\mathsf{a}}A\quad y^{\prime}\Leftrightarrow_{\mathsf{a}}y\quad\quad\Gamma\vdash a\Leftarrow_{\mathsf{a}}A\quad a^{\prime}\Leftrightarrow_{\mathsf{a}}|a|\quad\Gamma\vdash b\Leftarrow_{\mathsf{a}}A\quad\quad\Gamma\vdash d\Leftarrow_{\mathsf{a}}|C|\,|a|\,(\mathsf{refl}\,|a|)\quad\Gamma\vdash p\Leftarrow_{\mathsf{a}}\mathsf{Id}\,A\,|a|\,|b|}{\Gamma\vdash\mathsf{J}\,a\,C\,d\,b\,p\Rightarrow_{\mathsf{a}}|C|\,|b|\,|p|}\quad\textsc{right={A-J}}

Figure 10: Inference in the algorithmic systems

\mathcal{A}_{0}

and

\mathcal{A}_{1}

. The types of the context and of the judgments are annotation-free. A-

\Sigma

is A-

\Pi

with

\mathsf{max}

in place of

\mathsf{imax}

. In A-J , the premises compare the type of the motive with

\Pi y{:}A.\,\mathsf{Id}\,A\,a\,y\to\mathrm{Sort}\,v

for the base point

a

of the term, and they are evaluated from left to right. As in Chapter 2 ,

\bar{u}

are the level parameters in scope, and in A-Const

\bar{u}

are the parameters of the declaration and

\bar{v}

those in scope.

\frac{C\searrow\Pi x{:}A^{\prime}.\,B\quad\Gamma\vdash A\Rightarrow_{\mathsf{a}}D\quad D\searrow\mathrm{Sort}\,\ell\quad|A|\Leftrightarrow_{\mathsf{a}}A^{\prime}\quad\Gamma,x{:}|A|\vdash b\Leftarrow_{\mathsf{a}}B}{\Gamma\vdash\lambda x{:}A.\,b\Leftarrow_{\mathsf{a}}C}\quad\textsc{right={A-Chk-Lam}}\frac{C\searrow\Sigma x{:}A.\,B\quad\Gamma\vdash a\Leftarrow_{\mathsf{a}}A\quad\Gamma\vdash b\Leftarrow_{\mathsf{a}}B[|a|/x]}{\Gamma\vdash\langle a,b\rangle\Leftarrow_{\mathsf{a}}C}\quad\textsc{right={A-Chk-Pair}}\\ \frac{C\searrow\mathsf{Id}\,A\,x\,y\quad\Gamma\vdash a\Leftarrow_{\mathsf{a}}A\quad x\Leftrightarrow_{\mathsf{a}}|a|\quad|a|\Leftrightarrow_{\mathsf{a}}y}{\Gamma\vdash\mathsf{refl}\,a\Leftarrow_{\mathsf{a}}C}\quad\textsc{right={A-Chk-Refl}}\frac{\Gamma\vdash a\Rightarrow_{\mathsf{a}}A\quad A\leq_{\mathsf{a}}C}{\Gamma\vdash a\Leftarrow_{\mathsf{a}}C}\quad\textsc{right={A-Chk-Sub}}\\ \frac{A\Leftrightarrow_{\mathsf{a}}B}{A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Sub-Conv}}\frac{A\searrow\mathrm{Sort}\,m\quad B\searrow\mathrm{Sort}\,n\quad m\leq_{\mathrm{c}}n}{A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Sub-Cum}}\frac{A\searrow\Pi x{:}A_{1}.\,B_{1}\quad B\searrow\Pi x{:}A_{2}.\,B_{2}\quad A_{1}\Leftrightarrow_{\mathsf{a}}A_{2}\quad B_{1}\leq_{\mathsf{a}}B_{2}}{A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Sub-

\Pi

}}

Figure 11: Checking and subsumption in the algorithmic system

\mathcal{A}_{1}

;

\mathcal{A}_{0}

omits A-Sub-

\Pi

\frac{A\searrow C\quad C\text{ a class}\quad B\searrow\mathsf{Entity}}{\Gamma\vdash A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Class-Ent}}\frac{A\searrow C\quad B\searrow D\quad C\sqsubseteq^{*}D}{\Gamma\vdash A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Class-Sub}}\\ \frac{A\searrow n\quad\Gamma\vdash n\Rightarrow_{\mathsf{s}}U\quad U\searrow\mathsf{Class}\quad B\searrow\mathsf{Entity}}{\Gamma\vdash A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Class-Var}}\\ \frac{B\searrow T_{1}\vee T_{2}\quad\Gamma\vdash A\leq_{\mathsf{a}}T_{i}}{\Gamma\vdash A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Join-I}}\frac{A\searrow T_{1}\vee T_{2}\quad B\searrow U\quad U\text{ a graph type}\quad\Gamma\vdash T_{1}\leq_{\mathsf{a}}B\quad\Gamma\vdash T_{2}\leq_{\mathsf{a}}B}{\Gamma\vdash A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Join-L}}\\ \frac{A\searrow\mathsf{sing}\,T\,b\quad B\searrow U\quad U\text{ a graph type}\quad\Gamma\vdash T\leq_{\mathsf{a}}B}{\Gamma\vdash A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Sing-Sub}}\\ \frac{A\searrow R\quad B\searrow R^{\prime}\quad\mathrm{labels}(R^{\prime})\subseteq\mathrm{labels}(R)\quad\Gamma,\mathrm{tel}(R)\vdash A_{\ell}\leq_{\mathsf{a}}A^{\prime}_{\ell}\quad(\ell\in\mathrm{labels}(R^{\prime}))\quad w\leq w^{\prime}}{\Gamma\vdash A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Rec-Sub}}\\ \frac{A\searrow R\wedge\textstyle\bigwedge S\quad B\searrow R^{\prime}\wedge\textstyle\bigwedge S^{\prime}\quad\Gamma\vdash R\leq_{\mathsf{a}}R^{\prime}\quad\forall D^{\prime}\in S^{\prime}.\ \exists D\in S.\ D\sqsubseteq^{*}D^{\prime}}{\Gamma\vdash A\leq_{\mathsf{a}}B}\quad\textsc{right={A-Ref-Sub}}\\ \frac{C\searrow\mathsf{sing}\,T\,b\quad\Gamma\vdash a\Leftarrow_{\mathsf{a}}T\quad|a|\Leftrightarrow_{\mathsf{a}}b}{\Gamma\vdash a\Leftarrow_{\mathsf{a}}C}\quad\textsc{right={A-Chk-Sing}}\frac{C\searrow T_{1}\vee T_{2}\quad\Gamma\vdash a\Leftarrow_{\mathsf{a}}T_{i}}{\Gamma\vdash a\Leftarrow_{\mathsf{a}}C}\quad\textsc{right={A-Chk-Join}}

Figure 12: The rules that the procedure gains for Chapter 5 , with

i\in\{1,2\}

\mathsf{sing}\,T\,b

is the singleton

T_{b}

T

. In A-Rec-Sub ,

A_{\ell}

and

A^{\prime}_{\ell}

are the field types of the record types

R

and

R^{\prime}

, and

w

and

w^{\prime}

their levels. A graph type is a weak-head normal form headed by a former of the class system (Definition 5.38 ).

\Gamma\vdash n\Rightarrow_{\mathsf{s}}U

reads the type of a neutral term off its spine.

Result	Status
Weak-head reduction is deterministic; stability of weak-head normal forms	proved (Lemmas 6.3 , 6.4 )
Conversion test sound, complete relative to termination	proved (Theorem 6.7 (1), (2))
Normalization by evaluation sound, complete on $\mathrm{SN}$	proved (Theorem 6.11 )
Inversion lemmas	proved (Section 5 )
Type checker sound, complete relative to termination	proved (Theorems 6.16 , 6.17 ; Proposition 6.20 )
Properties of the checker for Chapters 3 and 4	proved (Proposition 6.21 )

Table 12: The results of the chapter and their status.

Appendix figures & tables7 assets

Supplementary material from the paper’s appendix.

Appendix

Atomic Data	Data model	Theory
resource (subject URL)	resource ( urn: IRI)	record (Section 39 )
Property (requires shortname , datatype , description ; recommends classtype , allows-only , …)	property declaration	a label with its field type
datatype : slug, atomicURL, URI, string, markdown, integer, float, boolean, date, timestamp, resourceArray, json, ydoc	data_type (with format , content_type )	basic types (Definition 5.3 )
resourceArray	list-valued property	list type (Definition 5.11 )
classtype : one class, for atomicURL or resourceArray values	class_types : one or several classes	a class type; several give a join (Section 40 )
allows-only : a resourceArray of allowed values	allows_only	join of singletons; values compared by IRI, as tags (Section 40 )

Appendix

Table 10: Atomic Data, the data model of this chapter, and the theory.

RDFS / OWL / schema.org	Data model	Theory
rdfs:subClassOf	core:subclass_of (absent in Atomic Data)	declared subsumption between named types; requirement inheritance (Section 38 )
owl:equivalentClass	core:EquivalentClasses , an $n$ -ary resource listing core:classes	mutual subsumption; equal record types, distinct classes (Corollary 5.25 )
rdfs:domain (restrictive)	core:domain	bound on width (Definition 5.36 )
schema.org domainIncludes (advisory)	core:recommends on each domain class	admitted by width; not in the type
rdfs:range , rangeIncludes over classes	class_types	class type, or join of classes
owl:oneOf ; schema.org enumeration members	allows_only , with class_types $=[E]$ for an enumeration class $E$	join of singletons met with the class type

Appendix

Table 11: Constructs added for RDFS, OWL, and schema.org.

Book	Lean	Module	Status
Definition 2.7	Level , Level.eval , the Preorder instance, the Setoid instance, the order of cumulativity Level.CumLe	Level	definition
Proposition 2.8	Level.succ_congr , max_congr , imax_congr , imax_zero , imax_succ , inst_le_inst , inst_congr ; for $\leq_{\mathrm{c}}$ , CumLe.refl , CumLe.trans , CumLe.le , CumLe.of_le , CumLe.inst , cumLe_zero_iff , not_cumLe_zero_succ	Level	proved
Definition 2.1	Term	Term	definition
Definition 2.2	Term.liftN , Term.inst , Term.instL , Level.inst , with the lifting and substitution lemmas	Term	definition
The rules $\delta$ and $\iota$ as an interface to reduction (Definitions 2.25 and 2.18 )	RuleSet : shape, determinism, closure under liftN , inst , and instL	Reduction	definition
Definition 2.5 , one-step reduction $\longrightarrow$ and $\longrightarrow^{*}$	RuleSet.Red , RuleSet.RedStar ; parallel reduction RuleSet.Par with Par.liftN , Par.inst , Red.toPar , Par.toRedStar	Reduction	definition

Appendix

Table 25

Book	Lean	Module	Status
Definition 3.14	JTerm , Leaf , JTerm.leaves	Terms	definition
Conventions of Section 19	PropositionSystem	Kernel	interface
Definition 3.15	ConstantSpec , ConstantSpec.Admitted	Kernel	definition
Definition 3.17	ConstantSpec.evid	Evidence	definition
Lemma 3.18	ConstantSpec.card_evid_le	Evidence	proved
Definition 3.20	ConstantSpec.JB	Evidence	definition

Appendix

Table 26

Book	Lean	Module	Status
Definition 4.1	Institution	Basic	definition
Definition 4.2 (b)	Institution.Comorphism	Basic	definition
Semantic consequence, after Definition 4.1	Institution.SemCons	Basic	definition
Definition 4.3	EntailmentSystem	Entailment	definition
Closure function, Remark 2 after Definition 4.3	EntailmentSystem.clo and its laws	Entailment	proved
Definition 4.5	Logic , Logic.toInstitution , Logic.semCons , Logic.Complete	Logic	definition

Appendix

Table 27

Book	Lean	Module	Status
Definition 5.1	Value , FieldType , RecType , KGraph	Graph	definition
Definition 5.23	KGraph.DeclSub , Anc , Eqv , Req , RC , CondReqs	Graph	definition
Theorem 5.24	req_mono , rsub_RC_of_anc	Graph	proved
Corollary 5.25	RC_eq_of_eqv	Graph	proved
Definition 5.29	KGraph.VTy , RecTy , CondTy	Graph	definition
Definition 5.30	Declared , Structural , phi , Member , Mem	Graph	definition

Appendix

Table 28

Book	Lean	Module	Status
Section 1 , erasures	RuleSet.DefEq.erase_iff	TypeTheory/AnnotatedReduction	proved
Section 1 , strong normalization	SN , SN.red , SN.of_mem_comps , SN.acc_desc	Conversion	definition, proved
Definition 6.2	WhStep , WHShape , whStrategy , Env.rules_whShape , Env.whStrategy	WeakHead , EnvShape	definition, proved
Lemma 6.3	WhStep.toRed , WhStep.det	WeakHead	proved
Lemma 6.4	Rigid , Whnf.rigid	Conversion , WeakHead	proved
Corollary 6.5	Rigid.join , Rigid.defEq_iff	Conversion	proved

Appendix

Table 29

Dependent Type Theory

See all 8 papers

Aug 5, 2026

Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning

As "AI Scientists" emerge to drive research via the Model Context Protocol (MCP), systems relying on ephemeral scripts will fail. The sheer scale of stateful, interconnected evidence requires a machine-walkable warranty grounded in a purpose-built database architecture. Eigenius is an open-source, typed knowledge-graph DBMS built on a single premise: answering the audit question ("what do you know, and what is your warranty?") requires a unified kernel. By tightly coupling the type system, storage engine, and integration protocol, Eigenius turns data provenance into a structural invariant rather than a property reconstructed across subsystem boundaries. The kernel rests on three pillars whose metatheory is mechanized in Lean 4: a dependent type theory (EigenTT) separating confluent conversion from ontology subsumption and keeping proof irrelevance axiomatic so distinct warrants remain inspectable; proof-calculus institutions acting as strongly typed integration boundaries; and a content-addressed immutable storage layer. Epistemic status (declared/observed/derived/verified) forms a bounded lattice over a justification logic enforced at commit. Cross-system comorphisms carry explicit axiom policies (Adopt, Discharge, Relativize), transport witnesses at commit, and materialize outputs into the graph, while EigenQL provides a Grothendieck query view across all hosted logics and shared on-chain IRs collapse multi-system translations to identity. Pairing empirical justification logic with an in-process Lean 4 term checker, an end-to-end recomputation of a published Nature study from pinned data discharges all 52 derived conclusions and surfaces four machine-checked discrepancies in the original study.

Hans-Martin Will, Allen L. Brown, Matthew Fuchs

The Eigenius Project, United States · Docimion, United States

Data Provenance Dependent Type Theory Knowledge Graphs

Ask PDF

Oct 19, 2026

Theorem prover Arend

This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the framework of univalent foundations and with the focus on constructive mathematics. It is based on a variant of homotopy type theory with cubical syntax that is more closely aligned with Martin-Löf Type Theory (MLTT) than fully computational cubical type theories, while still retaining some of their computational properties useful in practice. Among the most notable features of the Arend language is its powerful system of classes and records supporting subsumptive subtyping, partial implementations and anonymous extensions, which provides extensive flexibility for constructing hierarchies of definitions. Formalization in Arend is streamlined by the IntelliJ Arend plugin, which transforms IntelliJ IDEA into a full-fledged integrated development environment (IDE) for the Arend language. The main Arend library arend-lib includes formalizations in constructive algebra, topology and synthetic homotopy theory.

Fedor Part, Valery Isaev, Sergey Sinchuk

JetBrains Research

Dependent Type Theory Interactive Theorem Proving

Ask PDF

Jun 2, 2026

ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics

We propose ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Lof Dependent Type Theory (MLTT) integrating trace-indexed types, presheaf non-monotone semantics, and constructive AGM belief revision. A Coq mechanisation accompanies the paper (34 complete proofs; zero admits for the two central results). (I) Trace types. FinTrace(s0,sn) is an inductive family of typed execution traces. FinTrace and Star(Step) are isomorphic as path types but not judgementally equal; TraceElim exposes the event label e:Event explicitly, giving a more ergonomic interface for event-driven induction. We prove the Trace-Reachability Correspondence, Deterministic Replay, and a canonicity framework via reducibility candidates with a Transport Lemma (RC-elim deferred; all other Core results are Coq-verified). (II) Sheaf semantics. Trace-indexed propositions are contravariant sheaves over the free trace partial-order category Tf. A Separation Theorem (explicit countermodel) distinguishes proof-theoretic monotonicity from semantic non-monotonicity. The term model is an initial CwF (syntactic universal property, not classical completeness). (III) AGM belief revision. We give an explicit constructive partial meet contraction algorithm verified against (C1)-(C4). All eight AGM postulates (R1)-(R8) are theorems. Proofs of R7 and R8 use the Disjunctive Entrenchment Lemma, given a self-contained constructive derivation. (IV) Integration. B^AGM fails the sheaf composition law BP-comp for sequential revision (explicit countermodel, Coq-verified). We introduce Single-Step Revision Systems (SSRS), prove B^AGM is a valid SSRS (Coq-verified), and show this suffices for trace morphisms, retraction characterisation, and revision witnesses. The BP-comp failure reveals a fundamental tension between path-dependent belief revision and functor consistency, not previously identified.

Peng Chen

School of Information Science, Beijing Language and Culture University Beijing 100081

Belief Revision Logical Reasoning Dependent Type Theory Nonmonotonic Reasoning

Ask PDF

Abstract

Dependent Type Theory

Explore similar work

Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning

Theorem prover Arend

ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics