Normalization by Evaluation with Substitutions as Operations CPYWHRTPKC

URI	`m2://res/CPYWHRTPKC`
Kind	preprint
Creators	Jason Z. S. Hu
Date	2026-10-15
Subjects	arxiv cs.PL, arxiv math.LO
Scope	border

Expressions

e1: version, preprint

Date	2026-10-15
Ids	arXiv 2610.21131

Items in this resource

The mentions of the inventory that name this resource. Each name links to the card of its inventory row.

Item	Kind	Where	Source
Identity Substitution	statement	lemma 2.17	arxiv
Pointwise Equality at the Head Yields Type Equality	statement	corollary 4.14	arxiv
Realizability of the gluing model	statement	theorem 7.32	arxiv
Fundamental --- \textsc{Tm-Trans	statement	lemma 6.49	arxiv
1TSPHEFCTB	statement	lemma 5.2	arxiv
Identity is a Semantic Weakening	statement	lemma 6.27	arxiv
Fundamental --- \textsc{Ctx-Ext	statement	lemma 6.51	arxiv
$\Uc_i$ implies $\mathrel{<:_i}$	statement	lemma 6.17	arxiv
$q$ Distributes over Composition	statement	lemma 2.21	arxiv
Base PERs are PERs	statement	lemma 6.4	arxiv
Identity Weakening	statement	lemma 2.6	arxiv
Fundamental --- \textsc{Sub-Univ	statement	lemma 6.69	arxiv
Semantic --- \textsc{Ze-I	statement	lemma 7.40	arxiv
Composition of Substitutions is Well-Typed	statement	lemma 4.8	arxiv
Subtyping of $\Uc_i$	statement	lemma 6.15	arxiv
PER $\textsf{Neu}$	definition	definition 6.5	arxiv
Weakenings	definition	definition 2.3	arxiv
4GTZX47TQY	statement	lemma 3.2	arxiv
Substitution Preserves Judgments	statement	lemma 4.7	arxiv
Initial Environment	definition	definition 5.4	arxiv
Semantic Weakening	definition	definition 6.26	arxiv
Action of $q^n$ on Indices	statement	lemma 2.18	arxiv
Universe Term Predicate $\textsf{Univ}_{i,j}^{\El}$	definition	definition 7.12	arxiv
Right irrelevance of $\Uc_i$	statement	lemma 6.12	arxiv
Fundamental --- \textsc{Var	statement	lemma 6.56	arxiv
Fundamental --- \textsc{N-E} / \textsc{Rec-Cong	statement	lemma 6.63	arxiv
Extension is Well-Typed	statement	lemma 4.3	arxiv
Substitution Operations	definition	definition 2.11	arxiv
Fundamental --- \textsc{$\Pi$-$\eta$	statement	lemma 6.66	arxiv
Functionality of $\Uc_i^\ast$	statement	lemma 7.24	arxiv
7E2AMFYY4V	statement	lemma 4.10	arxiv
Extension--Composition Distribution	statement	lemma 2.26	arxiv
Semantic Judgment for Terms	definition	definition 6.31	arxiv
Semantic --- \textsc{Ctx-Ext	statement	lemma 7.35	arxiv
Fundamental Theorem (Soundness	statement	theorem 7.47	arxiv
Pi Type Predicate $\Pi_i(R_I, P_I, \El_I, P_O)$	definition	definition 7.9	arxiv
Semantic --- \textsc{$\lambda$-E	statement	lemma 7.43	arxiv
PER $\textsf{Nat}$	definition	definition 6.6	arxiv
Semantic --- \textsc{Su-I	statement	lemma 7.41	arxiv
Extension by precomposed term	statement	lemma 6.45	arxiv
Fundamental --- \textsc{Sub-Eq	statement	lemma 6.72	arxiv
Weakening Preserves Typing	statement	lemma 4.1	arxiv
Semantic weakening gives semantic substitution	statement	lemma 6.35	arxiv
Natural Number Type Predicate $\textsf{Nat}_i$	definition	definition 7.7	arxiv
$q$--Extension Interaction	statement	lemma 2.27	arxiv
Embedding Correctness	statement	lemma 2.14	arxiv
Semantic --- \textsc{N-Wf	statement	lemma 7.38	arxiv
Context Gluing Monotonicity	statement	corollary 7.20	arxiv
\textsc{N-E} helper	statement	lemma 7.44	arxiv
Initial environment is in context PER	statement	lemma 6.25	arxiv
Substitution Application	definition	definition 2.12	arxiv
Identity Substitution is Well-Typed	statement	lemma 4.2	arxiv
Weakening--Substitution Commutation (Generalized	statement	lemma 2.20	arxiv
Weakening Application	definition	definition 2.4	arxiv
Composition Preserves Weakening Typing	statement	lemma 3.6	arxiv
Fundamental --- \textsc{Tm-Sym	statement	lemma 6.48	arxiv
Extension is semantic	statement	lemma 6.44	arxiv
$q$ Preserves Weakening Typing	statement	lemma 3.5	arxiv
PER $\Nf$ --- Normal Forms	definition	definition 6.1	arxiv
Fundamental --- \textsc{$\Pi$-$\beta$	statement	lemma 6.65	arxiv
Semantic Domain	definition	definition 5.1	arxiv
Lifting is semantic	statement	lemma 6.47	arxiv
$q$ Preserves Substitution Equivalence	statement	lemma 4.12	arxiv
Fundamental --- \textsc{$\lambda$-E} / \textsc{App-Cong	statement	lemma 6.60	arxiv
Fundamental --- \textsc{N-$\beta$-Su	statement	lemma 6.68	arxiv
Kripke weakenings are weakenings	statement	lemma 7.2	arxiv
Single Substitution Lemma	statement	corollary 4.9	arxiv
Soundness of NbE	statement	theorem 7.48	arxiv
Precomposition of substitutions by $\Uparrow$	statement	lemma 6.40	arxiv
$q$ Preserves Substitution Typing	statement	lemma 4.6	arxiv
Gluing respects judgmental equality	statement	lemma 7.26	arxiv
Identity is semantic	statement	lemma 6.36	arxiv
Natural Number Term Predicate $\textsf{Nat}_i$	definition	definition 7.8	arxiv
Neutral Predicate $\Ne_i^a$	definition	definition 7.14	arxiv
Categorical Laws for Weakenings	statement	lemma 2.10	arxiv
Monotonicity	statement	theorem 7.19	arxiv
Semantic context yields context PER	statement	lemma 6.34	arxiv
Semantic --- \textsc{N-E	statement	lemma 7.45	arxiv
Term-predicate syntactic escape	statement	lemma 7.23	arxiv
$q$ Commutes with Pointwise Weakening	statement	lemma 2.23	arxiv
Determinism	statement	lemma 5.3	arxiv
Weakening--Substitution Interaction	statement	lemma 2.24	arxiv
Symmetry of context PER	statement	lemma 6.22	arxiv
Weakening of Substitution is Well-Typed	statement	lemma 4.5	arxiv
Contexts	definition	definition 2.2	arxiv
Expansion of Substitutions	statement	lemma 2.31	arxiv
Decidability of Judgmental Equality	statement	corollary 7.49	arxiv
Term predicate closed under PER-equivalence	statement	lemma 7.29	arxiv
Shift Weakening	statement	lemma 3.4	arxiv
Semantic Substitution Equality	definition	definition 6.30	arxiv
Universe Type Predicate $\textsf{Univ}_{i,j}$	definition	definition 7.11	arxiv
Context PER	definition	definition 6.19	arxiv
Cumulativity	statement	lemma 6.10	arxiv
$q$-Identity	statement	lemma 2.5	arxiv
Symmetry of semantic substitutions	statement	lemma 6.41	arxiv
Neutral Term Predicate $\textsf{Neu}_i^e$	definition	definition 7.6	arxiv
Shift is a Semantic Weakening	statement	lemma 6.28	arxiv
$\textsf{Nat}$ reads back correctly	statement	lemma 6.8	arxiv
Fundamental --- \textsc{Subsump	statement	lemma 6.64	arxiv
Judgment Forms	definition	definition 3.1	arxiv
Semantic --- \textsc{$\Pi$-Wf	statement	lemma 7.39	arxiv
$\textsf{Nat}$ is a PER	statement	lemma 6.7	arxiv
Fundamental --- \textsc{Sub-Trans	statement	lemma 6.71	arxiv
Type Gluing Model $\Uc_i^\ast$	definition	definition 7.4	arxiv
Semantic Subtyping $<:_i$	definition	definition 6.11	arxiv
Symmetry of $\Uc_i$	statement	lemma 6.13	arxiv
Fundamental --- \textsc{Ctx-Emp	statement	lemma 6.50	arxiv
Action of $q^n$ on Substitution Indices	statement	lemma 2.19	arxiv
Identity Weakening	statement	lemma 3.3	arxiv
Normal Form Predicate $\Nf_i^a$	definition	definition 7.13	arxiv
Semantic Subtyping for Contexts	definition	definition 6.20	arxiv
Semantic --- \textsc{$\lambda$-I	statement	lemma 7.42	arxiv
Semantic recursion, one-sided substituted	statement	lemma 6.62	arxiv
Semantic --- \textsc{Ctx-Emp	statement	lemma 7.34	arxiv
Transitivity of semantic subtyping for contexts	statement	lemma 6.24	arxiv
Type-predicate syntactic escape	statement	lemma 7.22	arxiv
Subtyping type-escape	statement	lemma 7.30	arxiv
Semantic Context Well-Formedness	definition	definition 6.33	arxiv
Semantic Judgment for Subtyping	definition	definition 6.32	arxiv
$q^n$ Distributes over Composition	statement	lemma 2.8	arxiv
Double extension by precomposed terms	statement	lemma 6.46	arxiv
Kripke weakening	definition	definition 7.1	arxiv
Transitivity of context PER	statement	lemma 6.23	arxiv
Realizability of the PER model	statement	lemma 6.18	arxiv
Universe PER $\Uc_i$	definition	definition 6.9	arxiv
Semantic --- \textsc{Subsump	statement	lemma 7.46	arxiv
PER membership yields gluing-model membership	statement	lemma 7.28	arxiv
PER $\textsf{Ty}$ --- Types	definition	definition 6.3	arxiv
Fundamental --- \textsc{$\lambda$-I} / \textsc{$\lambda$-Cong	statement	lemma 6.59	arxiv
Initial Environment Validity	statement	lemma 7.33	arxiv
Precomposition with weakening	statement	lemma 6.39	arxiv
Semantic --- \textsc{U-Wf	statement	lemma 7.37	arxiv
Wrapped predicates $\Botp_i^a$ and $\Topp_i^a$	definition	definition 7.15	arxiv
Shift is semantic	statement	lemma 6.37	arxiv
$q$ Preserves Semantic Weakening	statement	lemma 6.43	arxiv
Substitution Equivalence	definition	definition 4.11	arxiv
Structural Properties of $\iota$	statement	lemma 2.15	arxiv
Fundamental --- \textsc{$\Pi$-Wf} / \textsc{$\Pi$-Cong	statement	lemma 6.54	arxiv
Composition of Semantic Weakenings	statement	lemma 6.29	arxiv
Embedding of Weakenings into Substitutions	definition	definition 2.13	arxiv
Fundamental Theorem	statement	theorem 6.73	arxiv
Fundamental --- \textsc{N-$\beta$-Ze	statement	lemma 6.67	arxiv
$q$ Distributes over Composition	statement	lemma 2.7	arxiv
Transitivity of semantic substitutions	statement	lemma 6.42	arxiv
Raw Expressions	definition	definition 2.1	arxiv
Composition of Substitution Application	statement	lemma 2.22	arxiv
Fundamental --- \textsc{Ze-I	statement	lemma 6.57	arxiv
TFRMJ9ZZWJ	definition	definition	arxiv
Semantic --- \textsc{Var	statement	lemma 7.36	arxiv
Neutral Type Predicate $\textsf{Neu}_i^e$	definition	definition 7.5	arxiv
Completeness of NbE	statement	theorem 6.74	arxiv
NbE	definition	definition 5.5	arxiv
Semantic recursion, unsubstituted	statement	lemma 6.61	arxiv
Generalized $q$--Extension Interaction	statement	lemma 2.28	arxiv
Fundamental --- \textsc{Sub-Pi	statement	lemma 6.70	arxiv
Cumulativity of $\Uc_i^\ast$ (subrelation	statement	lemma 7.25	arxiv
Fundamental --- \textsc{Su-I} / \textsc{Su-Cong	statement	lemma 6.58	arxiv
Categorical Laws for Substitutions	statement	lemma 2.29	arxiv
Semantic context well-formedness	definition	definition 7.17	arxiv
Substitution--Extension Commutation	statement	lemma 2.30	arxiv
Fundamental --- \textsc{N-Wf	statement	lemma 6.53	arxiv
Shift--Extension Cancellation	statement	lemma 2.25	arxiv
Pi Term Predicate $\Pi_i^{\El}$	definition	definition 7.10	arxiv
$\Vdash \Gamma$ implies $\vdash \Gamma$	statement	lemma 7.18	arxiv
Composition of Kripke weakenings	statement	lemma 7.3	arxiv
Right irrelevance of context PER	statement	lemma 6.21	arxiv
$\Uc_i^\ast$ closed under $\Uc_i$-equivalence	statement	lemma 7.27	arxiv
Transitivity of $\Uc_i$	statement	lemma 6.14	arxiv
PER $\Ne$ --- Neutral Terms	definition	definition 6.2	arxiv
Gluing implies PER	statement	lemma 7.21	arxiv
Transitivity of $<:_i$	statement	lemma 6.16	arxiv
Subtyping term-transfer	statement	lemma 7.31	arxiv
Equivalent Substitutions Preserve Judgments	statement	lemma 4.13	arxiv
Single Substitution is Well-Typed	statement	lemma 4.4	arxiv
Composition of Weakening Application	statement	lemma 2.9	arxiv
Fundamental --- \textsc{U-Wf	statement	lemma 6.52	arxiv
Lookup at fixed instantiation	statement	lemma 6.55	arxiv
Context Gluing	definition	definition 7.16	arxiv
Identity Instantiation of Semantic Typing	statement	lemma 6.38	arxiv

Catalogue records

arxiv: 2610.21131 (work)