Nova Foundation

Rendered from docs/NovaFoundation.txt — the plain text remains the source of truth.

fixed syntax
⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ let → ⨯ ⊎ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class inj₁ inj₂ ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim ⊎-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath ν 𝕏 K out corec poly map Code Id refl univ el eq pi sigma zero one nat 𝒱 ↦ ≅ Con Sub Ty Tm Var Trk emb ty ◇ Id refl 𝒱 ↦ ≅ ⟨ ⟩ var vz vs lam app pair
ToS metavariables
𝔄 𝔅 𝕥 𝕦 𝕧 𝕤 𝕔 𝕜 𝕘 𝕒 𝕓 𝕞 Φ 𝒮 ς 𝔎 𝔽 𝔾
Nova metavariables
Γ Δ Ξ Σ σ τ δ θ+ any bare Latin letter (t₀, A′, ē)
walk / certificate metavariables
𝑤 ρ υ π 𝒞 ℰ γ 𝒢
meta-level naturals (indices)
ₙ₊₁
links to its rule
rule-name
comment, unhighlighted
# prose

Preface

(`#!` lines are HIGHLIGHTING DECLARATIONS read by tools/render-specs.py — the spec declares its own syntax tables: `keywords` is the FIXED syntax, judgement-level (⊦ : ≐ type …) and object-level (⬡ ▷ El ☐ λ → …) alike, rendered gold; the remaining classes are the METAVARIABLE alphabets by kind — ToS, Nova (`latin` marks bare Latin letters as Nova metavariables inside judgements), and the reflection/walk apparatus. Tokens in no table render ink. They carry no theory content.)

This file contains a formalisation of Nova's type theory: Extensional Computational Type Theory. The presentation is by inference rules over a first-order grammar, and its OFFICIAL reading is INTRINSIC (https://ncatlab.org/nlab/show/intrinsic+and+extrinsic+views+of+typing): the judgements are simultaneously-defined sorts, the rules their constructors, and a term exists only at its type — the grammar below is notation for constructor shapes, not a prior universe of raw terms that typing then carves. docs/NovaSyntax.txt makes this reading precise (a quotient inductive-inductive-recursive definition) for a fragment, and classifies where every rule class lands in it.

Semantics is assigned by the SETOID MODEL: a type denotes a structural CODE together with a proof-irrelevant equivalence relation on the code's decoding — type equality is equality of codes, element equality is the relation. docs/NovaModel.txt constructs the code layer for the structural fragment; the relation layer is where quotients, Ω-truth and the QIIT congruences live (see the SEMANTICS notes at their rules).

NOTE: well-typed terms need not normalize in an inconsistent context. Equality reflection makes typability hypothesis-sensitive: e.g. under Γ ∋ h : Prf (A ≡ (A → A) ∈ 𝕌), reflection gives El A ≐ El A → El A, so self-application types and ω ω is well-formed at El A, where ω ≜ λx. x x — yet ω ω has no normal form. Normalization is therefore a property of terms in consistent contexts only; any procedure that beta-normalizes a well-formed term (as the checker does when storing and comparing facts) may diverge under inconsistent hypotheses. This is a liveness caveat, not a soundness one: a non-terminating normalization never certifies a judgement.

Type Theory

We have:

  • Empty type: 𝟘
  • Unit type: 𝟙
  • Natural numbers type: ℕ
  • Dependent product type: (→)
  • Dependent sum type: (⨯)
  • Non-dependent sum type: (⊎) — the disjoint union, with injections inj₁/inj₂ and a dependent eliminator ⊎-elim (β on each injection, uniqueness η in el-nat-eta's style). DEFINABLE as a QIIT (a two-point signature — see SUBSUMPTION in the QIIT notes); retained as a standalone former, like ℕ and (/)
  • Equality proposition: (≡), Ω-valued, with reflection — used through Prf; proof-irrelevant by el-prf-prop (see the Ω block)
  • Quotient type: (/), by an Ω-valued relation
  • A predicative universe: 𝕌
  • A universe of mere propositions: Ω (squash ∥-∥, propositional extensionality)
  • Quotient inductive-inductive types (QIITs): a SCHEME (not a single former) — for each well-formed signature 𝒮 (mutually-defined, possibly index-dependent sorts with point AND equation (path) constructors), the sorts 𝒮.𝕤 ē as types, their constructors 𝒮.𝕔 θ, the imposed path equations, and a dependent eliminator 𝒮.𝕤-elim with its computation and uniqueness laws. Every rule is stated against a signature (no Σ-entry; 𝒮 is carried by the formers). This subsumes ℕ, (⊎) and (/) (each a one- or two-line signature), including indexed inductive types and quotient inductive types as special cases; its equation constructors are INDUCTIVE (they may relate constructor terms across indices and participate in the induction). ℕ, (⊎) and (/) are retained for now.
  • Coinductive types: a second SCHEME, dual to QIITs in its smallest useful form — for each POLYNOMIAL 𝔽 (a one-hole strictly positive code), the type ν 𝔽, its observation out (the eliminator), its corecursor corec (the introduction), β running one observation step, and a uniqueness law that is the coinduction principle (bisimulation implies equality). Every ν 𝔽 is DERIVABLE (an ℕ-indexed limit — see SUBSUMPTION in the coinductive notes); the scheme is kept for structural identity and one-step β.

Syntax

signature identifier

x ::= <signature-entry-identifier>

signature context

Σ ::= ε
    | Σ (Γ  x  a : A)     # term definition
    | Σ (Γ  x  T type)    # type definition
    | Σ (Γ  x : A)         # term declaration (a HOLE — no definiens)
    | Σ (Γ  x type)        # type declaration
    | Σ (Γ  a  a : A)     # element equation constraint (nameless)
    | Σ (Γ  T  T type)    # type equation constraint (nameless)

typing context

Γ ::= ε      # empty typing context
    | Γ  T  # extended typing context

A defined (meta-level) notion Γ‖ₙ: the (n+1)-th type in Γ counting from the right (0 = the innermost extension), i.e. the type ☐ₙ names before weakening.

(Γ  A)      A[]
(Γ  A)ₙ₊₁    Γ[]

typing context substitution

σ, τ ::=
       ·             # empty substitution
     | σ, t          # extension substitution
     | σ  σ         # composition substitution
     | id            # identity substitution
     |              # weakening substitution

typing context normal substitution

, ,  ::= · | , t

type

T ::= x []         # type in the signature context
    | 𝟘
    | 𝟙
    | 
    | 𝕌              # predicative universe
    | Ω              # universe of mere propositions
    | T  T          # dependent product type (Π)
    | T  T          # dependent sum type (Σ)
    | T  T          # non-dependent sum type (disjoint union)
    | El t           # Every element of the universe is a type
    | T / t          # quotient type (t an Ω-valued relation)
    | Prf t          # decoding of a proposition (Ω's El; deliberately not
                     #   written El: it shares none of El's rules — not
                     #   structural, not injective, no decoding computation)
    | 𝒮.𝕤 ē          # sort 𝕤 of a QIIT signature 𝒮 at index spine ē
                     #   (see "Quotient inductive-inductive types"); 𝒮 is
                     #   carried in the type, so QIIT equality is structural
    | ν 𝔽            # coinductive type at polynomial 𝔽 (see "Coinductive
                     #   types"); 𝔽 is carried in the type, so ν-equality
                     #   is structural

element

t ::= x []         # element in the signature context
    |              # i-th element in the typing context
    | λ t            # dependent product type introduction
    | t t            # dependent product type elimination
    | let t t        # let-expression (definiens, body — the body
                     #   binds the definiens AND its unfolding
                     #   equation; see the let block)
    | t , t          # dependent sum type introduction
    | t .π₁          # dependent sum type elimination (1)
    | t .π₂          # dependent sum type elimination (2)
    | inj₁ t         # non-dependent sum type introduction (left)
    | inj₂ t         # non-dependent sum type introduction (right)
    | ⊎-elim t t t   # non-dependent sum type elimination
                     #   (left case, right case, eliminee)
    | 𝟘              # element of the universe
    | 𝟙              # element of the universe
    |               # element of the universe
    | t  t          # element of the universe (encodes Π)
    | t  t          # element of the universe (encodes Σ)
    | t  t          # element of the universe (encodes ⊎)
    | t  t  T      # equality PROPOSITION — an Ω-element; T an
                     #   arbitrary TYPE, so equality props exist at
                     #   large types (see the Ω block)
    | t / t          # element of the universe (encodes quotient)
    | 𝟘-elim t
    | ()             # the only element of 𝟙
    | Z
    | S t
    | ℕ-elim t t t
    | class t        # quotient type introduction
    | quot-elim t t  # quotient type elimination
    | T            # squash: proposition from an arbitrary type (an element
                     #   form embedding a type — the converse direction of El)
    |               # the canonical proof of a true proposition
    | 𝒮.𝕤 ē          # universe code for the sort 𝕤 of a SMALL 𝒮 at ē
    | 𝒮.𝕔 θ          # POINT constructor 𝕔 of 𝒮, SATURATED: θ a full
                     #   argument spine, like every other former
                     #   (equation constructors mint no term: their
                     #   content is a judgement — see el-qiit-path)
    | 𝒮.𝕤-elim  ē t # QIIT eliminator (elimination problem ℰ, indices ē,
                     #   eliminee t) — see the QIIT section
    | ν 𝔽            # universe code for the coinductive type at 𝔽
                     #   (every polynomial is small — see "Coinductive types")
    | out t          # coinductive observation (the ELIMINATOR)
    | corec 𝔽 t t t  # corecursor (the INTRODUCTION: polynomial, carrier
                     #   code, coalgebra body, seed — 𝔽 and the carrier are
                     #   CARRIED, like ℰ at 𝒮.𝕤-elim: el-nu-beta consumes
                     #   map_𝔽, so the redex must be self-contained)

(type) telescope

Δ ::= ε | T  Δ

(element) spine

ē ::= · | e, ē

Conventions: how to read the rules

The rules below are presented COMPACTLY. Each convention comes with its mechanical expansion, so the fully explicit form of every rule is recoverable without judgement calls. (The previous fully-explicit presentation additionally carried, with every rule, an argument-labelling scheme consumed by the since-removed .rules derivation checker; that interface lives on in git history only.)

  • AMBIENT SIGNATURE. Every judgement is relative to a signature Σ, presupposed well-formed. The Σ prefix and the premise `Σ sig` are omitted everywhere; rules that inspect or extend Σ (the sig rules, the x[e˲] rules) name it explicitly. Expansion: prefix every judgement with `Σ ⊦`/`Σ Γ ⊦` as appropriate and add `Σ sig` as the first premise of every rule.
  • PRESUPPOSITIONS. Each judgement form PRESUPPOSES the well-formedness of its parts, as listed in the judgement-form table below. A rule omits every premise that lies in the presupposition CLOSURE of its retained premises and its conclusion (the closure: start from the retained premises and the conclusion, add their presuppositions, and close transitively). Expansion: add the closure back as explicit premises — this recovers the previous exhaustive style, where e.g.
  `Γ  A  f : B` was always accompanied by `Γ ctx`, `Γ  A type` and
  `Γ  A  B type`. Premises NOT in the closure are never omitted: in

particular eliminator motives, the middle subject of a transitivity, and the data of the coercion rules are genuine inputs and always appear.

  • GROUPED CONCLUSIONS. A rule with several conclusions below the line abbreviates one rule per conclusion (same premises).
  • EQUIVALENCE RULES. Each of the seven equality judgements —
    Γ₀  Γ₁ ctx                 (contexts)
    σ₀  σ₁ : Γ  Δ             (substitutions)
    e˲₀  e˲₁ : Γ  Δ norm      (normal substitutions)
    Γ  A₀  A₁ type            (types)
    Γ  a₀  a₁ : A             (elements)
    Γ  Δ₀  Δ₁ tel             (telescopes)
    Γ  ē₀  ē₁ : Δ             (element lists)

— is governed by three rules adopted once here and not repeated per class. Writing J for the well-formedness form and J⁼ for the equality form of a class:

    J(a)              J⁼(a₀  a₁)          J⁼(a₀  a₁)   J⁼(a₁  a₂)
    ----------(refl)  -----------(sym)     ------------------------(trans, via a₁)
    J⁼(a  a)         J⁼(a₁  a₀)          J⁼(a₀  a₂)

(transitivity's middle subject a₁, with J(a₁), is an input of the rule). Instances are named ctx-refl, ctx-sym, ctx-trans, sub-refl, ..., sp-trans. Consequently the pointwise equality rules for constants and atoms (ε ≐ ε ctx, id ≐ id, ↑ ≐ ↑, · ≐ ·, x[e˲] ≐ x[e˲], ...) are refl instances and are not stated.

  • DEFINITIONAL EQUALITY. A rule concluding J ≜ K asserts the corresponding ≐-judgement and additionally marks it as a computation step, oriented left to right. Its presuppositions are those of the underlying ≐ form.
  • NAMES. Every rule carries a canonical name on its inference line, following one homogeneous scheme — <class>-<former>-<kind> — where the class is the judgement class (ctx, sub, sub-norm, ty, el, code, poly, tel, sp), the former names the connective or constructor, and the kind distinguishes introduction (i), elimination (e), computation (beta), uniqueness (eta), congruence (cong), injectivity (inj), substitution action (sub), and coercion (coe). These names are the ones docs/NovaKernel.txt and docs/NovaElaboration.txt cite; there are no synonyms.

Judgement forms and their presuppositions

  Form                         Presupposes
  --------------------------   ------------------------------------
  Σ sigΓ ctxΓ₀  Γ₁ ctx                  Γ₀ ctx;  Γ₁ ctx
  σ : Γ  Δ                    Γ ctx;  Δ ctx
  σ₀  σ₁ : Γ  Δ              σ₀ : Γ  Δ;  σ₁ : Γ  Δ
   : Γ  Δ norm              Γ ctx;  Δ ctx
  e˲₀  e˲₁ : Γ  Δ norm       e˲₀ : Γ  Δ norm;  e˲₁ : Γ  Δ norm
  Γ  A type                   Γ ctx
  Γ  A₀  A₁ type             Γ  A₀ type;  Γ  A₁ type
  Γ  a : A                    Γ  A type
  Γ  a₀  a₁ : A              Γ  a₀ : A;  Γ  a₁ : A
  Γ  Δ tel                    Γ ctx
  Γ  Δ₀  Δ₁ tel              Γ  Δ₀ tel;  Γ  Δ₁ tel
  Γ  ē : Δ                    Γ  Δ tel
  Γ  ē₀  ē₁ : Δ              Γ  ē₀ : Δ;  Γ  ē₁ : Δ
  Γ  Φ qctx                   Γ ctx        (qiit-context)
  Γ ; Φ  𝔄 qty                Γ  Φ qctx   (qiit-type)
  Γ ; Φ  𝕥 : 𝔄                Γ ; Φ  𝔄 qty (qiit-term)
  Γ  ς : Φ₀  Φ₁              Γ  Φ₀ qctx;  Γ  Φ₁ qctx   (qiit-substitution)
  Γ  𝒮 qsig                   Γ ctx        (QIIT signature;  Γ  𝒮 qctx)
  Γ   : 𝒮 mot                Γ  𝒮 qsig   (motive family)
  Γ   : 𝒮 dalg               Γ  𝒮 qsig   (displayed algebra,  =  ; )
  Γ   : 𝒮 eprob              Γ   : 𝒮 dalg   (elimination problem)
  Γ  φ :  sect               Γ   : 𝒮 mot    (section candidate)
  Γ  𝔽 poly                   Γ ctx        (polynomial — see "Coinductive types")
  # the theory-of-signatures judgements (dual zone Γ ; Φ — Nova zone,
  # then ToS zone) are defined in the QIIT section; a signature is
  # nothing but a well-formed qiit-context. Like signatures,
  # polynomials are inert syntax with no equality judgement of their
  # own: they are compared structurally, per IDENTITY in each scheme's
  # section.

A context extension Γ ▷ A presupposes Γ ctx and Γ ⊦ A type, so a premise stated under Γ ▷ A carries A's well-formedness with it (and likewise for iterated extensions).

Rules (sig)

ε sig
Σ Γ  a : A
xΣ
Σ (Γ  x  a : A) sig
Σ Γ  A type
xΣ
Σ (Γ  x  A type) sig
Σ Γ  A type
xΣ
Σ (Γ  x : A) sig
Σ Γ ctx
xΣ
Σ (Γ  x type) sig
Σ Γ  a₀ : A
Σ Γ  a₁ : A
Σ (Γ  a₀  a₁ : A) sig
Σ Γ  A₀ type
Σ Γ  A₁ type
Σ (Γ  A₀  A₁ type) sig

DEFINITIONAL AND OPEN SIGNATURES

A signature is DEFINITIONAL when every entry is a definition (sig-def/sig-ty-def). The other entry kinds make it OPEN: a DECLARATION is a hole — a name with a type and no definiens, whose references x[e˲] are STUCK (el-sig-decl / ty-sig-decl below; deliberately no -beta) — and a CONSTRAINT is an assumed equation, used through el-sig-eq/ty-sig-eq exactly like a definitional equality. Open signatures are the working states of an elaboration run (docs/NovaElaboration.txt): the declarations and constraints of the run's signature ARE its open proof obligations, and a run is ACCEPTED only once its signature is definitional.

The canonical-forms semantics below reads over definitional signatures only. An open signature denotes the CLASS of its definitional REFINEMENTS — the signatures obtained by instantiating every declaration and discharging every constraint (the two admissible principles next); every judgement derived over the open signature holds over each refinement. The class may be EMPTY (a hole at Prf ∥𝟘∥, a constraint Z ≐ S Z : ℕ): judgements under unsatisfiable assumptions carry no absolute content — which is why acceptance demands a definitional signature and nothing weaker.

Both refinement principles are META-THEOREMS (by induction on derivations), not rules of the theory — the workflow they justify is edit-and-rerun, never an in-place signature surgery:

  • INSTANTIATION (signature cut). If Σ (Γ ⊦ x : A) Σ' ⊦ J and Σ Γ ⊦ t : A — the filling term lives in the PREFIX preceding the hole — then Σ Σ'[t/x] ⊦ J[t/x], where [t/x] replaces every reference x[e˲] by t[e˲]. Ditto for a type declaration filled by Σ Γ ⊦ T type. The IN-PLACE variant needs no substitution at all: Σ (Γ ⊦ x ≔ t : A) Σ' ⊦ J follows directly, since every rule that applied to the declaration entry has its conclusion re-derivable from the definition entry (el-sig-decl's conclusion is el-sig-var's) and no rule depends on x LACKING a body — the flip
  only refines, adding the equations x[]  t[].
  • DISCHARGE. If Σ (Γ ⊦ a₀ ≐ a₁ : A) Σ' ⊦ J and Σ Γ ⊦ a₀ ≐ a₁ : A — the constraint is DERIVABLE in its prefix — then Σ Σ' ⊦ J: the entry deletes, every el-sig-eq use of it being derivable outright. Ditto for type constraints via ty-sig-eq.

Substitution action is uniform in the entry kind: the -sub-sig-var rules (ty-sub-sig-var, el-sub-sig-var), stated below for definitions, are adopted verbatim for declarations — x[e˲][σ] ≜ x[e˲ ∘ σ] whichever entry x names.

Rules (ctx)

ε ctx
Γ  A type
Γ  A ctx
Γ₀  Γ₁ ctx
Γ₁  A₀  A₁ type
Γ₀  A₀  Γ₁  A₁ ctx

Rules (ctx substitution)

Γ ctx
· : Γ  ε
σ : Γ  ε
σ  · : Γ  ε
σ : Γ₀  Γ₁
Γ₀  t : A[σ]
sub-ext# A the type over Γ₁ being extended by
(σ, t) : Γ₀  Γ₁  A
σ : Γ₀  Γ₁
τ : Γ₁  Γ₂
sub-comp# via Γ₁
τ  σ : Γ₀  Γ₂
Γ ctx
id : Γ  Γ
Γ  A type
 : Γ  A  Γ
id  · : ε  ε
Γ  A type
sub-eta# admissible by meta-level induction
,   id : Γ  A  Γ  A
σ : Γ₀  Γ₁
σ  id  σ : Γ₀  Γ₁
σ : Γ₀  Γ₁
id  σ  σ : Γ₀  Γ₁
σ₁₀ : Γ₁  Γ₀
σ₂₁ : Γ₂  Γ₁
σ₃₂ : Γ₃  Γ₂
σ₁₀  (σ₂₁  σ₃₂)  (σ₁₀  σ₂₁)  σ₃₂ : Γ₃  Γ₀
σ : Γ₀  Γ₁
Γ₀  t : A[σ]
sub-wk-ext# weakening cancels a just-added extension
  (σ, t)  σ : Γ₀  Γ₁
σ : Γ₀  ε
sub-empty-comp# admissible
·  σ  · : Γ₀  ε
τ : Γ₀  Γ₁
σ : Γ₁  Γ₂
Γ₁  t : A[σ]
sub-ext-post# admissible
(σ, t)  τ  (σ  τ, t[τ]) : Γ₀  Γ₂  A
σ : Γ₀  Γ₁
Γ₁  A type
sub-lift# natural substitution (admissible)
σ  (σ  , ) : Γ₀  A[σ]  Γ₁  A
σ : Γ₀  Γ₁
Γ₀  t : A[σ]
τ : Γ₀  Γ₁  A
  τ  σ : Γ₀  Γ₁
Γ₀  [τ]  t : A[  τ]
sub-ext-unique# admissible
(σ, t)  τ : Γ₀  Γ₁  A
∎ (=>) τ  id  τ  (, )  τ    τ, [τ]  σ, t
  (<=)
      σ    (σ, t)    τ
      t  [σ, t]  [τ]
σ₀  σ₁ : Γ₀  Γ₁
τ₀  τ₁ : Γ₁  Γ₂
sub-comp-cong# via Γ₁
τ₀  σ₀  τ₁  σ₁ : Γ₀  Γ₂
σ₀  σ₁ : Γ₀  Γ₁
Γ₀  t₀  t₁ : A[σ₁]
(σ₀, t₀)  (σ₁, t₁) : Γ₀  Γ₁  A
Γ₀  Γ₁ ctx
σ : Γ₀  Δ
σ : Γ₁  Δ
Δ₀  Δ₁ ctx
σ : Γ  Δ₀
σ : Γ  Δ₁
Γ  Γ' ctx
σ  τ : Γ  Δ
σ  τ : Γ'  Δ
Δ  Δ' ctx
σ  τ : Γ  Δ
σ  τ : Γ  Δ'

Rules (normal substitution)

Γ ctx
· : Γ  ε norm
 : Γ  ε norm
  · : Γ  ε norm
 : Γ₀  Γ₁ norm
Γ₀  t : A[]
sub-norm-ext# A the type over Γ₁ being extended by
(, t) : Γ₀  Γ₁  A norm
e˲₀  e˲₁ : Γ₀  Γ₁ norm
Γ₀  t₀  t₁ : A[e˲₁]
(e˲₀, t₀)  (e˲₁, t₁) : Γ₀  Γ₁  A norm
 : Γ₀  Γ₁ norm
sub-norm-embed# a normal substitution is a substitution
 : Γ₀  Γ₁
 : Γ₀  Γ₁ norm
σ : Δ  Γ₀
sub-norm-comp# via Γ₀ defined by meta-level induction:
  σ : Δ  Γ₁ norm
    ·  σ  ·
    (, t)  σ  (  σ, t[σ])
e˲₀  e˲₁ : Γ₀  Γ₁ norm
σ : Δ  Γ₀
e˲₀  σ  e˲₁  σ : Δ  Γ₁ norm
Γ₀  Γ₁ ctx
 : Γ₀  Δ norm
 : Γ₁  Δ norm
Δ₀  Δ₁ ctx
 : Γ  Δ₀ norm
 : Γ  Δ₁ norm
Γ  Γ' ctx
   : Γ  Δ norm
   : Γ'  Δ norm
Δ  Δ' ctx
   : Γ  Δ norm
   : Γ  Δ' norm

Rules (type)

Γ ctx
Γ  𝟘 type
ty-zero
Γ  𝟙 type
ty-one
Γ   type
ty-nat
Γ  𝕌 type
ty-univ
Γ  Ω type
ty-prop
Γ  A type
Γ  A  B type
Γ  A  B type
Γ  A type
Γ  A  B type
Γ  A  B type
Γ  A type
Γ  B type
ty-sum# non-dependent: B over Γ, not Γ ▷ A
Γ  A  B type
Γ  A : 𝕌
Γ  El A type
Γ  p : Ω
Γ  Prf p type
Γ  A type
Γ  A  A[]  R : Ω
Γ  A / R type
(Γ  x  A type)  Σ
 : Δ  Γ norm
Σ Δ  x[] type
(Γ  x  A type)  Σ
 : Δ  Γ norm
Σ Δ  x[]  A[] type

Open-signature references: a type declaration types its references but never unfolds them (no -beta — the reference is stuck); a type constraint is used as a definitional equality.

(Γ  x type)  Σ
 : Δ  Γ norm
Σ Δ  x[] type
(Γ  A₀  A₁ type)  Σ
 : Δ  Γ norm
Σ Δ  A₀[]  A₁[] type

El-decoding: El of a code computes to the type it encodes.

Γ ctx
Γ  El 𝟘  𝟘 type
ty-el-zero
Γ  El 𝟙  𝟙 type
ty-el-one
Γ  El    type
ty-el-nat
Γ  A : 𝕌
Γ  El A  B : 𝕌
Γ  El (A  B)  El A  El B type
Γ  A : 𝕌
Γ  El A  B : 𝕌
Γ  El (A  B)  El A  El B type
Γ  A : 𝕌
Γ  B : 𝕌
Γ  El (A  B)  El A  El B type
Γ  A : 𝕌
Γ  El A  (El A)[]  R : Ω
Γ  El (A / R)  El A / R type

Substitution action on types: A[σ] is defined by meta-level induction on A via the ≜-equations below.

Γ₁  A type
σ : Γ₀  Γ₁
Γ₀  A[σ] type
Γ  A type
ty-sub-id# true on the nose by induction on A
Γ  A[id]  A type
Γ₂  A type
σ : Γ₁  Γ₂
τ : Γ₀  Γ₁
ty-sub-comp# true on the nose by induction on A
Γ₀  A[σ  τ]  A[σ][τ] type
σ : Γ₀  Γ₁
Γ₀  𝟘[σ]  𝟘 type
Γ₀  𝟙[σ]  𝟙 type
Γ₀  [σ]   type
Γ₀  𝕌[σ]  𝕌 type
Γ₀  Ω[σ]  Ω type
Γ₁  t : 𝕌
σ : Γ₀  Γ₁
Γ₀  (El t)[σ]  El t[σ] type
Γ₁  p : Ω
σ : Γ₀  Γ₁
Γ₀  (Prf p)[σ]  Prf p[σ] type
Γ₁  A type
Γ₁  A  B type
σ : Γ₀  Γ₁
Γ₀  (A  B)[σ]  A[σ]  B[σ] type
Γ₁  A type
Γ₁  A  B type
σ : Γ₀  Γ₁
Γ₀  (A  B)[σ]  A[σ]  B[σ] type
Γ₁  A type
Γ₁  B type
σ : Γ₀  Γ₁
Γ₀  (A  B)[σ]  A[σ]  B[σ] type
Γ₁  A type
Γ₁  A  A[]  R : Ω
σ : Γ₀  Γ₁
Γ₀  (A / R)[σ]  A[σ] / R[σ] type
(Γ  x  A type)  Σ
 : Γ₁  Γ norm
σ : Γ₀  Γ₁
Σ Γ₀  x[][σ]  x[  σ] type
Γ  A type
Γ  B type
Γ  t : 𝟘
ty-zero-elim# type equality from absurdity
Γ  A  B type
Γ₀  Γ₁ ctx
Γ₀  A type
Γ₁  A type
Γ₀  Γ₁ ctx
Γ₀  A  B type
Γ₁  A  B type
Δ  A₀  A₁ type
σ₀  σ₁ : Γ  Δ
Γ  A₀[σ₀]  A₁[σ₁] type
Δ  A₀  A₁ type
σ : Γ  Δ
ty-sub-cong-fix# admissible: specialize via sub-refl
Γ  A₀[σ]  A₁[σ] type
Γ  A₀  A₁ type
Γ  A₁  B₀  B₁ type
Γ  A₀  B₀  A₁  B₁ type
Γ  A₀  A₁ type
Γ  A₁  B₀  B₁ type
Γ  A₀  B₀  A₁  B₁ type
Γ  A₀  A₁ type
Γ  B₀  B₁ type
Γ  A₀  B₀  A₁  B₁ type
Γ  A₀  A₁ type
Γ  A₁  A₁[]  R₀  R₁ : Ω
Γ  A₀ / R₀  A₁ / R₁ type
Γ  t₀  t₁ : 𝕌
ty-el-cong# El congruence: equal codes decode to equal types
Γ  El t₀  El t₁ type
Γ  p₀  p₁ : Ω
ty-prf-cong# with code-prop-eq this is where iff becomes ≐
Γ  Prf p₀  Prf p₁ type

Type constructor injectivity

The congruence rules above run downward: equal components give equal composites. The rules below run upward: equal composites give equal components. They are NOT derivable from the rest of the theory — in the plain set-theoretic model (types as sets, function types as sets of graphs) the hypothesis h : Prf ((𝟙 → 𝟘) ≡ (ℕ → 𝟘) ∈ 𝕌) is satisfiable (both function spaces are the empty set), yet 𝟙 ≐ ℕ is refuted, so before these rules the composite equality was derivable in a context where the component equality was not. Adding them is a semantic commitment, and it is the one this file's preface already makes: a type denotes a structural CODE (docs/NovaModel.txt's code universes), so two Π-types are equal exactly when their heads and components are — the rules are the meta's ordinary constructor injectivity, read back through the interpretation — and likewise for the other formers. Under that semantics these rules are sound; models that collapse structurally distinct types (the set-theoretic one above) are hereby excluded, and the code-universe model shows the exclusion is not vacuous: all the rules hold in it at once (NovaModel's soundness notes). A concrete consequence: a context hypothesizing (𝟙 → 𝟘) ≡ (ℕ → 𝟘) ∈ 𝕌 is now INCONSISTENT (𝟙 ≐ ℕ gives Z ≐ S Z : ℕ via el-one-prop and coercion, and a ℕ-elim discriminator into 𝕌 turns that into an inhabitant of 𝟘).

Notes:

  • The codomain/relation components are concluded UNDER the domain — this is what keeps the rules compatible with empty-domain collapses (𝟘 → 𝟙 ≐ 𝟘 → ℕ is harmless: under a 𝟘-hypothesis the component 𝟙 ≐ ℕ is derivable by absurdity anyway).
  • Quotient relations are Ω-valued, so the relation components are compared at Ω, where judgemental equality IS logical equivalence (code-prop-eq). Quotient type equality therefore coincides with NuPRL's iff-based one — obtained through structural rules rather than a bespoke clause. This does not compromise 𝕌's structural discipline: 𝕌 is structural in its FORMERS and extensional in its element slots (≐ on elements is extensional via reflection); the Ω-slot in code-quot is the same pattern.
  • class stays NON-injective: class a ≐ class b : A / R does not entail a ≐ b — that is the entire point of quotients.
  • Prf and ∥-∥ likewise have NO injectivity rules: Ω is the anti-structural universe, compared by inhabitation alone (see the Ω block in the element rules). Equality is Ω-VALUED, so it inherits this: there is no eq-injectivity — code-prop-eq makes (Z ≡ Z ∈ ℕ) ≐ (S Z ≡ S Z ∈ ℕ) : Ω (both true), while the endpoint equalities Z ≐ S Z are refutable.
  • No-confusion (a Π-type is never equal to ℕ, a Σ-type, ...) is NOT expressible as a rule of this positive inference system, and in inconsistent contexts it is false. It remains a meta-property of consistent contexts, inherited from the meta's no-confusion for the code universes (docs/NovaModel.txt).
  • S-injectivity and pair-injectivity need no rules: they are already derivable (congruence with a ℕ-elim predecessor, respectively the projections). Ditto inj₁/inj₂-injectivity and -disjointness: injectivity by a ⊎-elim retraction at constant motive A whose right case returns a fixed default (the compared element itself serves), disjointness by a ⊎-elim discriminator at constant motive ℕ (Z left, S Z right) followed by the standard Z ≐ S Z refutation. The TYPE former ⊎ is injective by rule below, like every other structural former.
Γ  A₀  B₀ type
Γ  A₁  B₁ type
Γ  A₀  B₀  A₁  B₁ type
Γ  A₀  A₁ type
Γ  A₁  B₀  B₁ type
Γ  A₀  B₀ type
Γ  A₁  B₁ type
Γ  A₀  B₀  A₁  B₁ type
Γ  A₀  A₁ type
Γ  A₁  B₀  B₁ type
Γ  A₀  B₀  A₁  B₁ type
ty-sum-inj# non-dependent: both
Γ  A₀  A₁ type                              #   components over Γ
Γ  B₀  B₁ type
Γ  A₀  A₀[]  R₀ : Ω
Γ  A₁  A₁[]  R₁ : Ω
Γ  A₀ / R₀  A₁ / R₁ type
Γ  A₀  A₁ type
Γ  A₁  A₁[]  R₀  R₁ : Ω
Γ  El t₀  El t₁ type
Γ  t₀  t₁ : 𝕌

The same principles one level down, for the universe codes: the setoid model gives 𝕌 a structural universe of codes (Code₀ in docs/NovaModel.txt), so the code constructors are injective as elements of 𝕌.

Γ  El a₀  b₀ : 𝕌
Γ  El a₁  b₁ : 𝕌
Γ  a₀  b₀  a₁  b₁ : 𝕌
Γ  a₀  a₁ : 𝕌
Γ  El a₁  b₀  b₁ : 𝕌
Γ  El a₀  b₀ : 𝕌
Γ  El a₁  b₁ : 𝕌
Γ  a₀  b₀  a₁  b₁ : 𝕌
Γ  a₀  a₁ : 𝕌
Γ  El a₁  b₀  b₁ : 𝕌
Γ  a₀  b₀  a₁  b₁ : 𝕌
Γ  a₀  a₁ : 𝕌
Γ  b₀  b₁ : 𝕌
Γ  El a₀  (El a₀)[]  r₀ : Ω
Γ  El a₁  (El a₁)[]  r₁ : Ω
Γ  a₀ / r₀  a₁ / r₁ : 𝕌
Γ  a₀  a₁ : 𝕌
Γ  El a₁  (El a₁)[]  r₀  r₁ : Ω

Rules (tel)

Γ ctx
Γ  ε tel
Γ  A type
Γ  A  Δ tel
Γ  A  Δ tel
Γ  A₀  A₁ type
Γ  A₁  Δ₀  Δ₁ tel
Γ  A₀  Δ₀  A₁  Δ₁ tel
Γ₁  Δ tel
σ : Γ₀  Γ₁
tel-sub# defined by meta-level induction on Δ
Γ₀  Δ[σ] tel
σ : Γ₀  Γ₁
Γ₀  ε[σ]  ε tel
Γ₁  A type
Γ₁  A  Δ tel
σ : Γ₀  Γ₁
Γ₀  (A  Δ)[σ]  A[σ]  Δ[σ] tel
Γ₀  Γ₁ ctx
Γ₀  Δ tel
Γ₁  Δ tel
Γ₀  Γ₁ ctx
Γ₀  Δ₀  Δ₁ tel
Γ₁  Δ₀  Δ₁ tel
Γ  Δ₀  Δ₁ tel
σ₀  σ₁ : Ξ  Γ
Ξ  Δ₀[σ₀]  Δ₁[σ₁] tel

Rules (elem)

Γ ctx
el-var# Γ‖ₙ picks the type directly out of Γ's own structure — no
Γ   : Γ                # derivation of ☐ₙ₋₁, ☐ₙ₋₂, ... is required first.

Universe codes.

Γ ctx
Γ  𝟘 : 𝕌
code-zero
Γ  𝟙 : 𝕌
code-one
Γ   : 𝕌
code-nat
Γ  A : 𝕌
Γ  El A  B : 𝕌
Γ  A  B : 𝕌
Γ  A : 𝕌
Γ  El A  B : 𝕌
Γ  A  B : 𝕌
Γ  A : 𝕌
Γ  B : 𝕌
Γ  A  B : 𝕌
Γ  A : 𝕌
Γ  El A  (El A)[]  R : Ω
Γ  A / R : 𝕌

𝟘 and 𝟙.

Γ  A type
Γ  t : 𝟘
Γ  𝟘-elim t : A
Γ  t₀ : 𝟘
Γ  t₁ : 𝟘
Γ  t₀  t₁ : 𝟘
Γ ctx
Γ  () : 𝟙
Γ  t₀ : 𝟙
Γ  t₁ : 𝟙
Γ  t₀  t₁ : 𝟙

ℕ.

Γ ctx
Γ  Z : 
Γ  t : 
Γ  S t : 
Γ    A type
Γ  z : A[id, Z]
Γ    A  s : A[  , S ]
Γ  t : 
el-nat-e# motive A
Γ  ℕ-elim z s t : A[id, t]
Γ    A type
Γ  z : A[id, Z]
Γ    A  s : A[  , S ]
Γ  ℕ-elim z s Z  z : A[id, Z]
Γ    A type
Γ  z : A[id, Z]
Γ    A  s : A[  , S ]
Γ  t : 
Γ  ℕ-elim z s (S t)  s[id, t, ℕ-elim z s t] : A[id, S t]
Γ    A type
Γ    f₀ : A
Γ    f₁ : A
Γ  z : A[id, Z]
Γ    A  s : A[  , S ]
Γ  f₀[id, Z]  f₁[id, Z] : A[id, Z]
Γ    f₀[, S ]  s[id, f₀] : A[, S ]
Γ    f₁[, S ]  s[id, f₁] : A[, S ]
Γ  t : 
el-nat-eta# motive A
Γ  f₀[id, t]  f₁[id, t] : A[id, t]              # NOTE: essentially elimination into equality in A

Corollary: f₀[id, t] ≐ ℕ-elim z s t ≐ f₁[id, t] : A[id, t]

Π.

Γ  A  f : B
Γ  λ f : A  B
Γ  A  B type
Γ  f : A  B
Γ  e : A
Γ  f e : B[id, e]
Γ  A  f : B
Γ  e : A
Γ  (λ f) e  f[id, e] : B[id, e]
Γ  f : A  B
Γ  λ (f[] )  f : A  B

let — the local DEFINITION: the body is typed under TWO binders, the definiens' value and its UNFOLDING EQUATION, so inside b the definiendum unfolds judgementally — el-reflect on ☐₀ gives ☐₁ ≐ a[↑ ∘ ↑] : A[↑ ∘ ↑]. This is a definition-carrying context discipline (Γ ▷ (x ≔ a : A)) with NO new context former: extensionally a definition IS a variable plus a Prf of its unfolding — the same degeneration that collapses the QIIT coherence tower. el-let-beta unfolds the whole expression to the instantiated body, the ⋆ typed by el-eq-i at the reflexive instance a ≡ a, so a let and its unfolding are interchangeable everywhere. NOT a type former — nothing is introduced or eliminated, hence no eta and no injectivity — and DEFINABLE: let a b ≐ ((λ (λ b)) a) ⋆ (two el-pi-beta steps compute the encoding to b[id, a, ⋆]; ty-pi forms its Π-types from the premises' presuppositions). Retained like ℕ and (/) for convenience, not necessity — here the convenience is SYNTACTIC IDENTITY: a local definition should read (and print) as one, not as its λ-plumbing. A body that ignores the equation just weakens past ☐₀ — the "weak" (opaque-binder) let is the special case.

Γ  a : A
Γ  A  Prf (  a[]  A[])  b : B
Γ  let a b : B[id, a, ]
Γ  a : A
Γ  A  Prf (  a[]  A[])  b : B
Γ  let a b  b[id, a, ] : B[id, a, ]

Σ.

Γ  A  B type
Γ  a : A
Γ  b : B[id, a]
Γ  (a , b) : A  B
Γ  t : A  B
Γ  t .π₁ : A
Γ  t : A  B
Γ  t .π₂ : B[id, t .π₁]
Γ  A  B type
Γ  a : A
Γ  b : B[id, a]
Γ  (a, b) .π₁  a : A
Γ  A  B type
Γ  a : A
Γ  b : B[id, a]
Γ  (a, b) .π₂  b : B[id, a]
Γ  t : A  B
Γ  (t .π₁ , t .π₂)  t : A  B

⊎ — the non-dependent sum (disjoint union). Two injections; the eliminator is DEPENDENT (motive C over Γ ▷ A ⊎ B), with β on each injection. Uniqueness (η) is stated as elimination into equality — el-nat-eta's shape: any map out of A ⊎ B that agrees with the case functions on both injections IS the eliminator.

Γ  B type
Γ  a : A
Γ  inj₁ a : A  B
Γ  A type
Γ  b : B
Γ  inj₂ b : A  B
Γ  A  B  C type
Γ  A  l : C[, inj₁ ]
Γ  B  r : C[, inj₂ ]
Γ  t : A  B
el-sum-e# motive C
Γ  ⊎-elim l r t : C[id, t]
Γ  A  B  C type
Γ  A  l : C[, inj₁ ]
Γ  B  r : C[, inj₂ ]
Γ  a : A
Γ  ⊎-elim l r (inj₁ a)  l[id, a] : C[id, inj₁ a]
Γ  A  B  C type
Γ  A  l : C[, inj₁ ]
Γ  B  r : C[, inj₂ ]
Γ  b : B
Γ  ⊎-elim l r (inj₂ b)  r[id, b] : C[id, inj₂ b]
Γ  A  B  C type
Γ  A  B  g : C
Γ  A  l : C[, inj₁ ]
Γ  B  r : C[, inj₂ ]
Γ  A  g[, inj₁ ]  l : C[, inj₁ ]
Γ  B  g[, inj₂ ]  r : C[, inj₂ ]
Γ  t : A  B
el-sum-eta# motive C
Γ  g[id, t]  ⊎-elim l r t : C[id, t]

Corollary (two-candidate form, as at ℕ): two maps out of A ⊎ B that agree on both injections are equal — chain el-sum-eta through the eliminator they both equal.

≡ is Ω-VALUED: formation, introduction and reflection live in the Ω block below, alongside squash — equality is a proposition, used through Prf.

Quotients.

Γ  A  A[]  R : Ω
Γ  a : A
Γ  class a : A / R
Γ  A  A[]  R : Ω
Γ  a : A
Γ  b : A
Γ  r : Prf R[id, a, b]
el-quot-eq# R-related elements have equal classes
Γ  class a  class b : A / R
Γ  (A / R)  B type
Γ  A  f : B[, class ]
Γ  A  A[]  Prf R  f[    , ]  f[    , ] : B[    , class ]
Γ  q : A / R
el-quot-e# motive B
Γ  quot-elim f q : B[id, q]
Γ  (A / R)  B type
Γ  A  f : B[, class ]
Γ  A  A[]  Prf R  f[    , ]  f[    , ] : B[    , class ]
Γ  a : A
Γ  quot-elim f (class a)  f[id, a] : B[id, class a]
Γ  (A / R)  B type
Γ  (A / R)  g : B
Γ  A  f : B[, class ]
Γ  A  A[]  Prf R  f[    , ]  f[    , ] : B[    , class ]
Γ  A  g[, class ]  f : B[, class ]
Γ  q : A / R
el-quot-eta# motive B
Γ  g[id, q]  quot-elim f q : B[id, q]

Ω: equality, squash, proof irrelevance, propositional extensionality.

Ω is a second universe, of mere propositions; its equality discipline is the mirror image of 𝕌's. 𝕌's codes are compared STRUCTURALLY (the injectivity block); Ω's codes are compared by INHABITATION alone (code-prop-eq). Each discipline is sound only on its own side of the fence, so the universes must not mix: there is no code for Ω or for Prf p in 𝕌, and no Ω analogue of any inj rule.

PROPOSITIONAL EQUALITY LIVES HERE

(a₀ ≡ a₁ ∈ A) is an ELEMENT of Ω, not a type (the OTT design — observational equality in a definitionally irrelevant Prop). What this buys, and what it forfeits:

  • Proof irrelevance is inherited from el-prf-prop — no separate el-eq-eta is needed, and equality hypotheses never carry data.
  • The canonical proof is ⋆ — Refl is RETIRED. This is forced, not stylistic: code-prop-eq + ty-prf-cong + el-ty-coe move proofs between iff-equal props UNCHANGED (a true equation is ≐-equal to ∥𝟙∥ at Ω), so every inhabited Prf must have literally the same canonical form.
  • A is an ARBITRARY type: equality props exist at large types (a₀ ≡ a₁ ∈ 𝕌 : Ω), where the old code former could not go.
  • Ω-positions take equations directly — quotient relations need no squash (ℕ ⨯ ℕ / (p q. p .π₁ + q .π₂ ≡ p .π₂ + q .π₁ ∈ ℕ)), and the squashed-equality connective below is subsumed.
  • NO injectivity and NO 𝕌-code, both inherited from Ω's discipline. Losing the code means equational content cannot be STORED in a small type directly; where that is genuinely needed, the prf-code quotient trick below yields an iff-equivalent 𝕌-code (prf (a ≡ b ∈ A)), which is all a proposition can soundly give.

Notes:

  • Realizer irrelevance is FORCED, not chosen: code-prop-eq + ty-prf-cong + el-ty-coe move an element between the decodings of iff-equal props UNCHANGED, which is sound only if those decodings have literally the same canonical forms. So Prf p never exposes the squashed proofs: its one canonical form is ⋆ (cf. NuPRL's Ax), and el-prf-prop equates all members. Consequently there is no Prf-beta — Prf ∥A∥ does NOT reduce to A — and no code-squash-inj / ty-prf-inj: ∥𝟙∥ ≐ (Z ≡ Z ∈ ℕ) : Ω holds by code-prop-eq while the squashees are structurally distinct. Ω adds no computation rules beyond substitution actions; the preface's normalization story is unchanged.
  • Squash is the only way in: ∥-∥ takes an arbitrary TYPE, not a 𝕌-code, so the connectives are signature definitions, not rules — ⊤ ≔ ∥𝟙∥, ⊥ ≔ ∥𝟘∥, p ∧ q ≔ ∥Prf p ⨯ (Prf q)[↑]∥, p ⊃ q ≔ ∥Prf p → (Prf q)[↑]∥, ∀ over A ≔ ∥A → Prf p∥, ∃ over A ≔ ∥A ⨯ Prf p∥ — equality (≡) is the one PRIMITIVE prop beside ∥-∥ (squashing Prf of it is redundant by code-prop-eq). Every other definable prop is ∥-∥-headed, so the eliminators below lose no generality; derived intro/elim principles come from el-squash-i / el-squash-e-* over the underlying former.
  • Elimination goes only into equations and props: a squashed hypothesis may be unsquashed exactly when the goal cannot observe WHICH proof was used — equational goals (judgements do not consult witnesses) and propositional goals (the witness is ⋆ either way). With ≡ Ω-valued, el-squash-e-eq is ADMISSIBLE: equality props exist at every type (large included), so el-eq-i under the binder, el-squash-e-prf and el-reflect derive it. It is kept as a rule for the kernel's convenience. There is deliberately NO eliminator into arbitrary types — el-prf-prop would force it constant, and it would refute witness irrelevance in the model. The eliminators need no congruence rules: their conclusions are equations, respectively ⋆-typings covered by el-prf-prop.
  • IMPREDICATIVITY. ∥-∥ squashes arbitrary types, including quantifications over Ω itself and over 𝕌. This is sound because the candidate denotations of props form a FIXED two-point lattice — the empty and the unit subsingleton setoid — that does not grow with the quantification domain: a universally quantified prop is an infimum in that lattice, witnessed uniformly by ⋆ (precedent: the proof-irrelevant setoid models, where Prop is exactly this lattice; the PER models of CC ran the same argument with realizers). The restrictions above are the license for this; each blocks a known paradox: - proof irrelevance blocks Girard/Hurkens: nothing can be stored in a prop and retrieved for diagonalization (in particular, Church encodings through Ω are sterile — no data can be smuggled past the size restrictions); - no elimination into arbitrary types blocks unique choice / description, and with it the quotient+choice collapses (Chicli–Pottier–Simpson); - no Ω-code in 𝕌 blocks Reynolds/Cantor: A → Ω stays large, so no type contains its own powerset. Note that prf-codes themselves are DERIVABLE from the Ω-valued quotient slot: with Id the QIIT identity family over a small carrier (Id : (x y : El a) ⇛ U ; refl : (x : El a) ⇛ El (Id x x) — a small signature, so Id â t u : 𝕌), take
       prf r  Id ( / ) (class Z) (class (S Z)), a 𝕌-code whose
       decoding is inhabited iff r — el-quot-eq plus el-qiit-intro
       one way, effectivity along (x  y  ) ∨ r plus qiit
       elimination the other. So 𝕌's element slots already contain Ω up to iff,
       and the load-bearing prohibition is exactly the first
       clause: no code for Ω ITSELF. Propositions and powersets
       embed only into the CODES of 𝕌 — a large collection — never
       into the elements of a small type: equality has no 𝕌-code
       at all (it is Ω-valued), El A  𝕌 is large, and
       quotient elements cannot store a proposition (coherence
       forces eliminators out of 𝟙/-style types constant).

Payoff: least relations by intersection — e.g. an equivalence closure r⁺ of an arbitrary relation r, defined by quantifying over all Ω-valued relations containing r — with no inductive machinery. And since code-quot takes its relation at Ω rather than at 𝕌, A / r⁺ is still a 𝕌-code: quotients by generated congruences stay small.

  • Consequences for quotients (whose relation slot is Ω-valued — see ty-quot): 1. Mutually implied relations give EQUAL quotient types:
        code-prop-eq under Γ  A  A[] gives R₀  R₁ : Ω, then
        ty-quot-cong; dually ty-quot-inj returns only iff-content.
        A proof-relevant presentation is recovered as A / R.
     2. Effectivity: for R : Ω over Γ  A  A[], an equivalence
        at squash level, class a  class b : A / R implies
        Prf R[id, a, b] inhabited — via quot-elim at the constant
        motive Ω with f  R[id, a, ], coherence discharged by
        code-prop-eq from symmetry/transitivity, then el-quot-beta,
        ty-prf-cong and el-ty-coe on . Combined with r above this
        characterizes quotient equality for ARBITRARY relations.
     3. Equality proofs reflect directly: el-reflect reads
        a₀  a₁ : B off any s : Prf (a₀  a₁  B) — no squash
        apparatus is involved.
  • SEMANTICS. In the setoid model ⟦Prf p⟧ is a subsingleton setoid: carrier 𝟙 if p is true, 𝟘 otherwise (all elements related either way) — where ∥A∥ is true iff ⟦A⟧'s carrier is inhabited, and (a₀ ≡ a₁ ∈ A) is true iff ⟦a₀⟧ ~ ⟦a₁⟧ in ⟦A⟧'s relation; ∥A∥ ~ ∥B∥ : Ω iff A and B are equi-inhabited. code-prop-eq holds on the nose (iff-equal props have IDENTICAL denotations); el-squash-e-* are validated by instantiating their premise at any carrier element — the conclusion never consults which one. Model note: the prop layer cannot be built by the same stagewise induction as the rest of the type system (the Π-over-Ω clause consults Ω's full domain, non-monotonically); it is instead given IN ADVANCE — the fixed lattice above, with prop-truth defined against the full type system. A two-layer construction, as in the impredicative-Prop setoid models (and, before them, the PER models of CC). The Ω-valued quotient slot adds no further impredicative dependency: the quotient clause consumes Ω-truth POINTWISE (⟦El (A / R)⟧ keeps ⟦El A⟧'s carrier and coarsens its relation by the truth of R at each pair — in the setoid model a quotient is FREE), so quotient codes stay small however impredicative their relation — propositional resizing, in HoTT terms, which the setoid model validates.
Γ  A type
Γ  A : Ω
Γ  a₀ : A
Γ  a₁ : A
code-eq# A an ARBITRARY type — equality
Γ  (a₀  a₁  A) : Ω                 #   props exist at large types
Γ  p : Ω
code-squash-prf# squash is idempotent on
Γ  Prf p  p : Ω                             #   props — an Ω-level ≜,
                                                #   NOT a Prf-decoding
Γ  A₀  A₁ type
Γ  a₀  a₁ : A₁
Γ  b₀  b₁ : A₁
code-eq-cong# admissible via
Γ  (a₀  b₀  A₀)  (a₁  b₁  A₁) : Ω                      #   code-prop-eq +
                                                             #   el-reflect/el-eq-i
Γ  Prf p  s : (Prf q)[]
Γ  Prf q  t : (Prf p)[]
code-prop-eq# propositional extensionality:
Γ  p  q : Ω                                #   mutually implied props are equal codes
Γ  t : A
Γ   : Prf A
Γ  a₀  a₁ : A
el-eq-i# the canonical proof of a
Γ   : Prf (a₀  a₁  A)                #   true equation is ⋆
Γ  s : Prf (a₀  a₁  A)
el-reflect# equality reflection
Γ  a₀  a₁ : A
Γ  t₀ : Prf p
Γ  t₁ : Prf p
Γ  t₀  t₁ : Prf p
Γ  s : Prf A
Γ  A  b₀[]  b₁[] : B[]
Γ  b₀  b₁ : B
Γ  s : Prf A
Γ  A  t : (Prf q)[]
Γ   : Prf q

Quotient inductive-inductive types (signatures)

The formers ℕ and quotient each add ONE type. QIITs add a SCHEME: for each well-formed SIGNATURE 𝒮 — a family of mutually-defined, possibly index-dependent sorts, generated freely by point constructors and quotiented by equation constructors — the rules below license the sorts of 𝒮 as types (𝒮.𝕤 ē), their constructors (𝒮.𝕔 θ), the imposed path equations, and a dependent eliminator (𝒮.𝕤-elim) with its computation and uniqueness laws. Every rule is stated AGAINST a signature (⊦ 𝒮 qsig as a premise); a signature is NOT a Σ-entry and mints no names — 𝒮 is carried by the formers themselves (as A / R carries A and R). These are the inductive-inductive quotient types of Altenkirch–Kaposi. The scheme SUBSUMES ℕ, (⊎) and (/), and covers indexed inductive types (well-founded trees included) and quotient inductive types generally; ℕ, (⊎) and (/) are retained for now.

THE EXTENSIONAL PAYOFF

Under equality reflection (with Ω for proof-irrelevance) every type is a set: no higher paths, no coherence tower, no transport. A path constructor is therefore an equation IMPOSED judgementally (via el-reflect), and the eliminator's path premises collapse to WELL-DEFINEDNESS conditions — precisely quot-elim's f⁼ premise, one per equation, with no apd/transport. This degeneration is what lets the scheme be POSTULATED precisely rather than through a tower of coherences (contrast the intensional HIIT signatures, which need the full apparatus).

THEORY OF SIGNATURES

grammar. The ToS is a SMALL DEPENDENT TYPE THEORY of its own: qiit-contexts are built out of qiit-types, qiit-terms are typed at qiit-types, and all argument passing is by the ToS's own Π/λ/application — there is no spine syntax. A SIGNATURE is nothing but a closed qiit-context: sorts, point constructors and equation constructors are ordinary entries, distinguished by the HEAD of their type alone.

qiit-context

    Φ, 𝒮 ::=  | Φ  𝔄          # entries are ANONYMOUS

qiit-type

    𝔄 ::= U                     # the universe of codes
        | El 𝕥                  # decoding of a code 𝕥 : U
        | A  𝔄                 # EXTERNAL Π — domain a Nova
                                #   type; binds a NOVA variable
        | El 𝕥  𝔄              # INDUCTIVE Π — binds a ToS
                                #   variable

qiit-term

    𝕥 ::=                     # ToS VARIABLE, de Bruijn
        | 𝕥 t                   # application to a Nova term
        | 𝕥 𝕥'                  # application to a ToS term
        | λ 𝕥                   # external abstraction (binds
                                #   a NOVA variable)
        | 𝕥₀  𝕥₁               # equation CODE (in U, at the
                                #   sides' common El)

qiit-sub

    ς ::= 𝕚𝕕 |                 # the ToS's OWN substitution
             | ς  ς            #   calculus, mirroring Nova's
             | ς, 𝕥             #   (ς⁺ ≜ (ς ∘ ⇑, ⬡₀) derived)

(A ranges over Nova types, t over Nova terms; ⇛ is the ToS's Π, NOT Nova's →. The variable discipline is NAMELESS, like Nova's own: ⬡ᵢ counts inductive binders and context entries ONLY — ToS variables are ORTHOGONAL to Nova's ☐ᵢ, which external binders bind in the Nova zone, and the two calculi never touch each other's variables. In examples, named binders (x : A) ⇛ …, (𝕧 : El 𝕥) ⇛ … and named entries are DISPLAY SUGAR for the indexed core. Entry references from outside are POSITIONAL: 𝒮(k) = 𝔄 says entry k of 𝒮 (in declaration order) is 𝔄, the formers are 𝒮.k, and 𝕤, 𝕔 are used as metavariables for sort / constructor POSITIONS. There is no inductive λ: terms of inductive-Π type arise only as partial applications, which is all signatures need. The ToS has NO computation of its own — substitution application is a META-operation, and signatures are inert syntax, compared per IDENTITY below.)

Strict positivity and externality are GRAMMATICAL, by two features working together. First, Π domains are only Nova types or El-codes — U and Π-types never occur left of a ⇛. Second, the two Π's bind into DIFFERENT ZONES of the dual-zone judgements below: an external binder grows the NOVA zone Γ, an inductive binder the ToS zone Φ; Nova types are typed over Γ alone, so they cannot mention an inductive variable — sort-free automatically, with no projection and no side condition.

Entry classification, by the head of the entry's type (every qiit-type ends in U or El, so the classification is exhaustive — there are no other entry forms to exclude):

 U               a SORT (its Πs are the index arity)
    …  El (𝕤 ī)        a POINT constructor into sort 𝕤 El (l  r)      an EQUATION constructor (imposes l  r)

REFLECTION ⌊·⌋ interprets checked ToS syntax as Nova syntax (the two zones linearized in binder order). It is given as TYPED RULES after the well-formedness judgements below, whose derivations it computes on. Reflection is used ONLY by the OUTER formers (ty-qiit, el-qiit-*), to give a QIIT sort/constructor its Nova type; the ToS system itself never reflects.

META-OPERATIONS

(each ≜-defined by meta-level induction, like the substitution actions; A ranges over Nova types, Ξ over Nova telescopes, Φ over qiit-contexts).

Nova plumbing — context extension by a telescope, telescope weakening:

    Γ·ε  Γ                     ε  id
    Γ·(A  Ξ)  (Γ  A)·Ξ       (A  Ξ)    Ξ    # the ↑Ξ at Γ ▷ A
    (Ξ : Γ·Ξ  Γ, so [Ξ] weakens over Ξ)

LOOKUP Φ‖ᵢ — the type of ⬡ᵢ in Φ, weakened to all of Φ (mirrors Nova's Γ‖ᵢ, with the ToS shift):

    (Φ  𝔄)    𝔄[]
    (Φ  𝔄)ᵢ₊₁  (Φ)[]

OPENING

(Γ ; Φ) ⋉ 𝔄 — the dual zone reached by walking an El-ended type's binders, each into ITS zone (written Γ_𝔄 ; Φ_𝔄 when the base zone is clear):

    (Γ ; Φ)  El 𝕦         Γ ; Φ
    (Γ ; Φ)  (A  𝔄)      (Γ  A ; Φ[])  𝔄
    (Γ ; Φ)  (El 𝕥  𝔄)   (Γ ; Φ  El 𝕥)  𝔄

INSTANTIATION is not a bespoke operation — both binder instantiations are calculus instances, abbreviated 𝔄[t] / 𝔄[𝕥]: EXTERNAL, by a Nova term t: the NOVA substitution [id, t] acting through ToS syntax (below); INDUCTIVE, by a ToS term 𝕥: the ToS substitution [𝕚𝕕, 𝕥] (action with the qsub rules below).

NOVA SUBSTITUTION σ through ToS syntax (𝒮[σ], Φ[σ], 𝔄[σ], 𝕥[σ], ς[σ], ℰ[σ]): componentwise; σ acts on every embedded Nova piece, lifted (σ⁺, once per binder) over the EXTERNAL binders in scope at that piece; ToS variables are INERT (⬡ᵢ[σ] ≜ ⬡ᵢ — they are not Nova variables). The two calculi act on disjoint namespaces, so their actions commute.

THEORY-OF-SIGNATURES WELL-FORMEDNESS

The four ToS judgement forms and their PRESUPPOSITIONS are registered in the judgement-forms table at the top of the file:

    Γ  Φ qctx         Φ a well-formed qiit-context
    Γ ; Φ  𝔄 qty      𝔄 a well-formed qiit-type
    Γ ; Φ  𝕥 : 𝔄      𝕥 a qiit-term of type 𝔄
    Γ  ς : Φ₀  Φ₁    ς a qiit-substitution

The dual zone Γ ; Φ: Γ is the NOVA zone (the ambient context plus all external binders in scope), Φ the ToS zone (declared entries plus inductive binders). There is no separate signature judgement:

    Γ  𝒮 qsig      Γ  𝒮 qctx

— during checking, the growing context Φ IS the signature-so-far, so a later declaration reaches earlier sorts and constructors by qtm-var, with no prefix or ambient-𝒮 device.

Γ ctx
Γ   qctx
Γ  Φ qctx      Γ ; Φ  𝔄 qty
Γ  Φ  𝔄 qctx
Γ  Φ qctx
Γ ; Φ  U qty
Γ ; Φ  𝕥 : U
Γ ; Φ  El 𝕥 qty
Γ  A type      Γ  A ; Φ[]  𝔄 qty
qty-pi-ext# binds a NOVA variable:
Γ ; Φ  A  𝔄 qty                                    #   the Nova zone grows
Γ ; Φ  𝕥 : U      Γ ; Φ  El 𝕥  𝔄 qty
qty-pi-ind# binds a ToS variable:
Γ ; Φ  El 𝕥  𝔄 qty                                    #   the ToS zone grows
Φ = 𝔄
Γ ; Φ   : 𝔄
Γ ; Φ  𝕥 : A  𝔄      Γ  t : A
Γ ; Φ  𝕥 t : 𝔄[t]
Γ ; Φ  𝕥 : El 𝕦  𝔄      Γ ; Φ  𝕥' : El 𝕦
Γ ; Φ  𝕥 𝕥' : 𝔄[𝕥']
Γ  A ; Φ[]  𝕥 : 𝔄
Γ ; Φ  λ 𝕥 : A  𝔄
Γ ; Φ  𝕥₀ : El 𝕦      Γ ; Φ  𝕥₁ : El 𝕦
qtm-eq# equation code in U
Γ ; Φ  (𝕥₀  𝕥₁) : U

The ToS substitution calculus, mirroring Nova's (𝕚𝕕/⇑/∘/ext; the lift ς⁺ ≜ (ς ∘ ⇑, ⬡₀) : Φ₀ ▷ 𝔄[ς] ⇒ Φ₁ ▷ 𝔄 is derived):

Γ  Φ qctx
Γ  𝕚𝕕 : Φ  Φ
Γ ; Φ  𝔄 qty
Γ   : Φ  𝔄  Φ
Γ  ς : Φ₀  Φ₁      Γ  τ : Φ₁  Φ₂
Γ  τ  ς : Φ₀  Φ₂
Γ  ς : Φ₀  Φ₁      Γ ; Φ₀  𝕥 : 𝔄[ς]
Γ  (ς, 𝕥) : Φ₀  Φ₁  𝔄
Γ ; Φ₁  𝕥 : 𝔄      Γ  ς : Φ₀  Φ₁
qtm-sub# and likewise qty-sub;
Γ ; Φ₀  𝕥[ς] : 𝔄[ς]                              #   the action ≜-below

Action of ς (meta-level, one clause per former). Note the two binder cases: an INDUCTIVE binder lifts ς; an EXTERNAL binder instead Nova-weakens ς's embedded Nova pieces (ς[↑], the orthogonal action) — ToS indices do not shift at a Nova binder:

    U[ς]           U                (El 𝕥)[ς]       El (𝕥[ς])
    (A  𝔄)[ς]     A  𝔄[ς[]]     (El 𝕥  𝔄)[ς]   El (𝕥[ς])  𝔄[ς]
    [𝕚𝕕]                       []            ᵢ₊₁
    [ς, 𝕥]       𝕥               ᵢ₊₁[ς, 𝕥]       [ς]
    [τ  ς]      ([τ])[ς]
    (𝕥 t)[ς]       𝕥[ς] t          (𝕥 𝕥')[ς]        𝕥[ς] 𝕥'[ς]
    (λ 𝕥)[ς]       λ (𝕥[ς[]])     (𝕥₀  𝕥₁)[ς]     𝕥₀[ς]  𝕥₁[ς]

REFLECTION

the typed interpretation ⌊·⌋ of ToS syntax into Nova: one ADMISSIBLE rule per ToS judgement, computed by the ≜-clauses under it, by induction on the corresponding derivation (meta-level, like the substitution actions). The rules are stated for the entries of a COMPLETE signature 𝒮. Every clause is subscripted by its WALK STATE 𝑤 = (Γ̂, ρ, υ) — the ρ and υ a clause uses are the components of ITS 𝑤, bound by the subscript, never ambient:

    Γ̂   the MERGED context so far — both zones linearized in binder
        order, one Nova entry per binder;
    ρ   the REINDEXER  Γ̂  (the Nova zone so far);
    υ   the total WEAKENING  Γ̂  Γ, under which the carried
        signature moves (𝒮[υ]).

Crossing a binder STEPS the state (▷; the external step is present in both zones, so ρ lifts; the inductive step is merged-only, so ρ weakens):

    𝑤  A        (Γ̂  A[ρ], ρ, υ  )
    𝑤  El 𝕥     (Γ̂  El 𝕥_𝑤, ρ  , υ  )

The INITIAL state is 𝑤₀ ≜ (Γ, id, id); the FINAL state of an El-ended 𝔄's walk is written 𝑤_𝔄, with components Γ ⋈ 𝔄 (the MERGE) and ρ_𝔄:

    𝑤  El 𝕦         Γ̂
    𝑤  (A  𝔄)      (𝑤  A)  𝔄
    𝑤  (El 𝕥  𝔄)   (𝑤  El 𝕥)  𝔄

CONVENTION in the rules: reflections of WHOLE entry types (⌊𝔄⌋, ⌊𝔎⌋ᵗ) are at 𝑤₀; reflections of pieces under an entry's binders (⌊ī⌋, ⌊l⌋, ⌊r⌋, ⌊𝕥⌋) are at 𝑤_𝔄 — a use-site spine θ : ⌊𝔄⌋ᵗ then instantiates them, ⌊l⌋[θ], landing over Γ (Γ ⋈ 𝔄 = Γ·⌊𝔄⌋ᵗ, the binder telescope of an El-ended 𝔄 by the same recursion as the arity).

Qiit-types: an El-ended entry type reflects to a Nova TYPE (over Γ — the binders are re-bound inside it), a U-ended kind to a Nova TELESCOPE, its arity — same recursion, two read-outs:

Γ  𝒮 qsig      𝒮(𝕜) = 𝔄  (𝔄 El-ended)
Γ  𝔄 type
Γ  𝒮 qsig      𝒮(𝕤) = 𝔎  (𝔎 U-ended)
Γ  𝔎⌋ᵗ tel
El (𝕤 ī)_𝑤      𝒮[υ].𝕤 ī_𝑤      # ī = 𝕤's application chain,
                                      #   read off as a Nova spine
El (l  r)_𝑤    Prf (l_𝑤  r_𝑤  El 𝕦_𝑤)   # 𝕦 the sides' common
                                                     #   code; ≡ is Ω-valued,
                                                     #   so the type is a Prf
A  𝔄_𝑤         A[ρ]  𝔄_{𝑤  A}
El 𝕥  𝔄_𝑤      El 𝕥_𝑤  𝔄_{𝑤  El 𝕥}
U⌋ᵗ_𝑤            ε
A  𝔎⌋ᵗ_𝑤        A[ρ]  𝔎⌋ᵗ_{𝑤  A}
El 𝕥  𝔎⌋ᵗ_𝑤     El 𝕥_𝑤  𝔎⌋ᵗ_{𝑤  El 𝕥}

Qiit-terms. A ToS variable ⬡ᵢ either names an inductive Π-binder of the walk — reflected to the Nova variable at its MERGED slot m(i) (which counts ALL binders passed, not just inductive ones; a meta-level index computation) — or reaches through the binders into the signature, at entry position k. The rule is stated at the full OPENING (⋉, meta-operations above), whose merge is Γ ⋈ 𝔄:

Γ  𝒮 qsig      𝒮(𝕜) = 𝔄  (𝔄 El-ended)
(Γ ; 𝒮)  𝔄  𝕥 : El (𝕤 ī)
Γ  𝔄  𝕥_{𝑤_𝔄} : El (𝕤 ī)_{𝑤_𝔄}

The term clauses match on MAXIMAL application chains, because the Nova constructor former is SATURATED — a chain reflects at once, never through a partial application (a well-formed signature's qiit-terms are El-typed, so constructor chains are always full):

_𝑤           _{m(i)}    ( a binder of the walk; m(i) its merged
                               #  slot — a variable is an ordinary
                               #  term, it applies freely)
𝕥 t_𝑤          𝕥_𝑤 t[ρ]        (𝕥 BINDER-headed)
𝕥 𝕥'_𝑤         𝕥_𝑤 𝕥'_𝑤      (𝕥 BINDER-headed)
 𝕒₁𝕒ₙ_𝑤   𝒮[υ].k (𝕒₁_𝑤,, 𝕒ₙ_𝑤)
                    ( reaching POINT entry k of 𝒮: the whole chain at
                    #  once, onto the saturated former — external
                    #  components as t[ρ], inductive as reflections)
 𝕒₁𝕒ₙ_𝑤   
                    ( reaching an EQUATION entry of 𝒮: no bespoke
                    #  term is minted for it — the imposed equation
                    #  holds by el-qiit-path, so its Prf-type is
                    #  inhabited by ⋆ via el-eq-i)
λ 𝕥_𝑤          λ 𝕥_{𝑤  A}     # A the Π-domain of λ 𝕥's type

(a sort position 𝕤 occurs only applied inside El/≡ codes, handled by the El clause — 𝒮.𝕤 is a type former, not a term.)

Every conclusion above is a NOVA judgement: reflection of well-formed ToS syntax is well-formed Nova syntax, by simultaneous induction on the ToS derivation — the dual-zone discipline (Nova pieces typed over the Nova zone alone) is exactly what makes the ρ-reindexing well-defined. The outer formers below use the closed instances, further instantiated by use-site spines.

IDENTITY

(structural). 𝒮.𝕤 ē carries the signature 𝒮; two QIIT types are equal exactly when their signatures, sorts (positions), and indices are — homogeneous with every other former. The signature is compared INTENSIONALLY, and the NAMELESS discipline makes that comparison PLAIN STRUCTURAL EQUALITY of indexed syntax — there are no names, so there is no α to quotient by; like universe codes. The inductive-inductive self-reference is a BOUND reference (a ⬡-index) inside the finite signature, so the comparison is finite and iso-recursive — it never unfolds the fixpoint into its carrier, and needs no equirecursive/coinductive machinery. (Signature equality is finer than initial-algebra isomorphism — it distinguishes entry reorderings — but SOUND; choosing a syntactic granularity over the semantic one is the commitment the code-injectivity block already makes: models collapsing structurally-distinct types are excluded.)

A NAME for a QIIT is an ordinary definition x ≔ 𝒮.𝕤 type (which unfolds, ty-sig-beta). Comparing two uses of the same name is then the ordinary rigid-rigid-before-δ discipline — try the name, compare substitutions, unfold only on mismatch — nothing QIIT-specific, and it keeps the common case cheap without any bespoke rule. Consequently the theory is UNIFORMLY structural, QIITs included, so (/) is a genuine instance — A / R is 𝒮.𝕢 · for

    𝒮 = ( 𝕢 : U ; cls : (x : A)  El 𝕢 ;
          eq : (x y : A)  (h : Prf R[x,y])  El (cls x  cls y) )

— and the primitive (/) is kept for convenience, not necessity.

FORMATION

The sort-𝕤 type of 𝒮 at an index spine ē (against the reflected arity of 𝕤's kind), and its universe code, with El bridging. A sort has no ι/β of its own — its only computation is the eliminator's β. (Every QIIT former is SATURATED — spine-applied, like S t, class a and every other Nova former. The ToS is curried internally; currying stops at the Nova boundary.)

Γ  𝒮 qsig      𝒮(𝕤) = 𝔎  (𝔎 U-ended)      Γ  ē : 𝔎⌋ᵗ
Γ  𝒮.𝕤 ē type

A signature is SMALL when every Nova type it embeds (the external Π domains) is itself codable — of the form El a, or Prf p (props are size-free: subsingleton setoids, per the Ω block). Only SMALL signatures get a universe code. This is the ty-pi/code-pi divide, and here it is load-bearing: with a LARGE external domain — say (a : 𝕌) — the code's decoding would contain 𝕌 as a RETRACT (eliminate at constant motive 𝕌 with method a ↦ a), the classic type-in-type collapse; and the model agrees — the universe of codes cannot be constructed while consulting its own totality. Large signatures still form perfectly good TYPES (ty-qiit above); they just have no code.

Γ  𝒮 qsig      𝒮 small      𝒮(𝕤) = 𝔎  (𝔎 U-ended)      Γ  ē : 𝔎⌋ᵗ
Γ  𝒮.𝕤 ē : 𝕌
Γ  𝒮 qsig      𝒮(𝕤) = 𝔎  (𝔎 U-ended)      Γ  ē : 𝔎⌋ᵗ
Γ  El (𝒮.𝕤 ē)  𝒮.𝕤 ē type

INTRODUCTION

point constructor, FULLY SATURATED: θ supplies every argument at once, and 𝒮.𝕔 θ is the canonical form of its sort. A bare curried 𝒮.𝕔 : ⌊𝔄⌋ is deliberately NOT a term: in the empty context it would be a non-λ inhabitant of a Π-type, breaking canonicity at Π (a closed Π-inhabitant is a λ — docs/NovaSyntax.txt's gluing theorem) — the same violation the judgemental el-qiit-path avoids at ≡-types. Nothing is lost: a partial application is a λ away, λ (𝒮.𝕔 (…, ☐₀)).

Γ  𝒮 qsig      𝒮(𝕔) = 𝔄  (𝔄 ending in El (𝕤 ī))      Γ  θ : 𝔄⌋ᵗ
Γ  𝒮.𝕔 θ : El (𝕤 ī)[θ]

PATH

equation constructor: the equation HOLDS, as a JUDGEMENT — el-quot-eq's shape, generalized. Deliberately no proof term is minted: equality is Ω-valued, so an equation entry's reflected type is a Prf, whose one canonical form is ⋆ — a constructor form there would be a second canonical inhabitant, refuting witness irrelevance. Nothing is lost — the Prf-type is inhabited by ⋆ via el-eq-i once el-qiit-path imposes the equation — and any witness data the equation is conditional on (e.g. the quotient's Prf R) is simply a binder of 𝔄, instantiated inside θ. (⌊𝔄⌋ᵗ for an El-ended 𝔄 is the binder telescope, by the same recursion as the arity.)

Γ  𝒮 qsig      𝒮(𝕔) = 𝔄  (𝔄 ending in El (l  r))      Γ  θ : 𝔄⌋ᵗ
Γ  l[θ]  r[θ] : El 𝕦[θ]      # 𝕦 the sides' common code

ELIMINATION

The eliminator is specified by a LAYERED stack of judgement forms — MOTIVE FAMILY, DISPLAYED ALGEBRA, ELIMINATION PROBLEM, SECTION CANDIDATE (all registered in the judgement-forms table) — and by TYPE-DIRECTED admissible translations (·ᴰ, ·ᴰᵗ, θ⟨φ⟩, ⟦·⟧), each computed by ≜-clauses like reflection. The layering is the dependency order: motives → ᴰ-translations → methods → method images → coherences; each layer's rules use only earlier layers. Grammar: an ℰ is a pair of families, ℰ ::= C̄ ; m̄ (one motive per sort position, one method per point position of 𝒮).

MOTIVE FAMILY

one Nova type family per sort, over its reflected index telescope and the sort itself (δ = ⌊𝔎⌋ᵗ's variables):

Γ  𝒮 qsig
for each sort position 𝕤 of 𝒮 (𝒮(𝕤) = 𝔎):
    Γ·𝔎⌋ᵗ  𝒮.𝕤 δ  C_𝕤 type
Γ   : 𝒮 mot

DISPLAYED TYPE 𝔄ᴰ⟨e⟩ and DISPLAYED TELESCOPE 𝔄ᴰᵗ — the two ᴰ-read-outs of an entry type, relative to motives C̄: for a term e of the head's type OVER THE MERGE, 𝔄ᴰ⟨e⟩ is the Nova type of "e is covered by the motives", a Π-type over the displayed telescope. The parameter is consumed ONCE, at the base, through the final projection — saturation means there is no function to thread through the binders. An INDUCTIVE binder at a sort code contributes its argument AND its induction hypothesis; an external binder, and an inductive binder at an EQUATION code (a content-free proof — the extensional degeneration), contribute only their argument.

Γ   : 𝒮 mot      𝒮(𝕜) = 𝔄  (𝔄 ending in El (𝕤 ī))
Γ  𝔄  e : El (𝕤 ī)_{𝑤_𝔄}
Γ  𝔄e type
Γ   : 𝒮 mot      𝒮(𝕜) = 𝔄  (𝔄 El-ended)
Γ  𝔄ᴰᵗ tel

The ᴰ-clauses walk like reflection, in the ᴰ-STATE (𝑤 ; π) — the reflection walk state paired with the PROJECTION π from the ᴰ-context so far onto the plain merge so far (Γ̂ of 𝑤), forgetting the IH slots. As with 𝑤, the π a clause uses is bound by its subscript. The steps (argument slots are shared, so π lifts; IH slots are ᴰ-only, so π weakens):

    (𝑤 ; π)  A           (𝑤  A ; π)
    (𝑤 ; π)  El (𝕤 ī)    (𝑤  El (𝕤 ī) ; π  )
    (𝑤 ; π)  El (l  r)  (𝑤  El (lr) ; π)

Initial state (𝑤₀ ; id); the FINAL π of an entry's walk is the πᴰ appearing in the rules (mimg, eprob):

(El (𝕤 ī))_{𝑤;π}e         C_𝕤[ī_𝑤[π], e[π]]     # the base: π is final
(A  𝔄)_{𝑤;π}e            A[ρ][π]  𝔄_{(𝑤;π)  A}e
(El (𝕤 ī)  𝔄)_{𝑤;π}e     El (𝕤 ī)_𝑤[π]  C_𝕤[ī_𝑤[π][], ]
                                  𝔄_{(𝑤;π)  El (𝕤 ī)}e
(El (l  r)  𝔄)_{𝑤;π}e   El (lr)_𝑤[π]
                                  𝔄_{(𝑤;π)  El (lr)}e          # no IH
(El 𝕦)ᴰᵗ_{𝑤;π}             ε
(A  𝔄)ᴰᵗ_{𝑤;π}            A[ρ][π]  𝔄ᴰᵗ_{(𝑤;π)  A}
(El (𝕤 ī)  𝔄)ᴰᵗ_{𝑤;π}     El (𝕤 ī)_𝑤[π]  C_𝕤[ī_𝑤[π][], ]
                                𝔄ᴰᵗ_{(𝑤;π)  El (𝕤 ī)}
(El (l  r)  𝔄)ᴰᵗ_{𝑤;π}   El (lr)_𝑤[π]  𝔄ᴰᵗ_{(𝑤;π)  El (lr)}
                                                            # no IH slot

(One recursion, two read-outs: 𝔄ᴰ⟨e⟩ is the Π over 𝔄ᴰᵗ ending in C_𝕤 at ⌊ī⌋[πᴰ] and e[πᴰ] — at a sort-inductive binder the value is ☐₁ and its induction hypothesis ☐₀. In the rules, unsubscripted 𝔄ᴰ⟨e⟩ / 𝔄ᴰᵗ of a whole entry type are at (𝑤₀ ; id).)

DISPLAYED ALGEBRA

motives plus a method per point constructor:

Γ   : 𝒮 mot
for each point position 𝕔 of 𝒮 (𝒮(𝕔) = 𝔄; δ = 𝔄⌋ᵗ's variables):
    Γ  m_𝕔 : 𝔄𝒮.𝕔 δ
Γ  ( ; ) : 𝒮 dalg
# (𝒮.𝕔 δ — the SATURATED constructor at the merge's own variables —
# is the e whose coverage the method provides.)

METHOD IMAGE ⟦·⟧

relative to a displayed algebra: the image of a qiit-term under the methods, with induction hypotheses read off the displayed telescope. Stated at the full OPENING of the entry type, concluded in its ᴰ-context. ⟦·⟧ walks APPLICATION CHAINS only, never binders, so all its clauses are at one fixed state — the final ᴰ-state (𝑤_𝔄 ; πᴰ) — and the ρ, υ, πᴰ below are its components:

Γ  ( ; ) : 𝒮 dalg      𝒮(𝕜) = 𝔄  (𝔄 El-ended)
(Γ ; 𝒮)  𝔄  𝕥 : El (𝕤 ī)
Γ·𝔄ᴰᵗ  𝕥 : C_𝕤[ī[π], 𝕥[π]]
     _{d(i)}          # d(i) = ⬡ᵢ's IH slot in 𝔄ᴰᵗ (a meta-level
                             #   index computation, like m(i))
𝕔      m_𝕔[𝔄ᴰᵗ]        # a point-constructor head, weakened in
𝕥 t    𝕥 (t[ρ][π])
𝕥 𝕥'   𝕥 (𝕥'[π]) 𝕥'          # 𝕥' at a sort code: value, image
𝕥 𝕡    𝕥 (𝕡[π])                # 𝕡 at an equation code: value only

ELIMINATION PROBLEM

a displayed algebra whose COHERENCES hold: per equation constructor, the method images of the two sides agree. This is quot-elim's f⁼, one per equation, with no transport (extensional: C[…,⌊l⌋[πᴰ]] ≐ C[…,⌊r⌋[πᴰ]] since ⌊l⌋ ≐ ⌊r⌋ by el-qiit-path). Coherences are CHECKED, not stored — the eliminator term carries ℰ = (C̄ ; m̄) only:

Γ   : 𝒮 dalg
for each equation position 𝕔 of 𝒮
    (𝒮(𝕔) = 𝔄, ending in El (l  r), the sides at code 𝕤 ī):
    Γ·𝔄ᴰᵗ  l  r : C_𝕤[ī[π], l[π]]
Γ   : 𝒮 eprob

SECTION CANDIDATE

one term per sort, in the motive's context; and the SECTION SPINE θ⟨φ⟩, a Nova spine for the displayed telescope that interleaves θ with the φ-images of its inductive components (θ's component at each binder written b):

Γ   : 𝒮 mot
for each sort position 𝕤 of 𝒮 (𝒮(𝕤) = 𝔎):
    Γ·𝔎⌋ᵗ  𝒮.𝕤 δ  φ_𝕤 : C_𝕤
Γ  φ :  sect
Γ  φ :  sect      𝒮(𝕜) = 𝔄  (𝔄 El-ended)      Γ  θ : 𝔄⌋ᵗ
Γ  θφ : 𝔄ᴰᵗ
(El 𝕦)φ            ·
(A  𝔄)φ           b, 𝔄φ
(El (𝕤 ī)  𝔄)φ    b, φ_𝕤 ī b, 𝔄φ
(El (l  r)  𝔄)φ  b, 𝔄φ                    # no IH slot

(b is θ's component at the binder — the clauses consume θ in order, and each ⌊ī⌋ is at the current walk state INSTANTIATED by the spine consumed so far, [id, θ↾] — so every component lives over Γ. Then m θ⟨φ⟩ : C_𝕤[⌊ī⌋[θ], e[θ]] for m : 𝔄ᴰ⟨e⟩, by the read-out note.)

Γ  𝒮 qsig      𝒮(𝕤) = 𝔎      Γ   : 𝒮 eprob
Γ  ē : 𝔎⌋ᵗ      Γ  w : 𝒮.𝕤 ē
Γ  𝒮.𝕤-elim  ē w : C_𝕤[ē, w]

COMPUTATION

(β) — at the saturated constructor (its sort and indices read off 𝕔's type). φᵉˡ is the family φᵉˡ_𝕤 ≜ 𝒮.𝕤-elim ℰ δ ☐₀ — a section candidate, by el-qiit-elim.

Γ  𝒮 qsig      𝒮(𝕔) = 𝔄  (𝔄 ending in El (𝕤 ī))
Γ   : 𝒮 eprob      Γ  θ : 𝔄⌋ᵗ
Γ  𝒮.𝕤-elim  ī[θ] (𝒮.𝕔 θ)  m_𝕔 θφᵉˡ : C_𝕤[ī[θ], 𝒮.𝕔 θ]
#   the RHS is 𝕔's method image with the hypotheses supplied by elim
#   itself. EQUATION constructors have NO β-rule (their content is a
#   judgement).

UNIQUENESS

(η) — the section is unique (initiality): any candidate that commutes with every point constructor IS the eliminator.

Γ   : 𝒮 eprob      Γ  h :  sect
for each point position 𝕔 of 𝒮 (𝒮(𝕔) = 𝔄, ending in El (𝕤 ī);
                                θ = 𝔄⌋ᵗ's variables):
    Γ·𝔄⌋ᵗ  h_𝕤[ī, 𝒮.𝕔 θ]  m_𝕔 θh : C_𝕤[ī, 𝒮.𝕔 θ]
𝒮(𝕤) = 𝔎      Γ  ē : 𝔎⌋ᵗ      Γ  w : 𝒮.𝕤 ē
Γ  h_𝕤[ē, w]  𝒮.𝕤-elim  ē w : C_𝕤[ē, w]
#   any h satisfying the β-equations equals elim: two maps out of a
#   QIIT that agree on all constructors are equal (el-nat-eta /
#   el-quot-eta, generalized).

SUBSTITUTION ACTION

Substitution acts through the carried signature:

    (𝒮.𝕤 ē)[σ]           𝒮[σ].𝕤 ē[σ]     (type and code)
    (𝒮.𝕔 θ)[σ]           𝒮[σ].𝕔 θ[σ]
    (𝒮.𝕤-elim  ē w)[σ]  𝒮[σ].𝕤-elim [σ] ē[σ] w[σ]

where 𝒮[σ] and ℰ[σ] are the ToS substitution meta-operation (defined with the grammar above): σ on every embedded Nova piece, lifted over the external binders in scope; inductive variables untouched.

CONGRUENCE and INJECTIVITY are STRUCTURAL: equal QIIT types/codes have equal signatures, sort positions, and index spines, and conversely — the signature compared componentwise (entry by entry; qiit-types and qiit-terms as plain indexed syntax — nameless, no α — their embedded Nova pieces by the existing congruence/injectivity rules). Stated by that meta-recursion rather than spelled per entry, and sound by the same canonical-forms commitment as the other formers' inj rules.

NOTES

  • SUBSUMPTION. ℕ is 𝒮.𝕟 · for 𝒮 = (𝕟 : U; Z : El 𝕟; S : (𝕧 : El 𝕟) ⇛ El 𝕟). The quotient A / R is 𝒮.𝕢 · for the signature under IDENTITY above. The disjoint union A ⊎ B is 𝒮.𝕤 · for 𝒮 = (𝕤 : U; inl : (x : A) ⇛ El 𝕤; inr : (y : B) ⇛ El 𝕤) — two external-domain points, no equations; its eliminator's β and η are el-qiit-beta/-eta at that signature, which is exactly why ⊎'s standalone rules could be READ OFF the scheme. An indexed inductive type (well-founded trees included) is a sorts-and-points signature: sorts with index arities over I, one point constructor per node shape whose inductive binders are the subtrees. Because QIIT equality is structural (IDENTITY above), these are genuine equalities, not just encodings: ℕ and (/) are kept for convenience but are now DERIVABLE, each a one-line signature. (At the CODE level the signatures are small — ℕ's embeds no Nova types at all, and code-quot's arity, A : 𝕌 with R : Ω, is exactly El a and Prf R domains — so code-nat/code-quot are subsumed too.)
  • RELAXATION. Strict positivity is GRAMMATICAL — Π domains are only Nova types (sort-free: the Nova zone has no inductive variables) or El-codes; U and Π-types never occur left of a ⇛. This grammar is the DECIDABLE proxy for a semantic condition: that the signature's operator be monotone on the lattice of relations (the setoid congruences over the carrier). A future revision could widen the domain grammar and instead discharge a monotonicity obligation as an ordinary premise, admitting monotone-but-not-positive operators; postulated here in the positive fragment only.
  • SEMANTICS. The postulate asserts that 𝒮's INITIAL ALGEBRA exists in the setoid model: carriers are the constructor terms, the setoid relation is the congruence GENERATED by the equation constructors (no quotienting step — coarsening the relation IS the quotient), 𝒮.𝕤-elim is the unique section into any displayed algebra (el-qiit-eta), and β holds on the nose. This is the initiality commitment of Altenkirch–Kaposi–Kovács (finitary QIITs), transported to the proof-irrelevant setoid setting where the coherence tower degenerates. As with the injectivity rules, models that fail initiality are hereby excluded.

EXAMPLE

(inductive-inductive: contexts and types). The signature

    𝒮 = ( Con : U
        ; Ty  : (𝕘 : El Con)  U
        ;: El Con
        ; ext : (𝕘 : El Con)  (𝕒 : El (Ty 𝕘))  El Con      # Γ ▷ A
        ; u   : (𝕘 : El Con)  El (Ty 𝕘)
        ; pi  : (𝕘 : El Con)  (𝕒 : El (Ty 𝕘))
                   (𝕓 : El (Ty (ext 𝕘 𝕒)))  El (Ty 𝕘) )

gives types 𝒮.Con · and 𝒮.Ty c (Ty indexed by Con); induction is induction-induction — a motive for Con and one for Ty over it, the methods respecting the dependency.

EXAMPLE

(quotient: finite multisets over an external type A).

    𝒮 = ( Bag : U
        ; nil : El Bag
        ; ins : (x : A)  (𝕞 : El Bag)  El Bag              # x ∷ m
        ; swp : (x y : A)  (𝕞 : El Bag)
                   El (ins x (ins y 𝕞)  ins y (ins x 𝕞)) )

swp is an equation constructor; 𝒮.Bag ·'s eliminator carries the coherence premise that the method for ins is invariant under swapping the two heads — the multiset laws, no transport.

Signature references.

(Γ  x  a : A)  Σ
 : Δ  Γ norm
Σ Δ  x[] : A[]
(Γ  x  a : A)  Σ
 : Δ  Γ norm
Σ Δ  x[]  a[] : A[]

Open-signature references (see DEFINITIONAL AND OPEN SIGNATURES): a declaration types its references but never unfolds them (no -beta); an element constraint is used as a definitional equality.

(Γ  x : A)  Σ
 : Δ  Γ norm
Σ Δ  x[] : A[]
(Γ  a₀  a₁ : A)  Σ
 : Δ  Γ norm
Σ Δ  a₀[]  a₁[] : A[]

Substitution action on elements: t[σ] is defined by meta-level induction on t via the ≜-equations below.

Γ₁  t : A
σ : Γ₀  Γ₁
Γ₀  t[σ] : A[σ]
Γ  t : A
el-sub-id# true on the nose by induction on t
Γ  t[id]  t : A
Γ₂  t : A
σ : Γ₁  Γ₂
τ : Γ₀  Γ₁
el-sub-comp# true on the nose by induction on t
Γ₀  t[σ  τ]  t[σ][τ] : A[σ][τ]
σ : Γ₀  Γ₁
Γ₀  𝟘[σ]  𝟘 : 𝕌,   𝟙[σ]  𝟙 : 𝕌,   [σ]   : 𝕌,   ()[σ]  () : 𝟙,   Z[σ]  Z : 
Γ₁  t : 
σ : Γ₀  Γ₁
Γ₀  (S t)[σ]  S t[σ] : 
Γ₁  A : 𝕌
Γ₁  El A  B : 𝕌
σ : Γ₀  Γ₁
Γ₀  (A  B)[σ]  A[σ]  B[σ] : 𝕌
Γ₁  A : 𝕌
Γ₁  El A  B : 𝕌
σ : Γ₀  Γ₁
Γ₀  (A  B)[σ]  A[σ]  B[σ] : 𝕌
Γ₁  A : 𝕌
Γ₁  B : 𝕌
σ : Γ₀  Γ₁
Γ₀  (A  B)[σ]  A[σ]  B[σ] : 𝕌
Γ₁  A : 𝕌
Γ₁  El A  (El A)[]  R : Ω
σ : Γ₀  Γ₁
Γ₀  (A / R)[σ]  A[σ] / R[σ] : 𝕌
Γ₁  A type
σ : Γ₀  Γ₁
Γ₀  A[σ]  A[σ] : Ω
Γ₁  A  f : B
σ : Γ₀  Γ₁
Γ₀  (λ f)[σ]  λ f[σ] : A[σ]  B[σ]
Γ₁  A  B type
Γ₁  f : A  B
Γ₁  e : A
σ : Γ₀  Γ₁
Γ₀  (f e)[σ]  f[σ] e[σ] : B[σ, e[σ]]
Γ₁  a : A
Γ₁  A  Prf (  a[]  A[])  b : B
σ : Γ₀  Γ₁
Γ₀  (let a b)[σ]  let a[σ] b[σ] : B[σ, a[σ], ]
# (coherent: ☐₀[σ⁺] ≜ ☐₀ and a[↑][σ⁺] ≐ a[σ][↑], so the Prf entry
# lands as the unfolding equation OF a[σ] — the RHS is the let at
# a[σ] — and ⋆[σ] ≜ ⋆ keeps the conclusion type in shape)
Γ₁  A  B type
Γ₁  a : A
Γ₁  b : B[id, a]
σ : Γ₀  Γ₁
Γ₀  (a , b)[σ]  a[σ] , b[σ] : A[σ]  B[σ]
Γ₁  t : A  B
σ : Γ₀  Γ₁
Γ₀  (t .π₁)[σ]  t[σ] .π₁ : A[σ]
Γ₁  t : A  B
σ : Γ₀  Γ₁
Γ₀  (t .π₂)[σ]  t[σ] .π₂ : B[σ, t[σ] .π₁]
Γ₁  B type
Γ₁  a : A
σ : Γ₀  Γ₁
Γ₀  (inj₁ a)[σ]  inj₁ a[σ] : A[σ]  B[σ]
Γ₁  A type
Γ₁  b : B
σ : Γ₀  Γ₁
Γ₀  (inj₂ b)[σ]  inj₂ b[σ] : A[σ]  B[σ]
Γ  A  B  C type
Γ  A  l : C[, inj₁ ]
Γ  B  r : C[, inj₂ ]
Γ  t : A  B
σ : Δ  Γ
Δ  (⊎-elim l r t)[σ]  ⊎-elim l[σ] r[σ] t[σ] : C[σ, t[σ]]
Γ₁  a₀ : A
Γ₁  a₁ : A
σ : Γ₀  Γ₁
Γ₀  (a₀  a₁  A)[σ]  (a₀[σ]  a₁[σ]  A[σ]) : Ω
Γ₁   : Prf p
σ : Γ₀  Γ₁
Γ₀  [σ]   : (Prf p)[σ]
Γ    A type
Γ  z : A[id, Z]
Γ    A  s : A[  , S ]
Γ  t : 
σ : Δ  Γ
Δ  (ℕ-elim z s t)[σ]  ℕ-elim z[σ] s[σ] t[σ] : A[σ, t[σ]]
Γ  A  A[]  R : Ω
Γ  a : A
σ : Δ  Γ
Δ  (class a)[σ]  class a[σ] : A[σ] / R[σ]
Γ  (A / R)  B type
Γ  A  f : B[, class ]
Γ  A  A[]  Prf R  f[    , ]  f[    , ] : B[    , class ]
Γ  q : A / R
σ : Δ  Γ
Δ  (quot-elim f q)[σ]  quot-elim f[σ] q[σ] : B[σ, q[σ]]
Γ  A type
Γ  t : 𝟘
σ : Δ  Γ
Δ  (𝟘-elim t)[σ]  𝟘-elim t[σ] : A[σ]
σ : Δ  Γ
Δ  t : A[σ]
var-sub-hit# A the type ☐₀ names in Γ ▷ A
Δ  [σ, t]  t : A[σ]
Γ   : B
σ : Δ  Γ
Δ  t : A[σ]
var-sub-miss# A the extension type
Δ  ₙ₊₁[σ, t]  [σ] : B[σ]
Γ   : B
Γ  A type
Γ  A  []  ₙ₊₁ : B[]
Γ   : B
Γ  [id]   : B
Γ   : B
τ : Δ  Γ
σ : Ξ  Δ
Ξ  [τ  σ]  [τ][σ] : B[τ][σ]
(Γ  x  a : A)  Σ
 : Γ₁  Γ norm
σ : Γ₀  Γ₁
Σ Γ₀  x[][σ]  x[  σ] : A[  σ]

Coercion.

Γ  A₀  A₁ type
Γ  a : A₀
Γ  a : A₁
Γ  A₀  A₁ type
Γ  a₀  a₁ : A₀
Γ  a₀  a₁ : A₁
Γ₀  Γ₁ ctx
Γ₀  a : A
Γ₁  a : A
Γ₀  Γ₁ ctx
Γ₀  a₀  a₁ : A
Γ₁  a₀  a₁ : A

Congruence rules for element constructors.

Γ₁  t₀  t₁ : A
σ₀  σ₁ : Γ₀  Γ₁
Γ₀  t₀[σ₀]  t₁[σ₁] : A[σ₁]
Γ₁  t₀  t₁ : A
σ : Γ₀  Γ₁
el-sub-cong-fix# admissible: specialize via sub-refl
Γ₀  t₀[σ]  t₁[σ] : A[σ]
Γ  A  f₀  f₁ : B
Γ  λ f₀  λ f₁ : A  B
Γ  A  B type
Γ  f₀  f₁ : A  B
Γ  a₀  a₁ : A
Γ  f₀ a₀  f₁ a₁ : B[id, a₁]
Γ  a₀  a₁ : A
Γ  A  Prf (  a₁[]  A[])  b₀  b₁ : B
Γ  let a₀ b₀  let a₁ b₁ : B[id, a₁, ]
# (the a₀- and a₁-instance contexts are equal — ctx-ext-cong with
# code-eq-cong — so the premise is stated at the a₁ instance, as at
# the other congruences)
Γ  A  B type
Γ  a₀  a₁ : A
Γ  b₀  b₁ : B[id, a₁]
Γ  (a₀, b₀)  (a₁, b₁) : A  B
Γ  t₀  t₁ : A  B
Γ  t₀ .π₁  t₁ .π₁ : A
Γ  t₀  t₁ : A  B
Γ  t₀ .π₂  t₁ .π₂ : B[id, t₁ .π₁]
Γ  B type
Γ  a₀  a₁ : A
Γ  inj₁ a₀  inj₁ a₁ : A  B
Γ  A type
Γ  b₀  b₁ : B
Γ  inj₂ b₀  inj₂ b₁ : A  B
Γ  A  B  C type
Γ  A  l₀  l₁ : C[, inj₁ ]
Γ  B  r₀  r₁ : C[, inj₂ ]
Γ  t₀  t₁ : A  B
el-sum-e-cong# motive C
Γ  ⊎-elim l₀ r₀ t₀  ⊎-elim l₁ r₁ t₁ : C[id, t₁]
Γ  t₀  t₁ : 
Γ  S t₀  S t₁ : 
Γ    A type
Γ  z₀  z₁ : A[id, Z]
Γ    A  s₀  s₁ : A[  , S ]
Γ  t₀  t₁ : 
el-nat-e-cong# motive A
Γ  ℕ-elim z₀ s₀ t₀  ℕ-elim z₁ s₁ t₁ : A[id, t₁]
Γ  A type
Γ  t₀ : 𝟘
Γ  t₁ : 𝟘
el-zero-e-cong# stronger than a congruence: no t⁼ premise
Γ  𝟘-elim t₀  𝟘-elim t₁ : A
Γ  A  A[]  R : Ω
Γ  a₀  a₁ : A
Γ  class a₀  class a₁ : A / R
Γ  (A / R)  B type
Γ  A  f₀ : B[, class ]
Γ  A  f₁ : B[, class ]
Γ  A  A[]  Prf R  f₀[    , ]  f₀[    , ] : B[    , class ]
Γ  A  A[]  Prf R  f₁[    , ]  f₁[    , ] : B[    , class ]
Γ  A  f₀  f₁ : B[, class ]
Γ  q₀  q₁ : A / R
el-quot-e-cong# motive B
Γ  quot-elim f₀ q₀  quot-elim f₁ q₁ : B[id, q₁]

Congruence rules for universe code constructors.

Γ  A₀  A₁ : 𝕌
Γ  El A₁  B₀  B₁ : 𝕌
Γ  A₀  B₀  A₁  B₁ : 𝕌
Γ  A₀  A₁ : 𝕌
Γ  El A₁  B₀  B₁ : 𝕌
Γ  A₀  B₀  A₁  B₁ : 𝕌
Γ  A₀  A₁ : 𝕌
Γ  B₀  B₁ : 𝕌
Γ  A₀  B₀  A₁  B₁ : 𝕌
Γ  A₀  A₁ : 𝕌
Γ  El A₁  (El A₁)[]  R₀  R₁ : Ω
Γ  A₀ / R₀  A₁ / R₁ : 𝕌
Γ  A₀  A₁ type
Γ  A₀  A₁ : Ω

Coinductive types (polynomial codes)

The dual scheme to QIITs, in its smallest useful form: for each POLYNOMIAL 𝔽 — a one-hole strictly positive code, no binders over the hole, no internal fixpoints — the rules below license the coinductive type ν 𝔽, its observation out (the ELIMINATOR), its corecursor corec (the INTRODUCTION), a β-law running one observation step, and a uniqueness law (η) that IS the coinduction principle. The polarity is Π's, not ℕ's: canonical forms are corec-headed, out forces lazily, and elements are compared by observation. Like a QIIT signature, 𝔽 is not a Σ-entry and mints no names — it is carried by the formers and compared structurally.

THE EXTENSIONAL PAYOFF, dual to the QIIT section's: uniqueness of the corecursor is a plain judgemental rule. In intensional theories judgemental finality is rejected as undecidable, and coinductive equality degenerates into hand-rolled bisimulation setoids; here ≐ is already reflection-strong, so el-nu-eta is homogeneous with el-qiit-eta — and BISIMULATION IMPLIES EQUALITY becomes a corollary rather than a discipline.

POLYNOMIALS

grammar. External pieces are CODES, so every polynomial is small and ν 𝔽 always has a code (no smallness side condition — the grammar enforces it). A left-hand `El a` BINDS a Nova variable in its body, exactly as code-sigma/code-pi bind; the two product forms are distinguished by their left-hand side (K a ⨯ … is the non-binding instance of the same shape). The hole 𝕏 never occurs left of a → — strict positivity is GRAMMATICAL, with nothing to check (the same decidable-proxy commitment as RELAXATION in the QIIT notes: here the semantic condition is that 𝔽's operator be monotone on the setoid lattice).

polynomial

    𝔽, 𝔾 ::= 𝕏               # the hole
           | K a             # constant at a code
           | 𝔽  𝔾           # product
           | 𝔽  𝔾           # sum — onto the native ⊎
           | El a  𝔽        # dependent pair over external data
                             #   (binds a NOVA variable)
           | El a  𝔽        # exponent with external domain
                             #   (binds a NOVA variable)
Γ ctx
Γ  𝕏 poly
Γ  a : 𝕌
Γ  K a poly
Γ  𝔽 poly      Γ  𝔾 poly
Γ  𝔽  𝔾 poly
Γ  𝔽 poly      Γ  𝔾 poly
Γ  𝔽  𝔾 poly
Γ  a : 𝕌      Γ  El a  𝔽 poly
Γ  El a  𝔽 poly
Γ  a : 𝕌      Γ  El a  𝔽 poly
Γ  El a  𝔽 poly

REFLECTION ⌊𝔽⌋(c) — the code with the hole filled by Γ ⊦ c : 𝕌 (≜-defined by meta-level induction on 𝔽, like the QIIT ⌊·⌋; c weakens under the binders):

    𝕏(c)           c
    K a(c)         a
    𝔽  𝔾(c)       𝔽(c)  𝔾(c)[]      # code-sigma, non-dependent
    𝔽  𝔾(c)       𝔽(c)  𝔾(c)         # code-sum, direct
    El a  𝔽(c)    a  𝔽(c[])
    El a  𝔽(c)    a  𝔽(c[])

FUNCTORIAL ACTION map_𝔽 — for Γ ⊦ g : El c₀ → El c₁, a function term Γ ⊦ map_𝔽 g : El ⌊𝔽⌋(c₀) → El ⌊𝔽⌋(c₁), ≜-defined by meta-level induction on 𝔽 (clauses written applied; at the binding formers the recursion proceeds at the instantiated body and g weakens under the binder; the sum clause is ⊎-elim at constant motive):

    map_𝕏 g x              g x
    map_{K a} g x          x
    map_{𝔽  𝔾} g p        (map_𝔽 g (p .π₁) , map_𝔾 g (p .π₂))
    map_{𝔽  𝔾} g s        ⊎-elim (inj₁ (map_𝔽 g[] )) (inj₂ (map_𝔾 g[] )) s
    map_{El a  𝔽} g p     (p .π₁ , map_𝔽 g (p .π₂))
    map_{El a  𝔽} g f     λ (map_𝔽 g[] (f[] ))

The FUNCTOR LAWS — map_𝔽 (λ ☐₀) ≐ λ ☐₀ and map_𝔽 (g₁ ∘ g₀-composite) ≐ map_𝔽 g₁ ∘ map_𝔽 g₀ pointwise — are derivable per polynomial by meta-level induction on 𝔽, each instance an ordinary internal equation (β, η and ⊎-eta per former).

IDENTITY

(structural). ν 𝔽 carries its polynomial; two ν-types are equal exactly when their polynomials are — nameless indexed syntax, compared componentwise (embedded Nova pieces by the existing congruence/injectivity rules), iso-recursive: the comparison never unfolds the fixpoint into its body. ν 𝔽 and El ⌊𝔽⌋(ν 𝔽) are ISOMORPHIC (out one way; the derivable in below the other) and deliberately never ≐ — same commitment as the QIIT IDENTITY paragraph. Congruence and injectivity are structural, by that meta-recursion (code-nu-cong/-inj are the componentwise instances, not stated per former).

FORMATION

Every polynomial names a small type:

Γ  𝔽 poly
Γ  ν 𝔽 type
Γ  𝔽 poly
Γ  ν 𝔽 : 𝕌
Γ  𝔽 poly
Γ  El (ν 𝔽)  ν 𝔽 type

ELIMINATION

the observation. A sort of this scheme has no constructor canonical forms; out is the only way to consume it, and the only computation is β below (out of a neutral is neutral):

Γ  𝔽 poly      Γ  t : ν 𝔽
Γ  out t : El 𝔽(ν 𝔽)

INTRODUCTION

the corecursor: any coalgebra maps in. The polynomial 𝔽 and the carrier code a are CARRIED by the term (like ℰ at 𝒮.𝕤-elim — β consumes map_𝔽, so the redex is self-contained); f is the coalgebra body, x the seed. Write hᵉˡ ≜ λ (corec 𝔽 a f[↑] ☐₀) for the corecursor as a function term (cf. φᵉˡ at el-qiit-beta):

Γ  𝔽 poly      Γ  a : 𝕌
Γ  El a  f : El 𝔽(a)[]
Γ  x : El a
Γ  corec 𝔽 a f x : ν 𝔽

COMPUTATION

(β) — observing a corecursive value runs the coalgebra one step and re-wraps the recursive positions:

Γ  𝔽 poly      Γ  a : 𝕌
Γ  El a  f : El 𝔽(a)[]
Γ  x : El a
Γ  out (corec 𝔽 a f x)  map_𝔽 hᵉˡ (f[id, x]) : El 𝔽(ν 𝔽)

UNIQUENESS

(η) — the coinduction principle, el-quot-eta's shape: any candidate commuting with the observation IS the corecursor.

Γ  𝔽 poly      Γ  a : 𝕌
Γ  El a  f : El 𝔽(a)[]
Γ  El a  h : (ν 𝔽)[]
Γ  El a  out h  map_𝔽 ((λ h)[]) f : El 𝔽(ν 𝔽)[]
Γ  x : El a
Γ  h[id, x]  corec 𝔽 a f x : ν 𝔽

Corollary (two-candidate form, as at ℕ and ⊎): two maps into ν 𝔽 commuting with out through the same coalgebra are equal — chain el-nu-eta through the corecursor they both equal. This is the internal BISIMULATION-IMPLIES-EQUALITY principle: a bisimulation is a coalgebra on its own carrier, and its two projections commute.

COINDUCTION, RELATIONAL FORM — el-nu-eta's corollary adopted as a rule for the kernel's convenience (the el-squash-e-eq precedent: ADMISSIBLE, kept because the kernel replays it directly). It needs one more ≜-meta-operation, the RELATOR lift_𝔽(R) — the relation lifting of a polynomial: for Γ ▷ ν 𝔽 ▷ (ν 𝔽)[↑] ⊦ R : Ω and elements u, v of ⌊𝔽⌋(ν 𝔽)'s decoding (R's base weakens under every binder the clauses cross; its own two binders lift over it):

    lift_𝕏(R) u v           R[id, u, v]
    lift_{K a}(R) u v       u  v  El a
    lift_{𝔽  𝔾}(R) u v     Prf (lift_𝔽(R) (u .π₁) (v .π₁))
                                 Prf (lift_𝔾(R) (u .π₂) (v .π₂))
    lift_{𝔽  𝔾}(R) u v     ⊎-elim at motive Ω, on u then v:
                             the diagonal branches lift the
                             payloads, the off-diagonal ones are ⊥
                             — definitional collapse at canonical
                             forms, the tag mismatch judgementally
                             visible
    lift_{El a  𝔽}(R) u v  (h : Prf (u .π₁  v .π₁  El a))
                                 Prf (lift_{𝔽[u .π₁]}(R) (u .π₂) (v .π₂))
                             # the two instances are ≐ under h by
                             # el-reflect — no transport, the same
                             # extensional degeneration as the
                             # QIIT ᴰ-clauses
    lift_{El a  𝔽}(R) u v  (x : El a)  Prf (lift_𝔽(R) (u x) (v x))
Γ  𝔽 poly
Γ  ν 𝔽  (ν 𝔽)[]  R : Ω
Γ  p : Prf R[id, t₀, t₁]
Γ  ν 𝔽  (ν 𝔽)[]  Prf R  q : Prf (lift_𝔽(R) (out ) (out ))
Γ  t₀ : ν 𝔽      Γ  t₁ : ν 𝔽
Γ  t₀  t₁ : ν 𝔽

DERIVATION

(why admissible). From R build the subset carrier b ≜ (νᶜ ⨯ νᶜ) ⨯ prf R — νᶜ the ν-code, prf the derivable prf-code of the Ω block's impredicativity note — with the coalgebra observing the FIRST component, the closure q transporting the invariant to the tails; both projections commute with out (the second by q's head equations, reflected), so el-nu-eta equates them through the corecursor, and instantiating at (t₀, t₁, p) gives the conclusion. The kernel replays the rule as stated instead (a ⋆-payload — docs/NovaKernel.txt §8): the subset-carrier construction is the JUSTIFICATION, not the implementation.

SUBSTITUTION ACTION

Substitution acts through the carried polynomial (𝔽[σ] the evident meta-operation: σ on the embedded Nova pieces, lifted under the binders; the hole is inert):

    (ν 𝔽)[σ]         ν 𝔽[σ]          (type and code)
    (out t)[σ]       out t[σ]
    (corec 𝔽 a f x)[σ]   corec 𝔽[σ] a[σ] f[σ] x[σ]

NOTES

  • LAMBEK. in ≜ λ (corec 𝔽 ⌊𝔽⌋(ν 𝔽) (map_𝔽 (λ (out ☐₀)) ☐₀) ☐₀) inverts out up to ≐ — out ∘ in by el-nu-beta plus the functor laws, in ∘ out by el-nu-eta — so ν 𝔽 ≅ El ⌊𝔽⌋(ν 𝔽) elementwise, while the TYPES stay structurally distinct (IDENTITY above).
  • SUBSUMPTION (conservativity). Every ν 𝔽 is definable: with F̂ⁿ(𝟙) : 𝕌 by ℕ-elim at motive 𝕌, the ℕ-indexed limit (g : ℕ → El (F̂ⁿ 𝟙)-family) ⨯ Prf (restriction coherence) is a final 𝔽-coalgebra — containers preserve this limit — with out, corec and both laws provable (β up to lemmas, η by ℕ-induction and funext-via-reflection). The scheme is retained for structural identity, one-step β, and the uniform η; the encoding is its justification, exactly as the QIIT SEMANTICS note is for that scheme.
  • SEMANTICS. In the setoid model the carrier of ν 𝔽 is the meta-level limit above (the descending chain of the monotone operator, converging at ω), and the relation is the LARGEST BISIMULATION — el-nu-eta is finality, validated on the nose. Models that fail finality are hereby excluded, as models failing initiality are by the QIIT notes.
  • DELIBERATE OMISSIONS, each with a known upgrade path: no internal fixpoints in the grammar (interleaved nesting like ν of X ↦ A ⨯ List X needs the inner functor reified to shape-and-positions form by hand; non-interleaved nesting is free through K-constants at previously formed ν/QIIT codes); no indexed or mutual coinductive sorts and no coequations (those want the full dual theory of cosignatures); no ν under a QIIT constructor domain (an inner ν forces infinitary branching, which the finitary ToS grammar excludes).

EXAMPLES

    Stream a   ν (K a  𝕏)
    Conat      ν (K 𝟙  𝕏)
    Colist a   ν (K 𝟙  (K a  𝕏))
    Cotree a   ν (K 𝟙  (K a  (𝕏  𝕏)))    # leaf/node infinite trees
    Moore a b  ν (K b  (El a  𝕏))

head, tail, and friends are out followed by projections and ⊎-elim; constructors (cons, and Cotree's leaf/node) are in instances. Surface codata declarations elaborate to ν-polynomials — docs/NovaElaboration.txt's business.

Rules (elem list)

Γ ctx
Γ  · : ε
Γ  A  Δ tel
Γ  e : A
Γ  ē : Δ[id, e]
Γ  e, ē : A  Δ
Γ  A  Δ tel
Γ  e₀  e₁ : A
Γ  ē₀  ē₁ : Δ[id, e₁]
Γ  (e₀, ē₀)  (e₁, ē₁) : A  Δ
Γ₁  ē : Δ
σ : Γ₀  Γ₁
sp-sub# defined by meta-level induction on ē
Γ₀  ē[σ] : Δ[σ]
σ : Γ₀  Γ₁
Γ₀  ·[σ]  · : ε
Γ₁  e : A
Γ₁  A  Δ tel
Γ₁  ē : Δ[id, e]
σ : Γ₀  Γ₁
Γ₀  (e, ē)[σ]  e[σ], ē[σ] : A[σ]  Δ[σ]
Γ  Γ' ctx
Γ  ē : Δ
Γ'  ē : Δ
Γ  Δ  Δ' tel
Γ  ē : Δ
Γ  ē : Δ'
Γ  Γ' ctx
Γ  ē  ē' : Δ
Γ'  ē  ē' : Δ
Γ  Δ₀  Δ₁ tel
Γ  ē₀  ē₁ : Δ₀
Γ  ē₀  ē₁ : Δ₁
Γ₁  ē₀  ē₁ : Δ
σ₀  σ₁ : Γ₀  Γ₁
Γ₀  ē₀[σ₀]  ē₁[σ₁] : Δ[σ₁]

Rule name scheme

Names follow <class>-<former>-<kind> uniformly (see Conventions). The equivalence schema instances are ctx-refl/-sym/-trans, sub-…, sub-norm-…, ty-…, el-…, tel-…, sp-…. The poly class has well-formedness rules only (polynomials are inert syntax, no equality judgement). All other names appear verbatim on their rules; there are no synonyms.

Nova Model

Rendered from docs/NovaModel.txt — the plain text remains the source of truth.

NovaModel.txt — the standard meta-circular model

Preface

This file constructs the STANDARD (meta-circular) model of a fragment of docs/NovaFoundation.txt: Nova read as a category with families (CwF) inside a bigger, extensional type theory — the META-THEORY 𝒱 below. Each object-level feature is interpreted by its meta-level copy: object ℕ by meta ℕ, object Π by meta Π, object reflection by meta reflection. The model witnesses SOUNDNESS of the fragment's rules and CONSISTENCY relative to the meta-theory; it deliberately does not address canonicity or normalization (see Scope).

FRAGMENT

The formers 𝟘, 𝟙, ℕ, Π, Σ, the universe 𝕌 with its codes {𝟘, 𝟙, ℕ, →, ⨯} and El-decoding, and extensional equality in the composite form Prf (a₀ ≡ a₁ ∈ A) — formation (code-eq under Prf), introduction (el-eq-i), reflection (el-reflect), and proof irrelevance (el-prf-prop). Signatures are DEFINITIONAL only. Judgement classes covered: sig, ctx, sub, sub-norm, ty, el, and the coercion and congruence rules of each; telescopes and element lists are not needed by these formers. Excluded, with upgrade paths in the final section: Ω proper (∥·∥, code-prop-eq, the squash eliminators), quotients, QIITs.

THE ONE DESIGN DECISION

Types are NOT interpreted as meta-types. Foundation's injectivity block (ty-pi-inj, ty-sigma-inj, ty-el-inj, code-pi-inj, ...) is a semantic commitment that the naive reading — ⟦A → B⟧ a meta function type — REFUTES: meta function types are not injective in their components (Foundation's own remark: in the plain set model both 𝟙 → 𝟘 and ℕ → 𝟘 are empty). So the model interprets both 𝕌 and the judgement `Γ ⊦ A type` into CODE UNIVERSES — inductive-recursive types of names-with-decodings defined in the meta — where equality of types is equality of codes, and injectivity is the meta's ordinary constructor injectivity. Everything else is standard: elements decode to genuine meta values, functions are meta functions. The codes are exactly the model-side image of Foundation's structural commitment: a type IS its head-constructor tree.

NOTATION

⟦·⟧ is semantic interpretation (this file's use is unrelated to Foundation's method-image ⟦·⟧). γ ranges over semantic environments. Meta-level syntax is written with Nova's symbols (λ, →, ⨯, Σ-pairs (·,·)) — the meta is itself a type theory, and context disambiguates. ≜ marks defining clauses of the interpretation (meta-level definitions), as elsewhere.

The meta-theory

The meta-theory is an EXTENSIONAL type theory with:

  • 𝟘, 𝟙, ℕ, Π, Σ — with their dependent eliminators;
  • extensional identity Id — reflection, function extensionality, uniqueness of identity proofs (UIP); its canonical proof refl;
  • two cumulative universe levels 𝒱₀ : 𝒱₁ (𝒱₀ ⊆ 𝒱₁);
  • inductive and INDUCTIVE-RECURSIVE definitions (Dybjer–Setzer) at both levels, with the meta's usual constructor injectivity and no-confusion.

Where each capability is spent (the trust ledger):

  • meta ℕ-eliminator → el-nat-e/-beta, and termination of object recursion is INHERITED from meta ℕ's well-foundedness, not proven;
  • meta reflection → el-reflect; also silently, coherences like El₁ ∘ el = El₀ below;
  • meta funext → every ≐-judgement under a binder (equality of interpretations is pointwise), el-pi-eta, ty-zero-elim;
  • meta UIP → el-prf-prop;
  • meta surjective pairing→ el-sigma-eta;
  • induction-recursion → the code universes (hence the injectivity block); IR is replaceable by an indexed-inductive encoding at the cost of one level, noted below;
  • constructor injectivity→ ty-pi-inj, ty-sigma-inj, code-*-inj.

This model REALLOCATES trust upward rather than discharging it: the meta contains a structural copy of each object feature (extensionality included), and consistency is obtained RELATIVE to the meta's. Foundation's preface commits to the SETOID MODEL — types as code-with-relation pairs — of which this file constructs the CODE layer; the relation layer is the setoid refactoring named in the final section (trivial for every former here: the fragment has no quotients, so all relations are equality of decodings). This document exists because the code layer is the cheapest complete soundness witness for the structural fragment, and the template into which further formers' clauses slot one by one.

Semantic universes

Two inductive-recursive code universes, one per size. Code₀ interprets 𝕌; Code₁ interprets the judgement `type`. Each is a meta-level data type of NAMES given together with its decoding function; the decoding clause of each constructor is written to its right.

Small codes — the denotation of 𝕌:

    Code₀ : 𝒱₀        El₀ : Code₀  𝒱₀      # by induction-recursion
    zero₀  : Code₀                                    El₀ zero₀         𝟘
    one₀   : Code₀                                    El₀ one₀          𝟙
    nat₀   : Code₀                                    El₀ nat₀          
    pi₀    : (a : Code₀) (b : El₀ a  Code₀)  Code₀  El₀ (pi₀ a b)     (x : El₀ a)  El₀ (b x)
    sigma₀ : (a : Code₀) (b : El₀ a  Code₀)  Code₀  El₀ (sigma₀ a b)  (x : El₀ a)  El₀ (b x)

Large codes — the denotation of `type`. Same formers one level up, plus a code for 𝕌 itself and a code for equality types. eq is the ONLY constructor whose decoding is an Id-type; its arguments are a code and two elements of its decoding, so equality types exist at every type, 𝕌 included — Foundation's "equality props exist at large types".

    Code₁ : 𝒱₁        El₁ : Code₁  𝒱₁      # by induction-recursion
    zero₁  : Code₁                                    El₁ zero₁         𝟘
    one₁   : Code₁                                    El₁ one₁          𝟙
    nat₁   : Code₁                                    El₁ nat₁          
    pi₁    : (a : Code₁) (b : El₁ a  Code₁)  Code₁  El₁ (pi₁ a b)     (x : El₁ a)  El₁ (b x)
    sigma₁ : (a : Code₁) (b : El₁ a  Code₁)  Code₁  El₁ (sigma₁ a b)  (x : El₁ a)  El₁ (b x)
    univ   : Code₁                                    El₁ univ          Code₀
    eq     : (c : Code₁) (x y : El₁ c)  Code₁        El₁ (eq c x y)    Id (x, y)

The embedding of small codes into large ones is a DEFINED RECURSION, not a constructor — this is what makes the El-decoding rules (ty-el-zero ... ty-el-sigma) hold definitionally rather than clash with structural code equality:

    el : Code₀  Code₁
    el zero₀          zero₁
    el one₀           one₁
    el nat₀           nat₁
    el (pi₀ a b)      pi₁ (el a) (λ x. el (b x))
    el (sigma₀ a b)   sigma₁ (el a) (λ x. el (b x))

Two lemmas about el, both by Code₀-induction:

  • DECODING COHERENCE: El₁ (el c) = El₀ c. (Propositional in the meta, hence judgemental by meta reflection; used silently below whenever an element of El₀ is used at El₁.)
  • INJECTIVITY: el c = el c′ implies c = c′. (el maps distinct constructors to distinct constructors and is injective on each argument, recursively; note el never produces univ or eq.) This is the semantic content of ty-el-inj.

The CwF

The semantic category with families, all laws holding definitionally in the meta:

objects semantic contexts: meta types in 𝒱₁ morphisms meta functions

  Ty(X)           X  Code₁                (type families as code families)
  Tm(X, A)        (γ : X)  El₁ (A γ)
  A[f]            A  f                    (substitution = composition)

terminal 𝟙

  comprehension  X.A  (γ : X)  El₁ (A γ),  p  .π₁,  q  .π₂

The interpretation below is the evident partial map from raw syntax into this CwF: partial because raw syntax includes garbage; the soundness theorem states it is defined and coherent on every derivable judgement.

Interpretation

Contexts and substitutions.

    ε        𝟙
    Γ  A    (γ : Γ)  El₁ (A γ)
    · γ        ()
    σ, t γ     (σ γ , t γ)
    id γ       γ
     γ        γ .π₁
    σ  τ γ    σ (τ γ)
    # normal substitutions e˲ by the same clauses (· and extension).

Variables.

     γ      γ .π₂
    ₙ₊₁ γ     (γ .π₁)

Types — a code family ⟦A⟧ : ⟦Γ⟧ → Code₁ per type over Γ.

    𝟘 γ                      zero₁
    𝟙 γ                      one₁
     γ                      nat₁
    𝕌 γ                      univ
    A  B γ                  pi₁    (A γ) (λ x. B (γ, x))
    A  B γ                  sigma₁ (A γ) (λ x. B (γ, x))
    El t γ                   el (t γ)
    Prf (a₀  a₁  A) γ      eq (A γ) (a₀ γ) (a₁ γ)
    A[σ]                     A  σ
    # In this fragment Prf appears only in the composite above; Ω is
    # not itself a type of the fragment.

Elements — ⟦t⟧ : (γ : ⟦Γ⟧) → El₁ (⟦A⟧ γ). The universe codes (elements of 𝕌) land in Code₀ = El₁ univ; the element formers land in the decodings; disambiguation is by the typing judgement, as in Foundation's grammar.

    𝟘 γ          zero₀                        # : Code₀   (code-zero)
    𝟙 γ          one₀
     γ          nat₀
    t  u γ      pi₀    (t γ) (λ x. u (γ, x))
    t  u γ      sigma₀ (t γ) (λ x. u (γ, x))
    () γ             ()
    Z γ              Z
    S t γ            S (t γ)
    ℕ-elim z s t γ   ℕ-elim (z γ) (λ n r. s ((γ, n), r)) (t γ)   # the META recursor
    𝟘-elim t γ       𝟘-elim (t γ)                                    # meta absurdity
    λ f γ            λ x. f (γ, x)
    f e γ            f γ (e γ)
    (a , b) γ        (a γ , b γ)
    t .π₁ γ          t γ .π₁
    t .π₂ γ          t γ .π₂
     γ              refl
    t[σ]             t  σ
    # ⟦⋆⟧ is the clause where partiality is visible: refl is
    # well-typed at Id (⟦a₀⟧ γ, ⟦a₁⟧ γ) only when the equation holds
    # in the meta — exactly what el-eq-i's premise supplies.

Signatures. A definitional signature is interpreted entry by entry: (Γ ⊦ x ≔ a : A) defines the meta function ⟦x⟧ ≜ ⟦a⟧ (over ⟦Γ⟧), and a reference interprets by instantiation, ⟦x[e˲]⟧ γ ≜ ⟦x⟧ (⟦e˲⟧ γ); ditto type definitions. el-sig-beta / ty-sig-beta then hold definitionally. Open signatures are not interpreted: per Foundation's DEFINITIONAL AND OPEN SIGNATURES an open signature denotes the class of its definitional refinements, and this model interprets each refinement.

Soundness

THEOREM

(soundness). By induction on derivations, for the fragment's rules:

Γ ctx ⟹ ⟦Γ⟧ : 𝒱₁ defined σ : Γ₀ ⇒ Γ₁ ⟹ ⟦σ⟧ : ⟦Γ₀⟧ → ⟦Γ₁⟧ defined Γ ⊦ A type ⟹ ⟦A⟧ : ⟦Γ⟧ → Code₁ defined Γ ⊦ a : A ⟹ ⟦a⟧ : (γ : ⟦Γ⟧) → El₁ (⟦A⟧ γ) defined Γ₀ ≐ Γ₁ ctx ⟹ ⟦Γ₀⟧ = ⟦Γ₁⟧ Γ ⊦ A₀ ≐ A₁ type ⟹ ⟦A₀⟧ = ⟦A₁⟧ (pointwise, by funext) Γ ⊦ a₀ ≐ a₁ : A ⟹ ⟦a₀⟧ = ⟦a₁⟧ (σ-, e˲-equality analogously)

All equalities are the meta's Id, which by meta-extensionality is as strong as needed. Notes on the load-bearing cases; everything not listed is a one-line congruence or holds definitionally.

  • SUBSTITUTION CALCULUS. Every ≜-law of Foundation's substitution action (ty-sub-*, el-sub-*, var-sub-*, sub-assoc, sub-eta, ...) holds definitionally: substitution is interpreted as composition, and the clauses were arranged compositionally.
  • η-RULES. el-pi-eta ← meta funext (+ η); el-sigma-eta ← meta surjective pairing; el-one-prop ← meta 𝟙-uniqueness; el-zero-prop ← meta 𝟘-elimination. el-nat-eta ← meta ℕ-induction: the two candidates agree at Z, each commutes with S, so they agree pointwise (meta induction), hence are equal (funext). Note the pattern: uniqueness rules are THEOREMS of the meta, proved by the meta's induction — the model inherits them, it does not decide them.
  • EQUALITY BLOCK. el-eq-i ← refl (see the ⟦⋆⟧ clause); el-reflect ← meta reflection: an element of El₁ (eq c x y) = Id (x, y) reflects to x = y in the meta, which pointwise (all γ) is the conclusion's meaning; el-prf-prop ← meta UIP. code-eq congruence (equal components give equal eq-codes) is structural.
  • ty-zero-elim. A term ⟦t⟧ : (γ : ⟦Γ⟧) → 𝟘 makes ⟦Γ⟧ empty pointwise; two code families out of an empty domain are equal by funext through 𝟘-elim.
  • COERCION RULES (el-ty-coe, sub-coe-*, ...). Type equality is literal equality of code families, so the coerced object is re-typed UNCHANGED — the model's counterpart of Foundation's no-op coercion discipline.
  • INJECTIVITY BLOCK — the reason this model exists in this shape: ty-pi-inj, ty-sigma-inj ← constructor injectivity of pi₁/sigma₁ in the meta: equal codes have equal heads and equal arguments; the second components are equal as functions, i.e. pointwise — exactly the rules' under-binder conclusions. code-pi-inj, code-sigma-inj ← the same at Code₀. ty-el-inj ← the el-injectivity lemma above. No-confusion (a Π-type never equal to ℕ, ...) holds in the model by the meta's no-confusion for inductive types — consistent with Foundation, which keeps it a meta-property.

COROLLARIES

  • CONSISTENCY (relative). ⟦𝟘⟧ decodes to meta 𝟘, so a derivation of ε ⊦ t : 𝟘 would yield a meta element of 𝟙 → 𝟘: the fragment is consistent if the meta-theory is.
  • The injectivity block is REALIZABLE: Foundation's remark that those rules exclude the collapsing set model is answered constructively — the code-universe model satisfies all of them at once. Structural type equality is not merely consistent; it has a standard-flavored model.
  • NOT PROVIDED: canonicity and normalization. The model maps syntax INTO the meta and never back; establishing that every closed ⊦ t : ℕ is ≐-equal to a numeral requires a readback and its correctness — a gluing/logical-relations argument over this model, carried out (for closed terms) in docs/NovaSyntax.txt, which uses this model twice: as the target of evaluation and for the injectivity half of canonicity. Likewise nothing here is an algorithm; decidability is not addressed (and the full theory's ≐ is undecidable by design).

Excluded features and their upgrade paths

  • code-prop-eq (propositional extensionality) FAILS in this model, by design of the fragment: eq-codes are compared structurally, so the equi-true (Z ≡ Z ∈ ℕ) and (S Z ≡ S Z ∈ ℕ) denote DISTINCT codes. This is the correct price for a constructive-friendly meta. The upgrade is the truth-value interpretation: in a CLASSICAL meta, interpret equality codes by excluded-middle case split —
   Prf (a₀  a₁  A) γ  one₁ if a₀ γ = a₁ γ, zero₁
   otherwise — and   (). Then iff-equal equations denote the

SAME code, prop-ext holds, and this clause is the germ of the full Ω interpretation: Ω as a small complete lattice of meta truth values (classical 𝟚, a topos subobject classifier, or an impredicative meta-Prop), with ∥A∥ ↦ inhabitation of ⟦A⟧. Nova's Ω quarantine (no elimination into types, no unique choice, no Ω-code in 𝕌) is exactly what keeps that non-computational clause invisible to the data layer.

  • QUOTIENTS need the setoid refactoring of the model — types as code-with-relation pairs, the reading Foundation's preface commits to — where they are FREE: same carrier, coarsen the relation. (Alternatively, meta quotient types over the bare code model; then they cost whatever the meta charges for them.)
  • QIITs need meta QIITs — meta-circularity at its purest: the scheme is interpreted by its meta copy, initiality inherited, not proven. The from-below justification is Foundation's SEMANTICS note (initial algebras in the setoid model: constructor-term carriers with the generated congruence).
  • INDUCTION-RECURSION in the meta can be avoided: replace each code universe by an indexed inductive family over a separately given decoding target, or by a W-type encoding, at the cost of bookkeeping and one universe level. The IR presentation is used here because it makes every decoding clause definitional.

The ledger, restated once: this model interprets each feature by its meta copy, so its verdict is always RELATIVE — sound and consistent if the meta is. What it buys is precision about WHICH meta capabilities each rule consumes (the table in the meta-theory section), a reusable template for new formers, and the demonstration that the structural fragment — injectivity block included — has a standard model. What it cannot buy, by construction, is the analyzed foundation underneath: that is the setoid model of Foundation's preface — code-with-relation pairs — of which this file is the structural half, the relation half arriving with the formers (quotients, Ω, QIIT congruences) that actually consume it.

Nova Syntax

Rendered from docs/NovaSyntax.txt — the plain text remains the source of truth.

NovaSyntax.txt — intrinsic syntax (QIIR) and the representability theorem

Preface

This file presents the same fragment as docs/NovaModel.txt — 𝟘, 𝟙, ℕ, Π, Σ, the structural universe 𝕌 with El, and extensional equality Prf (a₀ ≡ a₁ ∈ A) — from the INTRINSIC side: the syntax as ONE simultaneous definition inside the meta-theory, by QUOTIENT INDUCTION-INDUCTION-RECURSION (QIIR). Substitutions are SYNTAX — ground trees with id, ↑ and composition as constructors, exactly Foundation's grammar σ ::= · | σ, t | σ ∘ σ | id | ↑ — but the substitution ACTION on types and terms is not: it is a meta-level operation defined by recursion MUTUALLY with the sorts and constructors that mention it. On top of the syntax, the file states the REPRESENTABILITY THEOREM: which meta types are isomorphic to their closed Nova counterparts, in what sense, and by what proof.

The sweep mirrors docs/NovaFoundation.txt exactly: Foundation's grammar has no T[σ] or t[σ] formers either — its substitution action is "defined by meta-level induction via the ≜-equations" (the ty-sub-*/el-sub-*/var-sub-* blocks), and its calculus laws carry annotations like "true on the nose by induction" (ty-sub-id, ty-sub-comp). The QIIR presentation is that discipline made intrinsic: the ≜-blocks become the defining clauses of the recursion, the annotated laws become meta-theorems about ACTIONS, and the QUOTIENT retains only the mathematically contentful equations — β, η, El-decoding, reflection, irrelevance. Sub itself is UNQUOTIENTED: id ∘ σ and σ are distinct trees whose actions agree; no downstream statement ever needs equality of substitutions, only equality of their actions.

THIN ICE, DECLARED UP FRONT. Unlike a plain QIIT, this definitional scheme — quotiented inductive-inductive sorts whose constructor INDICES mention recursive functions being defined in the same block — has NO settled general metatheory: the theory of signatures covers QIITs, Dybjer–Setzer covers IR, and their combination is past both. Moreover the recursion here is not even structural-by-inspection: its totality is the strong normalization of the substitution calculus (see the Justification section). This file therefore POSTULATES the scheme for THIS ONE INSTANCE, itemizes what the instance must discharge, and keeps the thick-ice fallback — an explicit-substitution QIIT plus a strictification theorem — as the construction that would cash the postulate. One casualty of the thin route is a pleasing self-reference: the explicit-substitution presentation is itself a signature of Foundation's own QIIT scheme; the QIIR presentation is not (Foundation's scheme has no recursion). The fallback keeps that property; the primary presentation trades it for a quotient a fraction of the size.

Relation to the other documents: docs/NovaFoundation.txt is the source of truth this file mirrors rule by rule — its official reading is intrinsic, and this file IS that reading made precise for the fragment (the classification table below records where each rule class lands); docs/NovaModel.txt is the standard model 𝓜, used twice — as the target of evaluation (initiality) and for the injectivity half of canonicity. The meta-theory is NovaModel's, plus the postulated QIIR scheme (a genuine new trust item — the fallback reduces it to finitary QIITs, which are constructible).

The syntax (QIIR)

SORTS

one simultaneous block, all small:

    Con : 𝒱₀                                  # Nova contexts
    Sub : Con  Con  𝒱₀                      # Nova substitutions (SYNTAX)
    Var : (Γ : Con)  Ty Γ  𝒱₀               # de Bruijn variables (☐ₙ)
    Ty  : Con  𝒱₀                            # Nova types
    Tm  : (Γ : Con)  Ty Γ  𝒱₀               # Nova elements

RECURSIVE OPERATIONS

defined mutually with the sorts:

    _[_]  : Ty Δ  Sub Γ Δ  Ty Γ             # substitution action
            (and the Tm instance)

DERIVED NOTATION

(formal composites — no computation involved):

    σ     (σ  , var vz)                   # lift under a binder (sub-lift)
    a    (id, a)                           # single substitution

POINT CONSTRUCTORS

The substitution grammar is Foundation's, constructor for constructor; term/type indices are Foundation's shapes VERBATIM (compare el-var, el-pi-e, el-nat-e):

    # contexts, substitutions, variables
          : Con                              # Foundation's ε
    __    : (Γ : Con)  Ty Γ  Con
    !      : Sub Γ                           # ·
    _,_    : (σ : Sub Γ Δ)  Tm Γ (A[σ])  Sub Γ (Δ  A)
    id     : Sub Γ Γ
          : Sub (Γ  A) Γ
    __    : Sub Δ Ξ  Sub Γ Δ  Sub Γ Ξ
    vz     : Var (Γ  A) (A[])               # ☐₀
    vs     : Var Γ A  Var (Γ  B) (A[])     # ☐ₙ₊₁
    # types (ty-*)
    𝟘 𝟙  𝕌 : Ty Γ
    Π Σ′   : (A : Ty Γ)  Ty (Γ  A)  Ty Γ
    El     : Tm Γ 𝕌  Ty Γ
    Eq     : (A : Ty Γ)  Tm Γ A  Tm Γ A  Ty Γ    # Prf (a₀ ≡ a₁ ∈ A)
    # elements (el-*, code-*)
    var    : Var Γ A  Tm Γ A
    zeroonenat: Tm Γ 𝕌
    pisigma: (a : Tm Γ 𝕌)  Tm (Γ  El a) 𝕌  Tm Γ 𝕌
    lam    : Tm (Γ  A) B  Tm ΓA B)
    app    : Tm ΓA B)  (a : Tm Γ A)  Tm Γ (B[a])
    pair   : (a : Tm Γ A)  Tm Γ (B[a])  Tm Γ (Σ′ A B)
    π₁     : Tm Γ (Σ′ A B)  Tm Γ A
    π₂     : (t : Tm Γ (Σ′ A B))  Tm Γ (B[π₁ t])
    tt     : Tm Γ 𝟙
    Z      : Tm Γ 
    S      : Tm Γ   Tm Γ 
    ℕ-elim : (A : Ty (Γ  ))  Tm Γ (A[Z])
               Tm (Γ    A) (A[  , S (var (vs vz))])
               (t : Tm Γ )  Tm Γ (A[t])
    𝟘-elim : Tm Γ 𝟘  Tm Γ A
    star   : (a : Tm Γ A)  Tm Γ (Eq A a a)         # el-eq-i

THE RECURSION'S DEFINING CLAUSES — the intrinsic transcription of Foundation's ≜-blocks. The variable and substitution-structure cases mirror var-sub-hit/-miss/-wk/-id/-comp verbatim; the former cases mirror ty-sub-*/el-sub-*; the remaining formers are structural in the same pattern:

    (var vz)[σ, t]       t                   # var-sub-hit
    (var (vs x))[σ, t]   (var x)[σ]          # var-sub-miss
    (var x)[]           var (vs x)          # var-sub-wk
    t[id]                t                   # var-sub-id / el-sub-id
    t[σ  τ]             t[σ][τ]             # var-sub-comp / el-sub-comp
A B)[σ]           Π (A[σ]) (B[σ])    # ty-sub-pi
    (El t)[σ]            El (t[σ])           # ty-sub-el
    (Eq A a₀ a₁)[σ]      Eq (A[σ]) (a₀[σ]) (a₁[σ])
    (lam t)[σ]           lam (t[σ])         # el-sub-lam
    (app f a)[σ]         app (f[σ]) (a[σ])   # el-sub-app
    (ℕ-elim A z s t)[σ]  ℕ-elim (A[σ]) (z[σ]) (s[σ]) (t[σ])

TWO HALLMARKS OF THE THIN ICE, stated rather than hidden:

  • TERMINATION IS NOT STRUCTURAL. At the ∘-clause the subject of the inner recursive call is an arbitrary result; at the binder clauses the substitution grows (σ⁺ contains σ ∘ ↑). These clauses are exactly the substitution fragment of the λσ-calculus, and the recursion's totality is that fragment's STRONG NORMALIZATION (Abadi–Cardelli–Curien–Lévy; Curien–Hardin–Lévy) — a true but non-obvious rewriting theorem, entered into the Justification ledger below. Only the σ-fragment is run: β is a quotient equation, never a clause, so the famous failure of PSN for full λσ is not in play.
  • WELL-TYPEDNESS IS SIMULTANEOUS. Some clauses typecheck only up to the calculus laws being established at the same time — the app clause needs (B[⟨a⟩])[σ] = (B[σ⁺])[⟨a[σ]⟩], an instance of composition-and-extension laws. In an intensional meta this is the notorious transport wall; in this file's extensional meta, reflection lets the clauses be accepted while the laws are discharged in the same mutual induction.

EQUATION CONSTRUCTORS

the quotient, ONLY the contentful equations, cited by the Foundation rule each mirrors. Sub carries NO equations:

reflect is the one CONDITIONAL equation (premise a term of the syntax); every induction over the syntax must validate it — extensionality concentrates there.

WHERE EVERY FOUNDATION RULE WENT

the classification:

formation / introduction / elimination rules, and the substitution grammar (·, ext, id, ↑, ∘)

       point constructors

substitution actions (ty-sub-*, el-sub-*, var-sub-*)

       defining CLAUSES of the recursion

substitution calculus laws (sub-id-pre, sub-id-post, sub-assoc, sub-wk-ext, sub-eta, sub-empty-unique, ty-sub-id, ty-sub-comp, ...)

       META-THEOREMS about ACTIONS (next section); Sub itself is
        unquotiented and distinguishes the trees

β / η / El-decoding / reflection / irrelevance

       equation constructors (the quotient)

congruence rules

       meta-congruence (free intrinsically)

injectivity block (ty-pi-inj, code-pi-inj, ...)

       a property of MODELS, realized by docs/NovaModel.txt

Substitution laws as meta-theorems

Sub is unquotiented, so the calculus laws are stated at the level where they are used: the ACTIONS of both sides agree on every subject. Provable by the standard nested structural inductions:

A[id] = A (ty-sub-id; a clause here)

    A[σ  τ]       = A[σ][τ]                 (ty-sub-comp; a clause here)
    A[id  σ]      = A[σ] = A[σ  id]        (sub-id-pre/-post)
    A[(σ  τ)  υ] = A[σ  (τ  υ)]          (sub-assoc)
    A[  (σ, t)]  = A[σ]                    (sub-wk-ext)
    A[(, var vz)] = A                       (sub-eta)
    naturality of every former               (the clause shapes)

(Some are literally clauses of the recursion, recorded above; the rest follow by induction — Foundation's "true on the nose by induction" annotations, now living where they always pointed.) In the extensional meta each law, once proven, is judgemental downstream. Nothing anywhere needs σ = τ AS TREES: the constructor indices, the quotient equations, and the gluing all consume substitutions only through their actions.

Justification: the postulated scheme and its fallback

WHAT IS POSTULATED

The simultaneous definition above determines: (i) the sorts and constructors, with the quotient imposed; (ii) the recursive action, its defining clauses holding judgementally; (iii) a dependent ELIMINATOR: any displayed structure over the sorts that is closed under the constructors, respects the equations (reflect included), and is compatible with the action's clauses, has a unique section.

WHAT THE INSTANCE MUST DISCHARGE

  • TERMINATION — strong normalization of the substitution fragment (the λσ σ-rules), NOT structural recursion; the classical proofs go through polynomial interpretations. This is the thin route's replacement for a visibly well-founded definition;
  • QUOTIENT-RESPECT — the action respects every equation constructor: substitution commutes with β, η, the decodings, and reflect (if a closed proof identifies a₀ = a₁, their substitution images are identified). The classical substitution lemmas, promoted to well-formedness obligations of the definition itself;
  • SIMULTANEOUS WELL-TYPEDNESS — the clause/law entanglement noted above, dischargeable in the extensional meta.

THE FALLBACK

(thick ice). Add point constructors _[_] for Ty/Tm, and add the substitution calculus as equation constructors (the full sub-* block plus one naturality equation per former). That is an ordinary FINITARY QIIT — constructible, no new scheme — and it is itself a signature of Foundation's own QIIT scheme. The STRICTIFICATION THEOREM then states: the recursive action is definable over it, every term is equal to a substitution-normal one, and the QIIR presentation above is isomorphic to the explicit-substitution QIIT. Under that theorem the postulate is a theorem and the thin ice bears; this file keeps the QIIR form primary because every downstream induction sheds the substitution-law coherences.

(A middle route exists and is recorded once: stratify the recursion through a separate sort of THINNINGS — order-preserving embeddings — with substitutions as term tuples and id/↑/∘ defined. That variant's two recursions are structural by inspection, trading the σ-SN obligation for a bootstrap sort that Foundation has no counterpart of. This file prefers the syntactic Sub: grammar-faithful to Foundation, no auxiliary sort, one classical rewriting theorem as the price.)

Global sections and the question

Write ⟨A⟩ ≜ Tm ◇ A for the CLOSED elements of A : Ty ◇, and emb : ℕ → ⟨ℕ⟩ for the numeral embedding (emb 0 ≜ Z, emb (n+1) ≜ S (emb n)). Initiality maps the syntax into 𝓜 (docs/NovaModel.txt); restricted to ◇ that map is the EVALUATOR, and it already gives non-degeneracy (⟦Z⟧ ≠ ⟦S Z⟧) and the emptiness of Tm ◇ 𝟘 — consistency.

The question: for which closed A is ⟨A⟩ isomorphic to its meta counterpart? Three classes, and the split is forced:

  • CLASS A — iso by the quotient's own equations, no theorem: 𝟙 (el-one-prop), Σ′ (β/η: ⟨Σ′ A B⟩ ≅ (t : ⟨A⟩) ⨯ ⟨B[⟨t⟩]⟩), Eq (star and reflect mutually inverse up to eq-irr: ⟨Eq A a₀ a₁⟩ ≅ Id (a₀, a₁)). The extensional equality fragment transports for free.
  • CLASS B — iso, but each a hard theorem: ⟨𝟘⟩ ≅ 𝟘 (consistency), ⟨ℕ⟩ ≅ ℕ (canonicity). Proof: the glued model below.
  • CLASS C — NOT an iso: Π. ⟨Π ℕ ℕ⟩ ≅ (⟨ℕ⟩ → ⟨ℕ⟩) fails in both directions. No surjection — DEFINABILITY: the meta defines this very file, so it proves total functions ℕ → ℕ that no Nova term denotes (Gödel's floor, not a removable gap). No injection — ω-INCOMPLETENESS: two closed functions can agree on every numeral yet not be derivably equal (equality under x : ℕ is derivability under a FREE variable; "true at all closed instances ⟹ derivable" is an ω-rule the finitary quotient lacks). Slogan: positive formers cross the syntax/meta boundary as isomorphisms; negative formers only map inward (the application map ⟨Π A B⟩ → ((a : ⟨A⟩) → ⟨B[⟨a⟩]⟩) always exists).

The glued model

The device proving Class B and repairing Class C: a proof-relevant logical predicate over the syntax — GLUING along global sections — presented as a displayed model 𝒢 over the syntax; the eliminator (initiality) produces a section of it. Each sort acquires a tracking layer (over a closed base; the displayed general form is over Sub ◇ Γ):

    context Γ      Trk Γ : Sub  Γ  𝒱₁
    type A         Trk A : (γ : Sub  Γ)  Trk Γ γ  Tm  (A[γ])  𝒱₁
    term a         its tracking proof at every tracked closing
    substitution   preservation of tracking (the swept action
                    shows up HERE, once: tracking is STABLE under
                    the action — a lemma by the same induction
                    that defines it, and the only residue of the
                    sweep in the proof)

Type-level clauses at closed instances:

    Trk 𝟘        t     𝟘
    Trk 𝟙        t     𝟙
    Trk         t     (n : )  Id (t, emb n)
    TrkA B)  t     (s : A)  Trk A s  Trk (B[s]) (app t s)
    Trk (Σ′ A B) t     Trk A (π₁ t)  Trk (B[π₁ t]) (π₂ t)
    Trk (Eq A a₀ a₁) t  𝟙
    Trk 𝕌        t     a tracked small code: t -equal to a code
                         built from zero/one/nat/pi/sigma′ with
                         tracked components (the small/large split
                         mirrors NovaModel's Code₀/Code₁)
    Trk (El c)   t     Trk (decoding of the tracked code of c) t

TWO LEMMAS, then the theorem.

  • TRACKING IS A MERE PREDICATE — at most one inhabitant, by induction on the clauses: at ℕ because emb is INJECTIVE (distinct numerals have distinct ⟦·⟧-images in 𝓜 — NovaModel's second use) plus meta UIP; at Π/Σ′ pointwise; at Eq/𝟙/𝟘 trivially.
  • FUNDAMENTAL LEMMA — every term tracks itself: the eliminator applied to 𝒢. With the substitution laws swept out of the quotient, the per-equation coherences are ONLY: the β-laws (the meta computes them), the η-laws (funext + UIP at tracking types), el-nat-eta (meta ℕ-induction on the scrutinee's tracking), the decodings (by the Trk (El c) clause), and REFLECT — the conscious one: a closed inhabitant of Eq A a₀ a₁ must force a₀ = a₁ semantically, and it does, because reflect is an equation of the syntax, so a₀ and a₁ are already identified in the quotient the predicate is defined over. The conditional equation costs nothing at ◇ — which is why the theorem lives at the empty context and does not extend to open ones (no normal forms under inconsistent hypotheses; Foundation's preface). Compatibility with the action is the stability lemma above.

THE REPRESENTABILITY THEOREM

For every closed A : Ty ◇, with 𝒢⟨A⟩ ≜ (t : ⟨A⟩) ⨯ Trk A t the type of TRACKED points:

    𝒢A  A

— forward by projection, back by t ↦ (t, fundamental lemma at t), round-trips by mere-ness of Trk. "A meta type representable in Nova" therefore means: each ELEMENT carries its Nova representative — pointwise representability, not availability of the type former.

COROLLARIES

(Class B, read off at the base clauses):

    𝟘  𝟘     consistency (Trk 𝟘 empty; every closed term tracked)
           canonicity (every closed -term -equal to a unique
                 numeral: fundamental lemma for surjectivity, 𝓜 for
                 injectivity)

At Π the theorem specializes to the honest replacement for Class C: ⟨Π A B⟩ is isomorphic to the type of TRACKED functions — meta functions on tracked points arising by application of a closed term — not to the full meta function space.

Scope and continuations

  • OPEN CONTEXTS / NORMALIZATION. Everything here is at ◇. The open-context analogue needs Kripke/presheaf gluing and FAILS for the full extensional theory (no normal forms under inconsistent hypotheses); what survives is the kernel's fuel-bounded, sound-incomplete approximation (docs/NovaKernel.txt), whose idealized semantics is this file's evaluation direction.
  • EXTENDING THE FRAGMENT. Ω adds a truth-value layer to 𝒢 (tracking at Prf p trivial, as at Eq; the model side needs NovaModel's Ω upgrade first). Quotients add tracked classes (tracking descends along el-quot-eq). Object-level QIITs make the syntax SCHEMATIC (one constructor family per signature); nothing conceptual changes, the bookkeeping grows — and each
   new former adds its -clauses to the recursion and its

quotient-respect obligation to the thin-ice ledger.

  • THE LEDGER, once more. The three classes are a property of the boundary itself: the syntax is finitary and recursively enumerable, the meta is not — data (positive formers) crosses losslessly, behavior (negative formers) crosses only as far as it is tracked by data. Class A is the quotient speaking, Class B is the gluing theorem, Class C is Gödel. Any future former joins one of the three.

Nova Kernel

Rendered from docs/NovaKernel.txt — the plain text remains the source of truth.

NovaKernel.txt — the trusted kernel, rule by rule

Preface

This file writes out every rule the kernel (Nova.Kernel) implements: the fuel-bounded normalizer, proof-spine typing, certificate replay for equality, and item-level re-checking over annotation skeletons. It exists so the kernel can be audited against docs/NovaFoundation.txt clause by clause — every rule below is an instance or a derivable composite of Foundation's rules, and each one names its justification.

Position in the pipeline (docs/NovaPipeline.txt): everything upstream — elaborator, discharge engine, AI — is untrusted and merely PROPOSES; the kernel re-establishes each judgement from its own signature Σ and is the only component whose verdict counts. Nothing here searches and nothing here chooses: every rule is syntax-directed, every premise is checked mechanically, and the sole inputs beyond the core term are the certificate and the skeleton the elaborator hands over.

Notation is Foundation's (contexts Γ, signature Σ, elements t, types

T, judgemental equality , definitional contraction ), with three

kernel-only judgement forms added:

  nf(t) ⇓ t′ , nf(T) ⇓ T′        fuel-bounded normalization
  Σ; Γ  p ⇒ᵖ T                  proof-spine inference
  Σ; Γ  p ⇐ᵖ T                  proof-argument checking
  Σ; Γ  𝒞  t₀  t₁ : T         certificate replay (element equation)
  Σ; Γ  𝒞  T₀  T₁             certificate replay (type equation)
  Σ; Γ  t  T sk              item-level checking (skeleton sk)
  Σ; Γ  t  T sk              item-level inference
  Σ; Γ  T type sk             item-level formation
  Σ; Γ  𝒮 qsig sk             item-level QIIT signature checking (§8)
  Σ; Γ  𝔽 poly sk             item-level polynomial checking (inside
                                 ν formation — Foundation's poly-* rules)

Every kernel judgement is decided inside a FUEL MONAD: a computation either returns, fails with a reason, or exhausts its fuel — and fuel exhaustion is REJECTION, so the kernel is total and every artifact gets a verdict. Fuel is supplied per entry point by the certificate's margin (the elaborator knows its own step counts); one unit is spent

per -contraction, nothing else costs fuel.

1. Normalization: nf, one fuel per contraction

nf mirrors Foundation's  rules clause for clause and normalizes

everywhere (under binders, in all components). The congruence clauses are not listed; the contraction clauses, each of which burns one unit of fuel, are exactly:

  (λ f) e              f[id, e]                    # el-pi-beta
  let a b              b[id, a, ]                 # el-let-beta (a let is
                                                    # ALWAYS a redex: normal
                                                    # forms contain no let)
  (a , b) .π₁          a                           # el-sigma-beta₁
  (a , b) .π₂          b                           # el-sigma-beta₂
  ℕ-elim z s Z         z                           # el-nat-beta-z
  ℕ-elim z s (S n)     s[id, n, ℕ-elim z s n]      # el-nat-beta-s
  ⊎-elim l r (inj₁ a)  l[id, a]                    # el-sum-beta₁
  ⊎-elim l r (inj₂ b)  r[id, b]                    # el-sum-beta₂
  quot-elim f (class a)  f[id, a]                  # el-quot-beta
  out (corec 𝔽 a f x)  map_𝔽 hᵉˡ f[id, x]         # el-nu-beta; map_𝔽 and
                                                    # hᵉˡ = λ (corec 𝔽 a f[↑] ☐₀)
                                                    # expand by Foundation's
                                                    # ≜-clauses at contraction
                                                    # time (one fuel unit)
  𝒮.𝕤-elim  ē (𝒮′.𝕔 θ)  m_𝕔 θφᵉˡ               # el-qiit-beta; fires
                                                    # only when 𝒮 and 𝒮′ are
                                                    # IDENTICAL after nf
  x[]                a[]      (Σ  Γ  x  a : A)   # el-sig-beta
  x[]                T[]      (Σ  Γ  x  T type)  # ty-sig-beta
  El 𝟘                 𝟘                           # El-decoding
  El 𝟙                 𝟙
  El                  
  El (a  b)           El a  El b
  El (a  b)           El a  El b
  El (a  b)           El a  El b
  El (a / r)           El a / r      # the Ω-valued relation is NOT decoded
  El (𝒮.𝕤 ē)           𝒮.𝕤 ē        # ty-el-qiit
  El (ν 𝔽)             ν 𝔽          # ty-el-nu

Ω adds exactly ONE contraction clause:

  Prf p              p             # code-squash-prf (squash is
                                      # idempotent on props)

Otherwise Prf and ∥-∥ are inert: Prf ∥A∥ does NOT reduce to A (realizer irrelevance is the point of the squash), equality props (l ≡ r ∈ A) — Ω-valued, per Foundation — have no contraction, and ⋆ has no eliminator. nf treats Prf/Ω/∥-∥/≡/⋆ congruently beyond the clause above.

QIIT formers (NovaFoundation.txt, QIIT section) normalize congruently everywhere they embed Nova syntax — inside a carried signature's external pieces, the eliminator's motives and methods, index and constructor spines — so the signature-identity test above is plain syntactic equality of normal forms (Foundation's structural identity, nameless: no α). θ⟨φᵉˡ⟩ is Foundation's section spine at the eliminator itself: the contraction materializes one recursive 𝒮.𝕤-elim call per inductive component of θ, and each later contraction of those burns its own fuel. Path constructors add NO contraction — their content is a judgemental equation (el-qiit-path), which enters replay as a step license (§4). A signature is inert syntax and is never itself a redex.

Scrutinees are normalized before the contraction test (call-by-value on elimination positions), so a stuck scrutinee leaves a stuck eliminator — nf never invents progress. A signature reference to a name missing from Σ, or used at the wrong syntactic class (a term definition in type position or vice versa), is rejected outright.

Σ may be OPEN (Foundation, DEFINITIONAL AND OPEN SIGNATURES): during an elaboration run it carries the run's assumed equation constraints and hole declarations. A reference to a DECLARATION is STUCK — typed by el-sig-decl/ty-sig-decl, no contraction — and nf leaves it as a neutral head. Constraint entries are nameless and never referenced by terms, so nf never sees them; they exist for the equational theory (el-sig-eq/ty-sig-eq). Only nf and equality replay tolerate open signatures: Nova.Compute (the uncertified evaluator) assumes a definitional Σ and rejects open entries outright.

HOLE INSTANTIATION

(kCheckSolution / kCheckTySolution): the elaborator may flip a declaration to a definition in place (Foundation, INSTANTIATION — the refinement that never removes judgements). The kernel's part is the legality check, run against the PREFIX Σ preceding the declaration: the proposed body checks at the declared type over the declaration's context, by the skeleton-free tiny checker of §3 (proof-spine typing). A name minted after the hole is absent from the prefix and fails the lookup, which enforces scope and occurs in one stroke; a body outside the tiny checker's fragment is rejected and no flip happens — conservative, never unsound. The declaration's context and type are NOT re-checked here: they are elaborator-made state whose well-formedness is an elaboration invariant, exactly like a constraint entry's statement — and the fragment must not gate which CONTEXTS holes may live in (a Prf ∥-∥ hypothesis would otherwise block every flip under it). The solution alone is the kernel's business.

Fuel is a LIVENESS bound, not a semantic one: under inconsistent hypotheses a well-formed term may have no normal form (see NovaFoundation.txt, preface), and the fuel bound is what keeps the kernel total in that world. Exhaustion never certifies anything.

2. Certificates

The certificate grammar (constructors in parentheses are the implementation's names):

  sel ::=                                          (Sel)
      suc                                          (SelSuc)
    | dom                                          (SelDom)
    | cod u                                        (SelCod)
    | suml                                         (SelSumL)
    | sumr                                         (SelSumR)
    | qdom                                         (SelQDom)
    | qrel u v                                     (SelQRel)
    | qidx i                                       (SelQIdx)
  step ::= (onLhs, path, lic, sels, flip)          (Step)
    onLhs : which side of the equation is rewritten
    path  : child indices from the root to the rewrite point
    lic   : the step's LICENSE — a proof element p (§3, §4), or a
            path license  qpath 𝕔 θ  (§4)
    sels  : component selectors applied to that equation (§5)
    flip  : whether the licensed equation is used right-to-left
  final ::=                                        (Final)
      beta                                         (FBeta)
    | prop                                         (FProp)
    | witness 𝒞?                                   (FWitness)
    | ηΠ 𝒞                                         (FEtaPi)
    | ηΣ 𝒞 𝒞                                       (FEtaSigma)
    | propext s sk t sk                        (FPropExt)
    | prfCong 𝒞                                    (FPrfCong)
    | quotCong 𝒞                                   (FQuotCong)
    | piCong 𝒞 𝒞                                   (FPiCong)
    | sigmaCong 𝒞 𝒞                                (FSigmaCong)
    | sumCong 𝒞 𝒞                                  (FSumCong)
    | qiitCong 𝒞̄ 𝒞̄                                 (FQiitCong)
    | nuCong 𝒞̄                                     (FNuCong)
  The three Ω finals: propext is code-prop-eq — the sides are prop codes
  and s, t are the two hypothetical implications, CHECKED as typings
  (Γ  Prf p  s  Prf q[] and symmetrically); prfCong is ty-prf-cong
  on a TYPE equation (both sides Prf-headed, 𝒞 proves the codes equal at
  Ω); quotCong is ty-quot-cong at a reflexive domain (both sides A / _,
  𝒞 proves the relations equal at Ω under the domain twice). FProp also
  closes an equation at a Prf type (el-prf-prop: proof irrelevance),
  alongside its 𝟙/𝟘 cases. qiitCong is the QIIT congruence (§7): both
  sides sort applications at the same sort position, the first
  certificate vector aligning the two signatures' embedded Nova
  pieces, the second the index spines.
  𝒞 ::= (tyEx?, steps, final)                      (ECert)
    tyEx  : optional TYPE BRIDGE (T′, 𝒞ᵀ) — replay the equation at T′
            instead of the site's type, justified by 𝒞 T  T′ (§7)
    steps : rewrite steps, applied in order
    final : how the sides are closed after the steps

Child indexing, shared by paths, the typed descent (§6) and skeletons (§8) — binders crossed in parentheses:

  elements:  𝟘-elim t  0            S t  0
             ℕ-elim z s t  0, 1(2), 2
             λ f  0(1)              f e  0, 1
             let a b  0, 1(2)       # body under value + unfolding-Prf binders
             (a , b)  0, 1          t.π₁ / t.π₂  0
             inj₁ t / inj₂ t  0     ⊎-elim l r t  0(1), 1(1), 2
             a b  0, 1(1)        a b  0, 1(1)
             a b  0, 1
             (l  r  T)  0, 1, 2ᵗ  a /r  0, 1(2)
             x[]  0.. (left to right)
             class a  0             quot-elim f q  0(1), 1
             T  0ᵗ
             𝒮.𝕤 ē (code)  0.. (the index spine)
             𝒮.𝕔 θ  0.. (the argument spine)
             𝒮.𝕤-elim  ē w  0..n-1 (the index spine), n (the eliminee)
             out t  0               corec 𝔽 a f x  0, 1(1), 2
             ν 𝔽 (code)  (none)
  types:     A  B  0, 1(1)         A  B  0, 1(1)
             A  B  0, 1            El e  0ᵉ               Prf e  0ᵉ
             A / r  0, 1ᵉ(2)        x[]  0..ᵉ
             𝒮.𝕤 ē  0..ᵉ            ν 𝔽  (none)
  (ᶜ marks universe codes; ᵉ marks descent into an element child, ᵗ into
   a type child. The quotient relation is an Ω-valued element child. A
   carried signature 𝒮 and eliminator problem  have NO child indices —
   they are OPAQUE to paths, approximation A3 (§9); only spines and
   eliminees are addressable.)

3. Proof spines: Σ; Γ ⊦ p ⇒ᵖ T

A step's proof license is an ELIMINATION SPINE over context variables and signature references (for the other license form, qpath, see §4). Inference implements Foundation's el-var, el-sig-var, el-pi-e, el-sigma-e₁/₂ and the ℕ/𝟙 introductions:

  Γ = T
  ------------------          Σ  (Δ  x  a : A)   Σ; Γ   ⇐ᵖ Δ
  Σ; Γ   ⇒ᵖ T              -----------------------------------
                              Σ; Γ  x[] ⇒ᵖ A[]
  Σ; Γ  f ⇒ᵖ T   nf(T) ⇓ A  B   Σ; Γ  e ⇐ᵖ A
  Σ; Γ  f e ⇒ᵖ B[id, e]
  Σ; Γ  t ⇒ᵖ T   nf(T) ⇓ A  B        (analogously .π₂ at B[id, t.π₁])
  Σ; Γ  t.π₁ ⇒ᵖ A
  Σ; Γ  () ⇒ᵖ 𝟙      Σ; Γ  Z ⇒ᵖ       Σ; Γ  t ⇐ᵖ   S t ⇒ᵖ 

Universe CODES infer at 𝕌 (components checked at their code types) — a generic lemma's 𝕌-parameter materialized at a concrete code is a legitimate spine argument — and so does a small signature's sort code, its index spine checked positionally against the reflected arity:

  Σ; Γ  c ⇒ᵖ 𝕌     (likewise 𝟘c, 𝟙c; Π/Σ//quot/ codes componentwise;
                      a ν code checks its polynomial's embedded pieces at 𝕌
                      in binder order, the context growing under El-binders)
  𝒮 small   𝒮(𝕜) = 𝔄 ending in U   Σ; Γ  ē ⇐ᵖ 𝔄⌋ᵗ (entrywise)
  Σ; Γ  𝒮.𝕤c ē ⇒ᵖ 𝕌

An ELIMINATOR chain (an unfolded recursive definition inside a lemma instantiation) is inferable too — el-qiit-elim with motives checked as types, methods at their method types, index spine and scrutinee at the sort — but a proof-fragment eliminator carries NO coherence certificates: each imposed method-image equation must hold by PURE β (nf-identical sides). An eliminator whose coherences need real replay lives at the item level, referenced through Σ (A4, §9).

Nothing else is inferable. Argument CHECKING (⇐ᵖ) accepts the introduction forms structurally and falls back to infer-and-compare:

  nf(T) ⇓ A / r   Σ; Γ  a ⇐ᵖ A         nf(T) ⇓ A  B
  -----------------------------         Σ; Γ  u ⇐ᵖ A   Σ; Γ  v ⇐ᵖ B[id, u]
  Σ; Γ  class a ⇐ᵖ T                   ---------------------------------
                                        Σ; Γ  (u , v) ⇐ᵖ T
  nf(T) ⇓ A  B   Σ; Γ  a ⇐ᵖ A         nf(T) ⇓ A  B   Σ; Γ  b ⇐ᵖ B
  -----------------------------         -----------------------------
  Σ; Γ  inj₁ a ⇐ᵖ T                    Σ; Γ  inj₂ b ⇐ᵖ T
  Σ; Γ  t ⇒ᵖ Tt   nf(Tt) ⇓ A  B
  Σ; Γ  A  l ⇐ᵖ T[]   Σ; Γ  B  r ⇐ᵖ T[]
  Σ; Γ  ⊎-elim l r t ⇐ᵖ T          # CONSTANT-MOTIVE (approximation
                                    # A1, see §9): the instance of
                                    # el-sum-e with motive T[↑]
  Σ; Γ  t ⇒ᵖ Tt   nf(Tt) ⇓ ν 𝔽
# el-nu-e: fully
  Σ; Γ  out t ⇒ᵖ El 𝔽(ν 𝔽)             # inference-driven
  nf(T) ⇓ ν 𝔽   (the term's carried 𝔽 nf-identical to nf(T)'s)
  Σ; Γ  a ⇐ᵖ 𝕌   Σ; Γ  El a  f ⇐ᵖ El 𝔽(a)[]   Σ; Γ  x ⇐ᵖ El a
  Σ; Γ  corec 𝔽 a f x ⇐ᵖ T               # el-nu-i
  nf(T) ⇓ 𝒮.𝕤 ē   𝒮(𝕔) = 𝔄 ending in El (𝕤 ī)
  Σ; Γ  θ ⇐ᵖ 𝔄⌋ᵗ (entrywise)   nf(ī[θ]) = nf(ē)
  Σ; Γ  𝒮.𝕔 θ ⇐ᵖ T                                    # the term's 𝒮 and
                                                       # nf(T)'s nf-identical
  nf(T) ⇓ Prf 𝟙                       nf(T) ⇓ Prf (l  r  A)   nf(l) = nf(r)
  ----------------                      -------------------------------------
  Σ; Γ   ⇐ᵖ T                         Σ; Γ   ⇐ᵖ T
  # el-squash-i with an evident witness, respectively el-eq-i after
  # the sides are seen ≜-equal. Equality is Ω-valued, so BOTH proofs
  # are ⋆ — Refl does not exist in the core. Squashed spellings
  # (∥Prf (l ≡ r ∈ A)∥) converge by code-squash-prf during nf.
  nf(T) ⇓ A  B   Σ; Γ  A  f ⇐ᵖ B     Σ; Γ  t ⇐ᵖ 𝟘
  ---------------------------------     ------------------------
  Σ; Γ  λ f ⇐ᵖ T                       Σ; Γ  𝟘-elim t ⇐ᵖ T
  Σ; Γ  t ⇐ᵖ    Σ; Γ  z ⇐ᵖ T   Σ; Γ    T[]  s ⇐ᵖ T[][]
  Σ; Γ  ℕ-elim z s t ⇐ᵖ T          # CONSTANT-MOTIVE (approximation
                                    # A1, see §9): the instance of
                                    # el-nat-e with motive T[↑]
  Σ; Γ  p ⇒ᵖ T′   nf(T′) = nf(T)
# fallback: infer, compare
  Σ; Γ  p ⇐ᵖ T

Signature substitutions e˲ ⇐ᵖ Δ are checked entrywise, entry i's telescope type instantiated by the preceding entries (sub-norm-ext).

let-expressions are NOT in the proof fragment (neither ⇒ᵖ nor ⇐ᵖ): a license containing one is rejected. Nothing is lost — a let is always a redex (§1), so the elaborator emits licenses let-free; a lemma whose body wants one is referenced through Σ, where the item level checks lets directly (§8).

4. What a step licenses

A step (onLhs, path, lic, sels, flip) licenses one equation, derived — never assumed — from its license. For a proof license p:

  Σ; Γ  p ⇒ᵖ T    nf(T) ⇓ Prf q    nf(q) ⇓ (l  r  A)
  (l′, r′, A′) = sels applied to (l, r, A)         (§5)
  step licenses  nf(l′)  nf(r′) : A′    (swapped when flip)

This is equality reflection (el-reflect) read certificate-side: the proof element is checked, its Prf-type's equality prop exposed, and the judgemental equation extracted. Equality is Ω-valued, so this is the ONE pathway — the old bare-≡ and squashed-reflection routes coincide (a squashed spelling normalizes to the prop by code-squash-prf). Any other proof type is rejected.

A step's license may instead be a PATH LICENSE, qpath 𝕔 θ, citing an imposed equation of the signature carried by the REWRITE POSITION'S TYPE: with the descent's expected type at the path end normalizing to 𝒮.𝕤′ ē″, the kernel demands 𝒮(𝕔) = 𝔄 ending in El (l ≡ r), checks θ entrywise against ⌊𝔄⌋ᵗ (⇐ᵖ, §3), and the step licenses

  nf(l[θ])  nf(r[θ]) : El 𝕦[θ]        (swapped when flip)

— Foundation's el-qiit-path read certificate-side, exactly as el-reflect is above. The signature is read off the site's type, which the descent has already computed positionally, so no signature is re-checked at step level; a path license at a position whose expected type is undetermined or not a sort application is rejected.

5. Selectors

Selectors pass from an equation between same-headed terms to a component equation. Each is licensed by a Foundation rule; both sides are normalized before the head test, and a selector whose head shapes do not match is rejected.

  suc      : S x  S y :               x  y : 
             # derivable congruence (pred via ℕ-elim)
  dom      : (a₀  b₀)  (a₁  b₁) : 𝕌   a₀  a₁ : 𝕌
             # code-pi-inj (also code-sigma-inj for pair codes)
  cod u    : (a₀  b₀)  (a₁  b₁) : 𝕌   b₀[id,u]  b₁[id,u] : 𝕌
             requires  Σ; Γ  u ⇐ᵖ El a₁
             # code-pi-inj second component, instantiated at u (el-sub-cong-fix)
  suml     : (a₀  b₀)  (a₁  b₁) : 𝕌   a₀  a₁ : 𝕌
  sumr     : (a₀  b₀)  (a₁  b₁) : 𝕌   b₀  b₁ : 𝕌
             # code-sum-inj; non-dependent, so neither component
             # crosses a binder and no instantiation element is needed
  qdom     : (a₀ / r₀)  (a₁ / r₁) : 𝕌   a₀  a₁ : 𝕌      # code-quot-inj
  qrel u v : (a₀ / r₀)  (a₁ / r₁) : 𝕌   r₀[id,u,v]  r₁[id,u,v] : Ω
             requires  Σ; Γ  u ⇐ᵖ El a₁   Σ; Γ  v ⇐ᵖ El a₁
             # the relation components live at Ω, not 𝕌
  qidx i   : 𝒮.𝕤 ē₀  𝒮.𝕤 ē₁ : 𝕌    ē₀ᵢ  ē₁ᵢ : Eᵢ
             requires the spines nf-EQUAL before i, so the entry type
             Eᵢ (entry i of 𝔎⌋ᵗ, instantiated by the shared prefix)
             is determined; the signatures and the sort position must
             be nf-identical      # QIIT code injectivity, indexwise

The injectivity rules are Foundation's (NovaFoundation.txt, "Type constructor injectivity"); the binder-crossing selectors take an instantiation element so the resulting equation stays in Γ. Those instantiation elements come from the (untrusted) certificate, so el-sub-cong-fix's premise is CHECKED (§3), not presumed — a binder equation only speaks about members of its domain, and an unchecked u would smuggle in an equation the premise never licensed.

NO selector passes from a constructor equation (𝒮.𝕔 θ₀ ≐ 𝒮.𝕔 θ₁ at a sort) to its components: point constructors are NOT injective — equation constructors may merge them (a quotient's cls is the canonical counterexample). And NO selector passes from an equation between equality props: equality is Ω-valued and inherits Ω's anti-structural discipline (code-prop-eq equates all true equations), so eq-injectivity is unsound — the old eqT/eqL/eqR selectors died with the ≡-type. Injectivity is a TYPE/CODE phenomenon only, exactly as in Foundation.

6. Typed path descent

Rewriting a subterm by an equation is CONGRUENCE, and Foundation's congruences demand the component equation AT THE COMPONENT'S TYPE. The descent therefore walks the path from the root, computing each child's expected type from its parent's, and verifies the licensed equation's type in situ at the rewrite point:

  at path end, b binders crossed, expected type E known:
    nf(E) = nf(A)[]     # the licensed type matches the position
    u = l[]             # the subterm is the licensed lhs, weakened
    u rewrites to r[]
  at path end with expected type UNDETERMINED: reject.

An expected type is undetermined at positions whose type only a motive or a non-normal spelling would determine; that is harmless at positions merely passed THROUGH (an intermediate hop of the path needs no type — congruence demands nothing there) and fatal only at the rewrite point itself. The child-type table (parent's expected type E; — means undetermined):

  𝟘-elim t        child 0 : 𝟘
  S t             child 0 : 
  ℕ-elim z s t    child 0 : E            # CONSTANT-MOTIVE (A1, §9)
                  child 1 : E[][]      # ditto
                  child 2 : 
  λ f             child 0 : B            when nf(E) ⇓ A  B
  let a b         (never reached: replay normalizes both sides before
                   any step (§7) and a let is always a redex (§1), so
                   no rewrite path meets one)
  f e             child 0 : —
                  child 1 : A            when f is an inferable spine
                                         # ⇒ᴺ, below
  (u , v)         child 0 : A            when nf(E) ⇓ A  B
                  child 1 : B[id, u]
  t.π₁ / t.π₂     child 0 : ⇒ᴺ(t)
  inj₁ a          child 0 : A            when nf(E) ⇓ A  B
  inj₂ b          child 0 : B            when nf(E) ⇓ A  B
  ⊎-elim l r t    children 0, 1 :# motive-dependent (like
                  child 2 : ⇒ᴺ(t)        # quot-elim's case function)
  a b          children : 𝕌
  a b, a b  children : 𝕌
  (l  r  T)     children 0,1 : T, child 2 : a type child
                  # the Ω-valued equality prop; congruence is
                  # code-eq-cong (admissible)
  a /r          children : 𝕌
  x[]           child i : Δᵢ[ prefix] # the telescope entry's type
  class a         child 0 : A            when nf(E) ⇓ A / r
  quot-elim f q   child 0 :, child 1 : ⇒ᴺ(q)
  out t           child 0 : ⇒ᴺ(t)
  corec 𝔽 a f x   child 0 : 𝕌, child 1 :# carrier-dependent (like
                  child 2 : El a              # quot-elim's case function)
  𝒮.𝕤 ē (code)    child i : entry i of 𝔎⌋ᵗ, instantiated by the
                            preceding children     (𝒮(𝕤) = 𝔎)
  𝒮.𝕔 θ           child i : entry i of 𝔄⌋ᵗ, likewise   (𝒮(𝕔) = 𝔄)
  𝒮.𝕤-elim  ē w  ē child i : entry i of 𝔎⌋ᵗ, likewise
                  eliminee : 𝒮.𝕤 ē

⇒ᴺ is neutral-spine inference: context variables, applications, first projections and signature references only — exactly the heads whose types are recoverable without annotations.

Steps inside TYPES (used by type certificates) walk the type formers (no rewrite may end at a type position — types are rewritten through their element children): the element entry points are the code under El (expected type 𝕌), the code under Prf and the relation of A / r (both expected type Ω), signature-entry arguments (the telescope type), and the index spine of a sort application 𝒮.𝕤 ē (the arity entry types, as above). The sides of an equation are reached THROUGH Prf's Ω-element child: Prf (l ≡ r ∈ T) descends 0ᵉ to the prop, then 0/1 to a side (expected type T).

Soundness note: the positional check is load-bearing. Equality is type-relative in this theory (a class equation at one quotient says nothing at another), and the two historical exploits (docs/NovaPipeline.txt, "Why this shape") both die on exactly this check or on proof-argument checking (§3).

7. Certificate replay

Element equations — Σ; Γ  𝒞  t₀  t₁ : T, with 𝒞 = (tyEx?, steps,

final):

  1. TYPE BRIDGE. If tyEx = (T′, 𝒞ᵀ): replay Σ; Γ  𝒞 T  T′ and
     continue at T′ in place of T. Justification: judgementally equal
     types have equal PERs (ty-el-cong / el-ty-coe collapse the
     membership), so the equation judgement is invariant under it.
     The bridge is the equation-level counterpart of the item level's
     head-exposure payload (§8): it lets steps land at positions whose
     structure only a lemma-normalized spelling of T exposes.
  2. Normalize both sides.
  3. Apply each step in order to its side (§4, §6), renormalizing the
     side after each step.
  4. Close by the final:
  beta         nf-equal sides:  l = r  syntactically after .
               # el-eq via ≜-chains
  prop         nf(T) ⇓ 𝟙 or 𝟘 or Prf p.  # el-one-prop / el-zero-prop /
               # el-prf-prop (proof irrelevance)
  witness 𝒞?   sides are class a  class b and nf(T) ⇓ A / r;
               then by the shape of nf(r[id, a, b]) (an Ω code):𝟙              — accepted (witness ())
                 ⇓ (wl  wr  W)    — replay 𝒞  wl  wr : W
               # el-quot-eq: the relation is Ω-valued, so its witness
               # shapes are prop codes — a squashed 𝟙 or an equality
               # prop (el-eq-i)
  ηΠ 𝒞         nf(T) ⇓ A  B; replay
               Σ; Γ  A  𝒞  l[]   r[]  : B     # el-pi-eta
  ηΣ 𝒞₁ 𝒞₂     nf(T) ⇓ A  B; replay
               𝒞₁  l.π₁  r.π₁ : A
               𝒞₂  l.π₂  r.π₂ : B[id, l.π₁]           # el-sigma-eta
  propext ...  nf(T) ⇓ Ω, sides prop codes p, q; check the two
               hypothetical implications as typings
               (Γ  Prf p  s  Prf q[] and symmetrically).  # code-prop-eq
Type equations — Σ; Γ  𝒞  T₀  T₁: no bridge is admissible (a

bridge on a type equation would be circular), steps apply through the type formers as in §6. The final is beta (nf-equal types), or one of the extensional-component congruences whose components cannot be flattened into steps: prfCong 𝒞 (both sides Prf-headed, 𝒞 proves the codes equal at Ω — ty-prf-cong), quotCong 𝒞 (both sides A / _ at a common domain, 𝒞 proves the relations equal at Ω — ty-quot-cong), piCong 𝒞 𝒞 / sigmaCong 𝒞 𝒞 (ty-pi-cong / ty-sigma-cong, componentwise: domain certificate, then codomain certificate under the RIGHT domain — needed exactly when a component's equality is itself extensional, e.g. a Prf codomain equal only by propext), sumCong 𝒞 𝒞 (ty-sum-cong, componentwise — both components over Γ, no binder to cross), nuCong 𝒞̄ (both sides ν types/codes ν 𝔽₀ / ν 𝔽₁: the polynomials must be identical one-hole syntax up to their embedded Nova pieces — former shapes and binder structure compared syntactically — with each aligned pair of embedded pieces replayed by its certificate, in the Nova-zone context accumulated from the binders passed. Foundation's structural ν congruence, stated there by meta-recursion; the same final closes a CODE equation ν 𝔽₀ ≐ ν 𝔽₁ : 𝕌 in element replay), and qiitCong 𝒞̄p 𝒞̄i (both sides sort applications 𝒮₀.𝕤 ē₀ / 𝒮₁.𝕤 ē₁ AT THE SAME SORT POSITION: 𝒮₀ and 𝒮₁ must be identical nameless ToS syntax up to their embedded Nova pieces — positions, entry shapes, binder structure compared syntactically, no α to quotient by — with each aligned pair of embedded pieces replayed by its certificate in 𝒞̄p, in the Nova-zone context accumulated from 𝒮₀'s preceding pieces; the index spines replayed pointwise by 𝒞̄i, entry i at 𝒮₀'s arity entry instantiated by ē₀'s prefix. This is Foundation's QIIT congruence, stated there by meta-recursion; the finals FQuotCong-style shortcut is what makes a signature-piece equation usable without descending into the carried 𝒮, which paths cannot do — A3, §9). The same final closes a CODE equation 𝒮₀.𝕤 ē₀ ≐ 𝒮₁.𝕤 ē₁ : 𝕌 in element replay, provided both signatures pass the smallness scan (§8). El-decoding inside nf gives ty-el-cong for free; a universe-code equation is transported through El by normalization, not by a rule.

8. The item level: skeletons

The kernel re-checks whole items bidirectionally. Its input is the core term plus a SKELETON — a tree positionally aligned with the term (same child indexing as §2), each node carrying zero or more payloads:

  payload ::=
      motive T sk       (PMotive)   eliminator motive + its skeleton
    | intro-ty T sk     (PIntroTy)  ascribed type of an intro form
                                      in inference position
    | switch 𝒞            (PSwitch)   inferred  expected, at a
                                      checked non-intro term
    | refl-eq 𝒞           (PReflEq)   the equation behind a  at an
                                      equality prop (el-eq-i)
    | wd 𝒞                (PWD)       quot-elim well-definedness
    | expose T 𝒞          (PExpose)   head exposure at a checked intro
    | squash-wit e sk   (PSquashWit) the witness behind a checked
                                       : Prf A (el-squash-i)
    | squash-elim e ske  (PSquashElim) el-squash-e-prf: scrutinee e
        b skb                       (inhabiting Prf A) and a body b
                                      proving (Prf q)[] under the raw
                                      squashee A
    | qcoh 𝒞₁𝒞ₖ        (PQCoh)    QIIT eliminator coherences, one
                                      certificate per equation entry
                                      of the carried signature

A payload is consumed when used (a node may carry several; order is immaterial). Missing children default to empty nodes.

Checking Σ; Γ ⊦ t ⇐ T ⟨sk⟩ :

  1. If sk carries switch 𝒞: infer Σ; Γ  t  T′ sk∖switch and
     replay 𝒞  T′  T. (The conversion is CERTIFIED, never decided
     by the kernel.)
  2. Otherwise, if sk carries expose T′ 𝒞: replay 𝒞  T  T′ and
     continue checking at T′. (T′'s well-formedness follows from T's
     by the certified equality; the intro checks against the exposed
     head and coercion — judgementally the identity — transports the
     result. This is PExpose; its equation-level twin is the bridge.)
  3. Then by the head of t:
     nf(T) ⇓ A  B    Σ; Γ  A  f  B sk.0
     Σ; Γ  λ f  T sk
     Σ; Γ  a  A sk.0
     Σ; Γ  A  Prf (  a[]  A[])  b  T[  ] sk.1
     Σ; Γ  let a b  T sk                            # el-let
     # T lives over Γ, so checking b at T[↑ ∘ ↑] is fully general,
     # not an approximation: under the unfolding hypothesis
     # (id, a, ⋆) ∘ (↑ ∘ ↑) ≐ id (el-reflect on ☐₀ plus el-prf-prop),
     # so any valid body type is ≐ T[↑ ∘ ↑]. The definiens is
     # INFERRED — an intro-form definiens carries intro-ty on sk.0,
     # the ascription route.
     nf(T) ⇓ A  B    Σ; Γ  u  A sk.0   Σ; Γ  v  B[id,u] sk.1
     Σ; Γ  (u , v)  T sk                            # el-sigma-i
     nf(T) ⇓ Prf (l  r  A)   sk carries refl-eq 𝒞   𝒞  l  r : A
     Σ; Γ    T sk                       # el-eq-i over replay
     # disambiguated from the squash rules below by nf(T)'s prop head
  el-nu-coind rides  too — COINDUCTION at an equality prop over a
  ν-type, the payload carrying the invariant, the endpoint proof and
  the one-step closure, each with its skeleton (all three are checked
  terms, not replay certificates — the premises are prop
  inhabitations, exactly the item-level checker's job):
     nf(T) ⇓ Prf p    nf(p) ⇓ (l  r  E)    nf(E) ⇓ ν 𝔽
     sk carries coind R skR,  skp,  skq
     Σ; Γ  ν 𝔽  (ν 𝔽)[]  R  Ω skR
     Σ; Γ    Prf R[id, l, r] skp
     Σ; Γ  ν 𝔽  (ν 𝔽)[]  Prf R    Prf (lift_𝔽(R) (out ) (out )) skq
     Σ; Γ    T sk                       # el-nu-coind
     # lift_𝔽 is the RELATOR (Foundation, coinductive section) —
     # KERNEL-computed from 𝔽 and R, like out's result type; the
     # closure's type is the rule's shape, never elaborator-supplied
     nf(T) ⇓ A  B    Σ; Γ  a  A sk.0
     Σ; Γ  inj₁ a  T sk                (inj₂ analogously at B)
     nf(T) ⇓ A / r    Σ; Γ  a  A sk.0
     Σ; Γ  class a  T sk
     nf(T) ⇓ ν 𝔽    (the term's carried 𝔽 nf-identical to nf(T)'s)
     Σ; Γ  a  𝕌 sk.0    Σ; Γ  El a  f  El 𝔽(a)[] sk.1
     Σ; Γ  x  El a sk.2
     Σ; Γ  corec 𝔽 a f x  T sk                      # el-nu-i
     nf(T) ⇓ 𝒮.𝕤 ē    𝒮(𝕔) = 𝔄 ending in El (𝕤 ī)
     Σ; Γ  θᵢ  (entry i of 𝔄⌋ᵗ)[θ prefix] sk.i (entrywise)
     nf(ī[θ]) = nf(ē)
     Σ; Γ  𝒮.𝕔 θ  T sk                          # el-qiit-intro
     # the term's carried 𝒮 and nf(T)'s must be nf-IDENTICAL;
     # equal-but-different spellings go through expose/switch, as
     # everywhere. The term's 𝒮 is NOT re-checked here — it is nf(T)'s
     # signature, already validated where T was.
     nf(T) ⇓ Prf A    sk carries squash-wit e ske   Σ; Γ  e  A ske
     Σ; Γ    T sk                                  # el-squash-i
     nf(T) ⇓ Prf q    sk carries squash-elim e ske b skb
     Σ; Γ  e  Prf A ske    Σ; Γ  A  b  (Prf q)[] skb
     Σ; Γ    T sk                            # el-squash-e-prf
     # disambiguated from el-squash-i above purely by which payload sk
     # carries; both erase to the same ⋆ (realizer irrelevance)
     Σ; Γ  t  𝟘 sk.0
     Σ; Γ  𝟘-elim t  T sk
     otherwise: infer Σ; Γ  t  T′ sk and demand nf(T′) = nf(T)
     — a mismatch without a switch certificate is rejection.

Inference Σ; Γ ⊦ t ⇒ T ⟨sk⟩ :

  If sk carries intro-ty T skT: check Σ; Γ  T type skT, then
  Σ; Γ  t  T sk∖intro-ty, and return T. (This is the ascription
  route: how introduction forms sit in inference position.)
  Otherwise by the head — variables and signature references (el-var,
  el-sig-var; the reference's substitution checked entrywise against its
  telescope, each entry against sk's children), (), Z, S t, spines:
     Σ; Γ  f  Tf sk.0   nf(Tf) ⇓ A  B   Σ; Γ  a  A sk.1
     Σ; Γ  f a  B[id, a]                              # el-pi-e
     (projections analogously: el-sigma-e₁/₂)
  let infers when its body does (definiens inferred, as in checking):
     Σ; Γ  a  A sk.0
     Σ; Γ  A  Prf (  a[]  A[])  b  B sk.1
     Σ; Γ  let a b  B[id, a, ]                       # el-let
  ℕ-elim demands its motive — the REAL rule, no approximation here:
     sk carries motive M skM       Σ; Γ    M type skM
     Σ; Γ  z  M[id, Z] sk.0
     Σ; Γ    M  s  M[(, S )  ] sk.1
     Σ; Γ  t   sk.2
     Σ; Γ  ℕ-elim z s t  M[id, t]                     # el-nat-e
  ⊎-elim demands its motive; the scrutinee's type is inferred (its
  head is neutral or an injection in the emitted fragment):
     sk carries motive M skM
     Σ; Γ  t  Tt sk.2    nf(Tt) ⇓ A  B
     Σ; Γ  A  B  M type skM
     Σ; Γ  A  l  M[, inj₁ ] sk.0
     Σ; Γ  B  r  M[, inj₂ ] sk.1
     Σ; Γ  ⊎-elim l r t  M[id, t]                     # el-sum-e
  quot-elim demands motive AND well-definedness:
     sk carries motive M skM and wd 𝒞
     Σ; Γ  q  Tq sk.1    nf(Tq) ⇓ A / r
     Σ; Γ  A/r  M type skM
     Σ; Γ  A  f  M[, class ] sk.0
     Σ; Γ  A  A[]  Prf r  𝒞  f[³, ]  f[³, ] : M[³, class ]
     Σ; Γ  quot-elim f q  M[id, q]                    # el-quot-e
  (the well-definedness hypothesis is Prf r — the DECODED relation)
  out is fully inference-driven — no motive, no skeleton payload
  beyond the scrutinee's:
     Σ; Γ  t  Tt sk.0    nf(Tt) ⇓ ν 𝔽
     Σ; Γ  out t  El 𝔽(ν 𝔽)                        # el-nu-e
  The QIIT eliminator carries its own motives and methods ( =  ; 
  in the TERM, Foundation's design), so no motive payload is needed —
  only the coherences, which are equations, arrive as certificates:
     Σ; Γ  𝒮 qsig sk𝒮    𝒮(𝕤) = 𝔎    sk carries qcoh 𝒞₁𝒞ₖ
     for each sort position 𝕤ⱼ of 𝒮 (𝒮(𝕤ⱼ) = 𝔎ⱼ):
         Σ; Γ·𝔎ⱼ⌋ᵗ  𝒮.𝕤ⱼ δ  C_𝕤ⱼ type skC.j             # mot
     for each point position 𝕔 of 𝒮 (𝒮(𝕔) = 𝔄; δ = 𝔄⌋ᵗ's variables):
         Σ; Γ  m_𝕔  𝔄𝒮.𝕔 δ skm.𝕔                     # dalg
     for each equation position 𝕔ⱼ of 𝒮
         (𝒮(𝕔ⱼ) = 𝔄ⱼ ending in El (l  r), sides at code 𝕤′ ī):
         Σ; Γ·𝔄ⱼᴰᵗ  𝒞ⱼ  l  r : C_𝕤′[ī[π], l[π]]  # eprob
     Σ; Γ  ēᵢ  (entry i of 𝔎⌋ᵗ)[ē prefix] sk.i (entrywise)
     Σ; Γ  w  𝒮.𝕤 ē sk.n
     Σ; Γ  𝒮.𝕤-elim  ē w  C_𝕤[ē, w]               # el-qiit-elim
  ·, ·⌋ᵗ, ··, ·ᴰᵗ, ·, θφ and π are Foundation's QIIT
  meta-operations, implemented as (trusted) kernel functions; the
  coherence replay in the -context is the QIIT generalization of
  quot-elim's wd certificate, one per equation entry.
  Universe codes infer at 𝕌 with components checked at 𝕌 (their
  binder children under El of the domain code), EXCEPT the quotient
  code's relation, checked at Ω: el-*-in-universe. Squash A infers
  at Ω with A checked as a type; an equality prop (l  r  A) infers
  at Ω with A checked as a type and the sides checked at A (code-eq). A sort application 𝒮.𝕤 ē infers at 𝕌
  when 𝒮 additionally passes the SMALLNESS scan — every external Π
  domain of every entry of the form El a or Prf p, a purely syntactic
  check (code-qiit) — with the spine checked as under formation below.
  Anything else in inference position (a bare intro form with no
  ascription payload) is rejected.

Formation Σ; Γ ⊦ T type ⟨sk⟩ : structural over the type formers (ty-pi/sigma/sum/el/prf/quot/nu/ty-prop/ty-sig-var), El's code checked at 𝕌, a ν type's polynomial checked structurally (poly-hole/-const/-prod/ -sum/-sigma/-pi: each embedded code at 𝕌, the context growing under the El-binders, skeleton children along in binder order), Prf's code and the quotient's relation checked at Ω, signature-type arguments checked against their telescope — all with skeleton children along. A sort application adds ty-qiit: Σ; Γ ⊦ 𝒮 qsig ⟨sk𝒮⟩, 𝒮(𝕤) = 𝔎 U-ended, and ē checked entrywise against ⌊𝔎⌋ᵗ (each entry's type instantiated by the preceding entries).

SIGNATURE CHECKING Σ; Γ ⊦ 𝒮 qsig ⟨sk⟩ is Foundation's qctx / qty / qtm system read as an algorithm — the ToS is syntax-directed by construction (qiit-terms are variables and application chains, so qiit-type checking and qiit-term inference need no annotations, and entry heads classify themselves). The only judgements with content are the embedded NOVA pieces — external Π domains checked as types over the Nova zone, external application arguments checked as elements — each with its own skeleton child: a former carrying 𝒮 aligns skeleton children with 𝒮's embedded Nova pieces in left-to-right order, before the former's own children. Signature checking burns fuel only through the Nova checking it triggers; the ToS layer itself is structural recursion.

Items. A definition (Δ ⊦ x ≔ t : T) is checked by: telescope entries as types left to right, T as a type under Δ, then Δ ⊦ t ⇐ T; a type definition likewise without the body. Acceptance EXTENDS the kernel's Σ with the entry; the kernel's Σ is the authoritative one, and an item is checked from it alone — the elaborator's opinion of any earlier item is never consulted. (The kernel accepts Foundation's general form — nonempty Δ, x[e˲] references with checked substitutions — but the elaborator only ever produces CLOSED items: surface parameters are Π-binders, so Δ = ε and every reference carries the empty substitution.)

9. Acknowledged approximations and their scope

The kernel is deliberately dumber than the theory; where it accepts by an approximation, the approximation is an INSTANCE of a Foundation rule (so soundness is unaffected) that may reject spellings the theory would accept (incompleteness only). There are two confined to EQUATION REPLAY (A1, A2), and three added by the QIIT extension (A3–A5):

  A1  CONSTANT MOTIVE. In proof-argument checking (§3) an ℕ-elim
      argument is checked by the el-nat-e instance whose motive is
      T[], and a ⊎-elim argument by the el-sum-e instance likewise;
      in the typed descent (§6) the z/s positions of an ℕ-elim
      are typed by the same reading (a ⊎-elim's case positions stay
      undetermined there). Dependent-motive recursors
      cannot be rewritten at those positions and their proofs cannot
      appear as step arguments; the ITEM level (§8) carries real
      motives and has no such limit.
  A2  NEUTRAL SPINES ONLY (⇒ᴺ). Argument and scrutinee positions in
      the descent are typed only when the applied head is a variable,
      application chain, first projection or signature reference. A
      rewrite point under, e.g., a bare ℕ-elim head is undetermined —
      the emitter's remedy is the type bridge (§7), which re-types
      the whole equation at a spelling where the position IS
      determined.
  A3  OPAQUE CARRIERS. Rewrite paths do not descend into a carried
      signature 𝒮 or eliminator problem  — their embedded Nova
      pieces are not addressable rewrite points (§2). The remedy for
      a signature-piece equation is the qiitCong final (§7), which
      replays all aligned pieces at once; failing that, a lemma
      respelling the whole former, via bridge or expose.
  A4  β-ONLY COHERENCES IN SPINES. Proof-spine checking (§3) accepts
      𝒮.𝕔 θ introductions, universe and sort codes, and eliminator
      chains — but no certificates travel inside a proof license, so
      a spine eliminator's coherences are verified by pure β alone.
      An eliminator whose coherences need real replay is referenced
      through Σ, where the item level carries the full apparatus
      (coherences as PQCoh certificates, §8).
  A5  NO η CERTIFICATE FOR QIITs. el-qiit-eta (like el-nat-eta,
      el-sum-eta and el-quot-eta before it) has no replay final; for
      ν the gap is CLOSED, by el-nu-coind as a -payload (§8) — the
      admissible relational form, not el-nu-eta itself (whose
      candidate h would be a carried higher-order payload; the
      relational form subsumes it via graph invariants);
      uniqueness arguments live in the elaborator as lemmas, not in
      kernel certificates (an el-sum-eta instance is proven as an
      ordinary ⊎-elim lemma at an equality motive, β closing both
      cases). The Π/Σ η finals are unaffected.
  A6  FIRST-ORDER SIGNATURE FRAGMENT. The signature checker (§8)
      covers the fragment the elaborator emits: no equation-code
      binders, no external λ (infinitary recursive arguments). Sort
      entries MAY carry inductive index binders (induction-induction
      — Con/Ty-style signatures check; the entry walk rebases each
      index code from its declaration site into the walk state of
      its use site). Foundation covers the rest; the restriction is
      checking incompleteness only.

Two structural caveats restated from docs/NovaPipeline.txt: an annotation (motive, ascription, exposure target) is a REPRESENTATIVE, never a canonical type — no consumer compares annotations syntactically, only up to certified conversion; and the kernel invariant is one-directional — kernel accepts the annotated tree ⟹ the erasure is Foundation-derivable at the stated type. Rejection claims nothing.

Nova Elaboration

Rendered from docs/NovaElaboration.txt — the plain text remains the source of truth.

NovaElaboration.txt — surface syntax and elaboration

Preface

This file specifies a syntax-driven ELABORATOR for Nova: a bidirectional algorithm that translates a surface-syntax file — a sequence of signature entries — into the core syntax of docs/NovaFoundation.txt, collecting along the way the set of equational side conditions ("obligations") that must hold for the translation to be justified.

Relationship to the rest of the codebase:

  • docs/NovaFoundation.txt is the sole source of truth and correctness. Every elaboration rule below is annotated with (or directly mirrors) the Foundation rule(s) that justify it, and the soundness contract (see Metatheory) is stated against Foundation derivability. Where this file and Foundation disagree, Foundation wins.
  • Elaboration is the sole way judgements are established. (It replaced the earlier derivation machinery — .rules/.target sessions, the fact table, `apply`/`query` — which has been removed; what remains shared with that era is only the core
    syntax (Ty/Elem/Sub/Ctx/Sig) and the -computation relation.)
  • This version is HOLE-FREE: no metavariables, no unification. Every binder is named, every motive is written, every ascription that the bidirectional discipline needs is supplied by the user. Holes are a planned extension (see Future work) and nothing here is allowed to obstruct them.

The elaboration model in one paragraph:

  The elaborator processes one signature entry at a time, in file order.
  Where checking meets an equation it cannot discharge algorithmically
  (by computation, by congruence, or from the accepted lemma store), it
  does not fail: it ASSUMES the equation, records it as an obligation,
  and carries on. At the end of the run all remaining obligations are
  reported. The user (human or AI) discharges an obligation by
  PREPENDING a lemma — an ordinary definition whose type is the
  corresponding equality type — before the entry that surfaced it, and
  re-running. A file is ACCEPTED exactly when a run ends with zero
  obligations; nothing survives between runs, and no assumption ever
  participates in an accepting run. Equality proofs in this theory are
  computationally irrelevant, so an assumed equation never changes what
  any term elaborates to — only whether the file is accepted.

Surface syntax

Token conventions: local identifiers are alphanumeric (a leading letter or `_`, then letters/digits/`_`/`'`); `_` is the wildcard binder, never resolvable; T{n}/t{n} names the type/term grammar at precedence level n, and T{>=n} any level at or above it. The term/type grammar below is self-contained.

A file is a sequence of items. `def` introduces a term definition, `type` a type definition — the two signature-entry forms of Foundation's Σ; `data` is an ITEM MACRO that expands into a batch of them (QIIT section below). Every item is declared in the EMPTY context: parameters are ordinary Π-binders in the item's type (the iterated binder syntax below keeps that pleasant), and a reference to an item is a bare name. Foundation's Σ entries keep their general declaration contexts; the elaborator simply only produces closed ones — so the normal-substitution syntax x[t˲] has no surface form.

file  ::= import* (item | fixity)*
imp   ::= import M | import M (n (, n)*)
item  ::= def  n : T{≥0}  t{≥0}
        | type x  T{≥0}
        | data ([x : T{≥0}])* ( n : Q (; n : Q)* )
                                              # a QIIT signature literal —
                                              #   an ITEM MACRO over an
                                              #   ambient PARAMETER
                                              #   telescope, see the QIIT
                                              #   section below
fixity ::= infixl d op | infixr d op          # d a digit 0-9

Q is the ToS type grammar of a data entry — Foundation's qiit-types in surface clothes (→ inside a data literal is Foundation's ⇛; binder groups iterate as everywhere, and a NON-DEPENDENT domain may stand bare, binding an anonymous binder — cls : El a → El Q):

  Q ::= U | El q | ((x : D))+  Q | D  Q

with q a ToS code (a sort name applied to arguments, or l ≡ r between sort elements) and D a domain CLASSIFIED BY NAME RESOLUTION: `El q` whose head resolves to a sort of the SAME literal (or an ≡ between such elements) is an INDUCTIVE domain; any other surface type is EXTERNAL, elaborated as an ordinary type over the external binders in scope. No new expression syntax exists outside the literal: everything a data item provides reaches the file as ordinary defs (see the QIIT section).

M is a dotted module name (Data.Nat); see Modules below. n is an identifier x or an operator token op — OPERATORS ARE NAMES: `def + : ℕ → ℕ → ℕ ≔ plus` defines the Σ-name "+", a fixity line gives it precedence/associativity for infix use, and `a + b` is nothing but application of that name. There is no notation-to-name mapping and hence no resugaring gap: the obligation printer prints the name, and the name is the operator (binary applications of operator-shaped names lay out infix, fully parenthesized). Operator tokens are maximal runs of the operator alphabet + - * < > = & | ! ? % ^ ~ @ # ⊕ ⊗ ⊙ ⊞ ⊟ ∙ ∘ · ≤ ≥ ∸ ⧺ ⊥ ⊤ ∧ ∨ ⊃ ¬ ↔ (the reserved theory tokens → ⨯ ≡ ∈ ≔ / . , : are excluded, and the lexer eats "--" as a comment, so no operator contains it). The mention form (op) — e.g. (+) — is the operator as an ordinary reference, usable anywhere an atom is; local binders are never operator-shaped. A FIXITY-FREE operator token is itself an ordinary name atom — that is how nullary and prefix operator names work (⊥, ⊤, ¬ p in prop.nova); an operator WITH a fixity in scope is infix-only outside the mention form, so application juxtaposition never captures it. A fixity declaration takes effect for the rest of the file and is exported with the name: opening an operator (`import nat (+)`) imports its fixity alongside. Infix use of an operator with no fixity in scope is a parse error.

Types. Elaboration needs no rule keywords and no context prefixes — the context is always implicit in where a subterm sits.

T{4} ::= 𝟘 | 𝟙 |  | 𝕌 | Ω | x | (T{≥0})
T{2} ::= El t{≥4} | Prf t{≥4} | ν F{≥2}
T{1} ::= ((x:T{≥0}))+  T{≥0} | ((x:T{≥0}))+  T{≥0}
       | T{≥1½} / (x y. t{≥1})
T{1½} ::= T{≥2}  T{≥1½}

⊎ is NON-DEPENDENT (no binder form), right-associative, and binds TIGHTER than → ⨯ / (Agda's convention: A ⊎ B → C is (A ⊎ B) → C); the T{1} infixes take their left operand at T{≥1½}

T{0} ::= t{≥2}  t{≥2}  T{≥1}

the quotient relation is an Ω-valued ELEMENT (t), not a type. EQUALITY IS Ω-VALUED (NovaFoundation.txt, Ω block): the surface ≡-TYPE above is SUGAR — it elaborates to Prf (l ≡ r ∈ T) (e-ty-eq). The proof of an equality is ⋆, like every proposition's; there is no Refl, in the core or on the surface.

Binder groups ITERATE: (x:T) (y:U) → B parses as (x:T) → (y:U) → B (each group scopes over the ones after it; likewise for ⨯), and the codomain is full T{≥0}, so a lemma statement needs no parentheses:

    (n : ) (m : )  plus n m  plus m n  

Elements. Two departures from the derivation surface syntax: 1. Ascription `(t : T)` is first-class. It is the user's lever for putting a term into inference mode (see e-ann below) — needed

     exactly where the bidirectional discipline says so (a λ or pair
     applied/projected directly, an eliminated term whose type the
     elaborator cannot see).

2. ℕ-elim and quot-elim take their motives inline, motive-first. Motives are not inferable without higher-order unification, so they are mandatory syntax here. 3. corec takes its state CARRIER inline, as a binder annotation — corec (x : a. f) u — the carrier code is not recoverable from

     the expected ν-type, so it is mandatory syntax, like a motive.
t{5} ::= x | () | Z |  | T{≥0} | 𝟘 | 𝟙 |  | (t{≥0}) | (t{≥0} : T{≥0})
t{3} ::= t{≥3} t{≥4} | t{≥3} .π₁ | t{≥3} .π₂                 (left-assoc)
t{2} ::= λx. t{≥1½}
       | let x  t{≥0} in t{≥1½}                              # let-expression
       | let x : T{≥0}  t{≥0} in t{≥1½}                      #   (annotated
                                                              #   definiens) —
                                                              #   see e-let
       | 𝟘-elim t{≥4}
       | S t{≥4}
       | ℕ-elim (n. T{≥0}) t{≥4} (n ih. t{≥4}) t{≥4}          # motive, z, s, scrutinee
       | inj₁ t{≥4}
       | inj₂ t{≥4}
       | ⊎-elim (z. T{≥0}) (a. t{≥0}) (b. t{≥0}) t{≥4}        # motive, left case,
                                                              #   right case, scrutinee
       | class t{≥4}
       | quot-elim (z. T{≥0}) (a. t{≥0}) t{≥4}                # motive, case fn, scrutinee
       | ν F{≥2}                                              # the ν CODE (⇒ 𝕌)
       | out t{≥4}
       | corec (x : t{≥0}. t{≥0}) t{≥4}                       # carrier code + coalgebra
                                                              #   body (one binder), seed
       | coind (x y. t{≥0}) t{≥4} (x y h. t{≥0})              # invariant, endpoint proof,
                                                              #   one-step closure — see
                                                              #   e-coind
       | squash-elim t{≥4} (x. t{≥0})               # el-squash-e-prf: eliminate a
                                                     #   proof of a squash into a
                                                     #   further proposition
       |  t{≥4}                          # el-squash-i, explicit witness (any A)
t{1} ::= ((x:t{≥0}))+  t{≥1} | ((x:t{≥0}))+  t{≥1}
       | t{≥1¼} / (x y. t{≥1})
                                                              # universe codes
       | t{≥1¼}  t{≥1¼}  T{≥2}     # the equality PROP (an Ω-element);
                                     #   ∈ embeds a TYPE, like ∥-∥
t{1¼} ::= t{≥1½}  t{≥1¼}            # the ⊎ code — tighter than the
                                     #   t{1} infixes, like its type

∥T∥ (squash), ≡ (equality props) and ⋆ (the canonical proof) are the Ω introductions; a squashed type is an Ω-valued element. Bare ⋆ (t{5}) auto-synthesizes only for evident propositions — a squashed 𝟙, or an equality prop whose sides are ≐; `⋆ e` (t{2}) checks e against the squashee directly, for any shape — el-squash-i was always general (NovaFoundation.txt), only the auto-synthesis was restricted. squash-elim is el-squash-e-prf's surface form: it has no automatic counterpart since there is nothing to search for.

t{1½} ::= t{≥2} (op t{≥2})*     # declared infix operators, by fixity
t{0} ::= t{≥1} , t{≥0}                                        (right-assoc)

Polynomials (the one-hole codes of Foundation's coinductive section). The hole is 𝕏; external pieces are element-level CODES. ⊎ binds tighter than ⨯, as everywhere; the binder forms mirror the type-level binder groups (a left-hand (x:t) BINDS x in the body):

F{2} ::= 𝕏 | K t{≥4} | (F{≥0})
F{1½} ::= F{≥2}  F{≥1½}
F{1} ::= F{≥1½}  F{≥1} | ((x:t{≥0}))+  F{≥1} | ((x:t{≥0}))+  F{≥1}
F{0} ::= F{≥1}

Name-dropping sugar: `A → B` for `(_:A) → B`, `A / R` for `A / (_ _. R)`, `_` in any binder.

Name resolution (front end, before elaboration)

Names are a parsing concern only. Parsing + scope resolution translate the named text into an INDEXED SURFACE AST: the same grammar with every variable occurrence replaced by its de Bruijn index ☐ᵢ (innermost binder wins; locals shadow the signature; a name bound by no binder is a signature reference, and whether it exists in Σ is the elaborator's question) and binder names carried along only as display metadata. Elaboration operates exclusively on this indexed surface syntax; its rules below never consult a name, Γ is a plain core context, and all binder bookkeeping is ordinary index arithmetic. Names reappear in exactly one place: the report printer, which uses the retained metadata to render obligations readably.

The indexed surface AST is still surface, not core: it contains ascription nodes `(t : T)` and inline eliminator motives, which core syntax lacks. Elaboration is what erases those — checking ascriptions away and moving motives out of the term — so the distance between surface and core is annotations, never names.

Elaboration state

A run threads three monotonically growing stores. Rules below read and extend them implicitly rather than threading them through every premise.

Σ — the signature: core entries produced by already-elaborated items,

      exactly Foundation's Σ. (Entries elaborated under assumptions are
      in Σ for the remainder of the run; acceptance semantics below.)

E — the equation store, feeding algorithmic discharge. Three sources:

      * ACCEPTED LEMMAS: for every entry (ε  x  p : A)  Σ whose type
        A, after peeling leading Π's into the context, is
        Prf (l  r  T), the store contains the reflected equation
            A₁  ...  Aₖl  r : T
        (the peeled binders become context entries — all of them
        PARAMETRIC, so the lemma applies in any context by first-order
        instantiation). Justified by Foundation (el-reflect) applied to
        x[·] ₖ₋₁ ... . This is how user-proved equalities enter
        discharge: prove at the element level once, use judgementally
        everywhere.
      * HYPOTHESES: for every entry of the AMBIENT context whose type,
        after peeling leading Π's, is a Prf of an equality prop, the
        reflected equation likewise — with the ambient context rigid
        and only the peeled binders parametric. Justified the same way,
        with  as the reflected element. This is what makes an
        induction hypothesis (an equality-hypothesis ℕ-elim binder)
        usable silently, and it is why induction proofs elaborate with
        `` in every case.
        An equality-typed lemma or hypothesis PARAMETER that the equation's
        sides do not determine is a SIDE CONDITION, discharged by a
        nested (budgeted) equality check — hypothesis-conditional
        lemmas, e.g. well-definedness facts assuming relatedness.
        Both sources are closed under COMPONENT DECOMPOSITION: an
        equation between same-headed universe codes also contributes
        its component equations as candidates (domain; codomain under
        the domain, as an extra parametric binder), licensed by
        Foundation's code-injectivity rules — so a hypothesis
        h : Prf ((a  𝟙)  (b  𝟙)  𝕌) silently yields a  b : 𝕌. The
        S-component closure is included too (derivable via a
        predecessor, no rule needed). class is NOT decomposed:
        quotients are not injective.
      * ASSUMED CONSTRAINTS: every equation constraint of Σ (each one
        an equation assumed by ↓ below), so that the run continues
        coherently and the same mismatch never surfaces twice.

There is NO separate obligation store: an OBLIGATION is a constraint entry of Σ (Foundation: sig-eq/sig-ty-eq — the signature is OPEN during a run), appended in surfacing order. Alongside each entry the elaborator keeps DISPLAY METADATA — outside the theory, consumed only by the report printer: the item and source position that surfaced it, the binder-name environment of its context, and — when its two sides were themselves elaborated under earlier assumptions — a note naming the composite equation it was decomposed from. The report enumerates Σ's constraint entries in order, and a run is ACCEPTED exactly when its final Σ is DEFINITIONAL (Foundation: no constraints — and, once surface holes land, no declarations).

The distinction that keeps this sound: entries of E may be USED freely by conversion during the run, but a constraint is only ever CLOSED — absent from the next run's Σ — because a lemma accepted earlier on that LATER RUN discharges the site that would have minted it. Within a run, an equation that matches an already-assumed constraint is deduplicated against it, not discharged by it. Assumptions therefore can never launder themselves into proofs; the wall between "assumed" and "proven" is crossed only by the prepend-and-rerun cycle.

Judgement forms

Γ below is a plain core context; T and t range over INDEXED surface syntax (see Name resolution above). Named binders appearing in the rules

(`Γ  x:A ⊢ ...`) are readability only — x is not consulted.

Σ; E; Γ ⊢ T ⇝ A type # surface type T elaborates to core A Σ; E; Γ ⊢ t ⇐ A ⇝ a # checking: core type A given Σ; E; Γ ⊢ t ⇒ A ⇝ a # inference: core type A produced Σ; E; Γ ⊢ A ≐ B type ↓ # type conversion: discharge or assume Σ; E; Γ ⊢ a ≐ b : A ↓ # element conversion: discharge or assume

The ↓ judgements ALWAYS SUCCEED — that is the "assume and carry on" principle. They either discharge the equation algorithmically or append it to O (and E). Elaboration proper (⇝ / ⇐ / ⇒) can fail, but only on STRUCTURAL grounds — an unbound name, a λ in inference position, an application whose function type never takes the shape of a Π — never on equational grounds. The dividing line: an equation with both sides in hand becomes an obligation; a missing STRUCTURE (which Π? which motive?) cannot be phrased as an equation with a known right-hand side and is instead an error asking the user for an ascription or annotation.

whnf

whnf(–) is weak-head normalization by Foundation's  rules:

el-pi-beta, el-let-beta (a let is always a redex — no whnf ever returns one), el-sigma-beta₁, el-sigma-beta₂, el-nat-beta-z, el-nat-beta-s, el-sum-beta₁, el-sum-beta₂, el-quot-beta, el-nu-beta (out at a corec head — map_𝔽 and hᵉˡ expanding by

Foundation's -clauses), el-qiit-beta (the eliminator at a

saturated constructor of the nf-identical signature), el-sig-beta/ty-sig-beta (signature unfolding — for DEFINITION entries; a declaration reference is stuck by design, el-sig-decl/ty-sig-decl, and constraint entries are nameless and never referenced), and the El-decoding family (ty-el-zero, ty-el-one, ty-el-nat, ty-el-pi, ty-el-sigma, ty-el-sum, ty-el-nu, ty-el-eq, ty-el-quot — the last

decoding El (A / r)  El A / r, the Ω-valued relation passing through
undecoded — and ty-el-qiit, El (𝒮.𝕤 ē)  𝒮.𝕤 ē; Prf A has no

decoding rule). Per Foundation's preface, normalization of well-formed terms may diverge under inconsistent hypotheses; whnf is therefore fuel-bounded, and fuel exhaustion is treated as "neutral" — a conservative outcome that can only produce a superfluous obligation, never an unsound acceptance.

Type elaboration

Γ ⊢ 𝟘 ⇝ 𝟘 type Γ ⊢ 𝟙 ⇝ 𝟙 type Γ ⊢ ℕ ⇝ ℕ type Γ ⊢ 𝕌 ⇝ 𝕌 type Γ ⊢ Ω ⇝ Ω type # (𝟘),(𝟙),(ℕ),(𝕌),(Ω)

(ε  x  T type)  Σ
e-ty-sig# (x[e˲] type)
Γxx[·] type

Every entry the elaborator produces is closed, so the core reference always carries the empty substitution. (Foundation's general x[e˲] stays available to the kernel; it just never appears in elaborator output.)

ΓTA type
Γ  x:AUB type
e-ty-pi# (A → B)
Γ ⊢ (x:T)  UA  B type
ΓTA type
Γ  x:AUB type
e-ty-sigma# (A ⨯ B)
Γ ⊢ (x:T)  UA  B type
ΓTA type
ΓUB type
e-ty-sum# (A ⊎ B)
ΓT  UA  B type
ΓTA type
Γ  x:A  y:A[]r  Ω            # the relation is Ω-valued
e-ty-quot# (A / r)
ΓT / (x y. r) ⇝ A /  type
ΓF𝔽 poly
e-ty-nu# (ν 𝔽)
Γν Fν 𝔽 type

Polynomial elaboration Γ ⊢ F ⇝ 𝔽 poly — structural, each external piece a code, the context growing under the binder forms (Foundation's poly-* rules):

Γ ⊢ 𝕏 ⇝ 𝕏 poly (e-poly-hole) Γ ⊢ t ⇐ 𝕌 ⇝ a ⟹ Γ ⊢ K t ⇝ K a poly (e-poly-const) componentwise at F ⨯ G and F ⊎ G (e-poly-prod, e-poly-sum)

Γt  𝕌a   Γ  x:El aF𝔽 polyΓ ⊢ (x:t)  FEl a  𝔽 poly             (e-poly-sigma)
   ⟹   Γ ⊢ (x:t)  FEl a  𝔽 poly             (e-poly-pi)
Γp  Ω
e-ty-prf# (Prf p)
ΓPrf pPrf  type
ΓTA type
Γt₀  Aa₀
Γt₁  Aa₁
e-ty-eq# Prf (a ≡ b ∈ A)
Γt₀  t₁  TPrf (a₀  a₁  A) type
# the surface ≡-TYPE is sugar: equality is Ω-valued, so the type it
# denotes is the Prf of the equality prop (ty-prf over code-eq)
Γt  𝕌a
e-ty-el# (El A)
ΓEl tEl a type

Element elaboration: inference

 in bounds for Γ
e-var# Γ‖ᵢ
Γ  Γ
(ε  x  a : A)  Σ
e-sig# (x[e˲])
Γx  Ax[·]
------------------ (e-unit)      ---------------- (e-zeroN)

Γ ⊢ () ⇒ 𝟙 ⇝ () Γ ⊢ Z ⇒ ℕ ⇝ Z

Γt  
ΓS t  S 
Γf  C        whnf(C) = A  B
Γe  A ⇝ ê
e-app# ((f : A → B) e)
Γf e  B[id, ê] ê
# whnf(C) of any other shape is a structural error: "cannot apply a
# term of non-Π type — ascribe the function". No obligation is emitted;
# there is no equation to state.
Γt  C        whnf(C) = A  B
e-proj1# ((t : A ⨯ B) .π₁)
Γt .π₁  A .π₁
Γt  C        whnf(C) = A  B
e-proj2# ((t : A ⨯ B) .π₂)
Γt .π₂  B[id,  .π₁] .π₂
ΓTA type
Γt  A
Γ ⊢ (t : T)  A
Γe  A ⇝ ê
Γ  x:A  h:Prf (  ê[]  A[]) ⊢ b  B
e-let# (let a b)
Γlet x  e in b  B[id, ê, ]let ê 
# The DEFINIENS is inferred — a checking-only definiens (λ, pair, ...)
# takes the annotated form, which is parse-level sugar for ascription:
#     let x : T ≔ e in b   ≜   let x ≔ (e : T) in b
# The BODY is elaborated under x AND the unfolding hypothesis h. h's
# type is a Prf of an equality prop, so E's HYPOTHESIS source reflects
# ☐₁ ≐ ê[↑ ∘ ↑] into discharge automatically: the definition is
# TRANSPARENT inside the body with no new mechanism — Foundation's
# el-let, the definition-carrying-context reading. h never appears in
# b (nothing binds it on the surface); it exists for discharge and for
# the kernel's context, and the report printer renders it silently.
Γ  n:TA type
Γz  A[id, Z] ⇝ ẑ
Γ  n:  ih:As  A[  , S ]ŝ
Γt  
Γℕ-elim (n. T) z (n ih. s) t  A[id, ]ℕ-elimŝ 
                                        # (ℕ-elim z s t motive A)
Γt  C        whnf(C) = A  B
Γ  z:(A  B) ⊢ TM type
Γ  a:Al  M[, inj₁ ]
Γ  b:Br  M[, inj₂ ]
Γ⊎-elim (z. T) (a. l) (b. r) t  M[id, ]⊎-elim   
                                # (⊎-elim l r t motive M)
# no side condition beyond the branches themselves — β covers both
# injections, so unlike quot-elim there is no well-definedness premise
Γt  C        whnf(C) = ν 𝔽
Γout t  El 𝔽(ν 𝔽) ⇝ out            # (out t)
# fully inference-driven, like the projections: no motive, the
# polynomial read off the scrutinee's whnf type
Γq  C        whnf(C) = A / r
Γ  z:(A / r) ⊢ TB type
Γ  a:Af  B[, class ]
Γ  a:A  b:A[]  h:Prf r[    , ]  [    , ]
                        : B[    , class ]
Γquot-elim (z. T) (a. f) q  B[id, ]quot-elim  
                              # (quote-elim (A / r) f f⁼ q motive B)
# the well-definedness hypothesis is Prf r (the DECODED relation), so a
# squashed-equality hypothesis is available to discharge f⁼
# The well-definedness premise f⁼ is a ↓-judgement: if the case function
# respects R by computation or by an accepted lemma, elaboration is
# silent; otherwise "f respects R" is surfaced as an ordinary equational
# obligation. This is the intended shape for all content-bearing side
# conditions: they become obligations, not errors and not annotations.

Universe codes infer at 𝕌, mirroring their formation rules: Γ ⊢ 𝟘 ⇒ 𝕌 ⇝ 𝟘 (likewise 𝟙, ℕ) # (𝟘 : 𝕌) etc.

Γt  𝕌a        Γ  x:El au  𝕌b
e-code-pi# (A → B : 𝕌)
Γ ⊢ (x:t)  u  𝕌a  b
   (e-code-sigma analogous for )                             # (A ⨯ B : 𝕌)
Γt  𝕌a        Γu  𝕌b
e-code-sum# (A ⊎ B : 𝕌)
Γt  u  𝕌a  b
   # non-dependent: u is checked over Γ, not Γ ▷ El a
Γt  𝕌a        Γ  x:El a  y:(El a)[]r  Ω
Γt / (x y. r)  𝕌a /                                   # (A / r : 𝕌)
   # the relation is checked at Ω, not 𝕌
ΓF𝔽 poly
e-code-nu# (ν 𝔽 : 𝕌)
Γν F  𝕌ν 𝔽
ΓTA type        Γt₀  Aa₀        Γt₁  Aa₁
Γt₀  t₁  T  Ω ⇝ (a₀  a₁  A)                # (a₀ ≡ a₁ ∈ A : Ω)
# code-eq: the equality prop, A an arbitrary type (large included) —
# there is no 𝕌-code for equality
ΓTA type
e-squash# (∥A∥ : Ω)
ΓT  ΩA
# ∥-∥ is the only Ω introduction that infers; ⋆ is checking-only
# (e-star below), since its proposition is not inferable from ⋆ alone.

Element elaboration: checking

Introduction forms check against the whnf of the expected type. A rigid shape mismatch here (λ against a non-Π, class against a non-quotient, ...) is a structural error, not an obligation: if the expected type is secretly Π only up to an unproven equation, the user states that intent with an ascription, which moves the equation to e-switch where it belongs.

whnf(C) = A  B        Γ  x:At  B
e-lam# (λ f)
Γλx. t  Cλ 
whnf(C) = A  B        Γu  A ⇝ û        Γv  B[id, û]
Γu , v  C ⇝ û ,                                           # (a, b)
whnf(C) = A  B        Γa  A ⇝ â
e-inj₁# (inj₁ a)
Γinj₁ a  Cinj₁ â
   (e-inj₂ analogous at B)                                    # (inj₂ b)
whnf(C) = A / r        Γa  A ⇝ â
e-class# (class a)
Γclass a  Cclass â
whnf(C) = ν 𝔽        Γt  𝕌a
Γ  x:El af  El 𝔽(a)[]        Γu  El a ⇝ û
Γcorec (x : t. f) u  Ccorec 𝔽 a  û    # (corec 𝔽 a f x)
# checking-only, like λ and class: the polynomial comes from the
# expected type. In ⇒ position, ascribe.
whnf(C) = Prf p    whnf(p) = (l  r  E)    whnf(E) = ν 𝔽
Γ  x:ν 𝔽  y:(ν 𝔽)[]R  Ω
Γp  Prf [id, l, r]
Γ  x:ν 𝔽  y:(ν 𝔽)[]  h:Prf q  Prf (lift_𝔽() (out ) (out )) ⇝ 
Γ ⊢ coind (x y. R) p (x y h. q)  C
# el-nu-coind's surface form: the core term is ⋆; the invariant,
# endpoint proof and closure ship in the skeleton payload
# (docs/NovaKernel.txt §8). The closure's expected type is the
# RELATOR at the generic observations — its sub-goals surface as
# ordinary obligations, dischargeable by the usual loop. Two engine
# facts make the closure proofs ergonomic: (1) a GROUND hypothesis
# whose type is a (possibly dependent) Σ-tree of Prf-equalities
# licenses one rewrite candidate per component, the proof element
# being the projection chain (el-reflect takes any Prf-typed term) —
# the shape squash-elim binds for conjunction/existential
# invariants; (2) a VARIABLE-DEFINITION hypothesis — ☐ₙ ≡ t with ☐ₙ
# not in t — is admitted as a rewrite rule even when size-increasing
# (each application strictly removes an occurrence, so it
# terminates): the "this variable is that machine" pattern every
# graph invariant produces.
whnf(C) = Prf p        p evident: whnf(p) = A with whnf(A) = 𝟙
                        (witness ()), or whnf(p) = (l  r  A) with
                        Γl  r : A ↓ (el-eq-i)
e-star# (⋆)
Γ  C
# el-squash-i / el-eq-i. A proposition that is not evident in one of
# these two shapes is a structural error (write `⋆ e` and supply a
# witness directly). Proof irrelevance (el-prf-prop) is not a
# checking rule but a DISCHARGE final: any two proofs of a Prf type
# are ≐, handled in the ↓ loop.
# THE payment rule, at equality props: ⋆ is the surface syntax for
# "this equation holds" — checking it emits the equation itself into
# ↓. Discharged by computation → silent; by an accepted lemma →
# silent; otherwise it IS the obligation, stated exactly where the
# user claimed it. There is no other proof syntax for equalities, by
# design: equality proofs carry no information (reflection erases
# them), so all structure lives in the judgemental layer and in
# prepended lemmas.
xΣ (as ?x)
e-hole# (?x)
Γ ⊢ ?x  C ⇝ ?x[𝕚𝕕]      extends Σ with (Γ  ?x : C)
# A RIGID HOLE (Foundation: sig-decl): a declaration entry at the
# AMBIENT context, referenced with the identity normal substitution
# ☐ₖ₋₁, ..., ☐₀. References are stuck (el-sig-decl); the hole is
# reported with its context and type, is never solved, and keeps Σ
# non-definitional — acceptance is blocked until the user edits it
# away. Checking position only: a hole in inference position is a
# structural error (its type is undetermined — ascribe). Hole names
# are unique per run. Interactivity is the point: the report (and an
# LSP consumer) answers "what goes here?" with the hole's type.
# The same token in TYPE position mints a type declaration
# (sig-ty-decl): Γ ⊢ ?x ⇝ ?x[𝕚𝕕] type, extending Σ with (Γ ⊦ ?x type)
# — (e-ty-hole). A hole-headed type offers no Π/Σ/quotient structure,
# so an intro form checked against one fails with the usual
# structural error, naming the hole.
#
# SOLVABLE HOLES: `_x` (or anonymous `_`, freshly named) mints the
# SAME declaration entry with one policy difference, recorded in the
# elaborator's display metadata: the elaborator MAY instantiate it.
# `_`-leading identifiers are reserved for this. Instantiation is a
# PATTERN SOLVE inside ↓: when an equation's beta-normal side is a
# reference to an unsolved solvable hole at its own context (the
# identity spine), the other side becomes the hole's body — the
# declaration FLIPS to a definition IN PLACE (Foundation:
# INSTANTIATION, in-place variant), kernel-checked against the PREFIX
# preceding the declaration by the skeleton-free tiny checker (§3 of
# NovaKernel.txt; a solution outside its fragment, or referencing a
# name minted after the hole, fails the check and no flip happens —
# conservative). After a flip the reference unfolds by el-sig-beta,
# so the forcing equation discharges by plain beta on retry, with an
# ordinary certificate — and so may the enclosing composite, retried
# once after decomposition before being assumed.
#
# A REPEAT occurrence of a hole name is a REFERENCE to the same entry
# (solved or not), legal at the entry's own context or any binder
# extension of it (the weakened identity spine), with the usual
# type-switch; a reuse in an unrelated context is a structural error.
# A solvable hole nothing pins simply REMAINS a declaration and is
# reported like a rigid one; `_`-holes may therefore appear in
# ACCEPTED files — a rerun re-solves them deterministically — while
# `?`-holes never can.
#
# Three refinements make elided PROOF-COMBINATOR INDICES (trans/sym-
# style applications with every index a `_`) solve wholesale — the
# intended fillings being near-syntactic, the machinery is kept
# deliberately first-order and intensional (in this extensional
# theory solutions are wildly non-unique up to ≐; the elaborator
# never searches that quotient — any pick is kernel-checked, and
# proof irrelevance makes index picks invisible downstream):
#  * ↓ decomposes WEAK-HEAD-normal sides first (whnf: contract the
#    head, keep every subterm as written; hole references are stuck),
#    falling back to the lemma-normalized sides only when the whnf
#    pair matches no case — full normalization would macro-expand
#    definitions into the children, and hypothesis REWRITING would
#    canonicalize straight through a hole's identity spine, masking
#    the pattern;
#  * the pattern solver takes the solution from the other side AS
#    WRITTEN when the kernel accepts it, walking it back into the
#    declaration's prefix by single δ-steps otherwise (a later-minted
#    def's DEFINIENS is often prefix-legal when its name is not); a
#    WEAKENED occurrence (the hole under k more binders, carrying the
#    weakened identity spine — an eliminator motive's body pinning
#    the eliminator's parameter) solves by STRENGTHENING the solution
#    back to the hole's own context, refused if it mentions any of
#    the k binders;
#  * an equation between two unsolved solvable holes ALIASES them:
#    the declared types are converted first (solving their own
#    embedded holes), then the later declaration flips to a reference
#    to the earlier.
# The kernel-Σ MIRROR of the solved holes happens once per item, at
# item end, in minting order (each solution is prefix-legal, so
# earlier mirrors carry later ones) — mirroring at flip time would be
# order-fragile: a solution may mention a hole solved only later in
# the item.
#
# ITEM-END CONSTRAINT DELETION (Foundation: DISCHARGE): a flip can
# make an equation assumed EARLIER IN THE SAME ITEM derivable by
# beta. At item end, each constraint the current item minted is
# re-attempted against its own Σ-prefix with the exact bare
# compare-beta-normal-forms certificate its site already embeds, and
# deleted on success — deletion never claims more than the kernel
# replay of the item will deliver, so a fully-resolved item is
# kernel-admitted as if nothing had ever been assumed. Constraints of
# EARLIER items are never deleted: their items' admission was already
# decided, and deleting their record would let a run end
# "definitional" around a skipped item. The remedy for a cross-item
# late solve is the usual one — reorder, or rerun.
whnf(C) = Prf A        Γe  A ⇝ ê
e-star-wit# (⋆ e)
Γ e  C
# el-squash-i, general form: e proves the squashee directly, whatever
# its shape (Π, Σ, anything). Erases to the same bare ⋆ as e-star —
# realizer irrelevance means the checked witness never survives into
# the core term, only into the skeleton (squash-wit, NovaKernel.txt)
# for the kernel to re-verify.
Γe  P        whnf(P) = Prf A        whnf(C) = Prf q
Γ  Ab  (Prf q)[]
Γsquash-elim e (x. b)  C                    # (squash-elim e (x. b))
# el-squash-e-prf: the only surface eliminator into a further
# proposition. The goal must itself whnf to Prf q — this is the
# structural enforcement of "no elimination into arbitrary types"
# (the restriction that blocks unique choice / description); a
# squash-elim checked against a non-Prf goal is a structural error.
# Erases to ⋆, same as every Prf-typed term (realizer irrelevance).
Γt  𝟘
e-zeroelim# (𝟘-elim t)
Γ𝟘-elim t  C𝟘-elim 
# Any expected C; 𝟘-elim is the one form that checks against
# everything. In inference position it is a structural error (ascribe).
Γe  A ⇝ ê
Γ  x:A  h:Prf (  ê[]  A[]) ⊢ b  C[  ]
Γlet x  e in b  Clet ê 
# let PROPAGATES the ambient mode to its body — this direct checking
# rule (rather than e-let + e-switch) is what lets a checking-only
# body form (a λ, a pair, a ⋆) sit under a let without ascription.
# C lives over Γ, so checking b at C[↑ ∘ ↑] is fully general, not an
# approximation (docs/NovaKernel.txt §8, el-let). The definiens and
# the hypothesis are exactly as at e-let.
Γt  B        ΓB  C type
Γt  C
# t any inference form. The mode switch is where inferred meets
# expected, and the ONLY place type conversion is consulted during
# term elaboration. Note the direction of failure: never an error —
# the residual equation is assumed and reported.

Mode inventory. Checking-only forms: λ, pairs, inj₁, inj₂, class, ⋆, ⋆ e, squash-elim, 𝟘-elim (their types are not determined by their syntax — an injection alone does not determine the OTHER summand); encountering one in inference position is a structural error whose fix is an ascription. let is BOTH-MODE: its body elaborates in the ambient mode (e-let / e-let-check), its definiens always in inference mode. Everything else — including ∥-∥ — infers and reaches checking mode through e-switch.

Conversion and discharge (the ↓ judgements)

Both ↓ judgements follow the same loop:

1. whnf both sides (this alone discharges everything the old derivation machinery called "by computation": β, El-decoding, signature unfolding). 2. α-equal → discharged. 3. Same rigid head → DECOMPOSE into component equations, each fed back into ↓. For the type formers and universe codes this is FAITHFUL — an equivalence, not merely sufficiency: downward it is Foundation's congruence rules, upward Foundation's injectivity rules (ty-pi-inj, ty-sigma-inj, ty-quot-inj, ty-eq-inj, ty-el-inj and their

     𝕌-code counterparts — see "Type constructor injectivity" there,
     including the semantic commitment they encode). Two cases remain
     merely sufficient: class-equations decomposed to their
     representatives (quotients are deliberately non-injective — the
     witness path below is the faithful route), and neutral-spine
     congruence (f a  f b from a  b). Each emitted obligation still
     carries the composite it descended from — as provenance, and
     because in those two cases the component can genuinely be
     stronger. A rigid HEAD MISMATCH stays an obligation, not an
     error: no-confusion is a meta-property of consistent contexts,
     not a rule, and the user may be working under inconsistent
     hypotheses. Decomposition:
       A₀  B₀    A₁  B₁      A₀  A₁ type;  Γ  A₁B₀  B₁ type
       A₀  B₀    A₁  B₁      likewise
       A₀  B₀    A₁  B₁      A₀  A₁ type;  B₀  B₁ type
                                 (both over Γ — non-dependent;
                                 faithful by ty-sum-inj)
       A₀ / r₀    A₁ / r₁      A₀  A₁ type;  Γ  A₁  A₁[]r₀  r₁ : Ω
                                 (the relation is compared AT Ω, where
                                  is iff — ty-quot-cong)
       Prf p      Prf q         p  q : Ω     (ty-prf-cong)
       (a₀b₀T₀)  (a₁b₁T₁) : Ω
                                  T₀  T₁ type;  a₀  a₁ : T₁;  b₀  b₁ : T₁
                                 (code-eq-cong — merely SUFFICIENT at
                                 Ω, where  is iff; the faithful
                                 route is propext)
       El a       El b         a  b : 𝕌
       A        B          A  B type (sufficient), OR — the
                                 faithful route at Ω — code-prop-eq
                                 (propext): the two implications
                                 Prf A  Prf B and back, each with
                                 its witness synthesized under the
                                 hypothesis
       𝒮₀.𝕤 ē₀   𝒮₁.𝕤 ē₁      the signatures identical nameless ToS
                                 syntax up to embedded Nova pieces and
                                 the sort positions equal (else the
                                 composite stays an obligation), the
                                 aligned Nova pieces pairwise in ↓,
                                 the index spines componentwise —
                                 FAITHFUL (QIIT congruence +
                                 injectivity; type and 𝕌-code alike)
       𝒮.𝕔 θ₀    𝒮.𝕔 θ₁       θ componentwise — merely SUFFICIENT,
                                 like class: point constructors are
                                 not injective (equation constructors
                                 may merge them); the faithful route
                                 is a path lemma from E (the data
                                 item's eq-lemmas land there)
       S a        S b          a  b : 
       inj₁ a     inj₁ b       a  b : A  (at A  B; faithful —
                                 injection injectivity is derivable;
                                 likewise inj₂ at B. An inj₁/inj₂
                                 HEAD MISMATCH stays an obligation,
                                 like every rigid mismatch)
       class a    class b      a  b : A, OR — the WITNESS path,
                                 (classr) — by the shape of the
                                 instantiated relation r[id, a, b] (an
                                 Ω code): a 𝟙-shaped relation is
                                 inhabited outright (witness ()), an
                                 equality-prop-shaped one reduces the
                                 witness to its equation ( by
                                 el-eq-i); other shapes keep the
                                 composite
       a₀ , b₀    a₁ , b₁      componentwise at the Σ-type
       neutral spines with the same head variable/eliminator:
                                 componentwise (app-cong, proj-cong,
                                 ℕ-elim-cong, quot-elim-cong)

4. Mixed El: whnf leaves `El a` (a neutral) against a rigid type B. When B is in the image of El-decoding with codable components

     (𝟘, 𝟙, , arrows/pairs/quotients/eq of codable parts), reduce to
     a  code(B) : 𝕌 — sufficient via El-congruence + El-decoding.
     Otherwise fall through to 7.

5. Prop-discharge: an element equation at type 𝟙, 𝟘, or Prf p is discharged outright — Foundation's el-one-prop, el-zero-prop, el-prf-prop (proof irrelevance: any two proofs of a proposition

     are equal; equality proofs included, since  is Ω-valued and
     its proofs live at Prf).

6. η: a λ against a neutral at Π compares via el-pi-eta (apply

     both to  under the binder); a pair against a neutral at Σ
     via el-sigma-eta.
     η fires ONLY when one side is a literal introduction form: two
     neutrals gain nothing from η, and η-expanding them regenerates
     the very eliminations congruence descent (step 3) came from —
     an η/congruence loop.

7. STORE USE — three complementary mechanisms over E:

     * REWRITING: equations usable as terminating rules — strictly
       size-decreasing instances first (plus n Z  n), then
       size-preserving NON-PERMUTATIVE ones (plus n (S m) 
       S (plus n m), induction hypotheses) — applied left-to-right
       as stated, at any subterm, to a fuel-and-seen-set-bounded
       fixpoint before every comparison. An equation whose sides are
       equal up to a bijective renaming of its parameters
       ("permutative": commutativity, exchange laws) NEVER rewrites —
       it would oscillate.
     * WHOLE-EQUATION MATCH: the equation (or its flip) matches a
       candidate's l/r under one consistent first-order
       instantiation; parameters the sides do not bind must carry a
       Prf (equality props included) or 𝟙 type whose instance
       discharges as a side condition.
       This is how permutative and hypothesis-conditional lemmas
       discharge. Matching is up to El-DECODING: normalization
       decodes El c at concrete codes (El c  ) — inside carried
       QIIT signatures too — so a pattern position El p (p a
       parameter) facing a decoded rigid type binds p to that
       type's code. A generic bag-swap lemma thus discharges its
       -instantiated goals.
     * TRANSITIVITY HOPS: a candidate that rewriting cannot apply
       may rewrite one side WHOLESALE, recursing with a small
       depth budget — chaining e.g. an exchange law, a hypothesis,
       and an exchange law again.
     Matched candidates' sides are stored normalized against the
     lemma store as of their acceptance, so equations stated in one
     spelling still match goals earlier rules have canonicalized.
     An already-assumed obligation matches verbatim (deduplication:
     nothing new is reported, and nothing is considered proven).
     Closing E under full congruence (e-graph style) remains a
     completeness upgrade; none of these mechanisms affects
     soundness — each discharge is a Foundation derivation via
     (el-sub-cong-fix) + congruence + transitivity + reflection.

8. ASSUME: append the equation to Σ as a constraint entry (sig-eq/ sig-ty-eq), record its display metadata (source position, and the composite it was decomposed from, if any), and add it to E; succeed.

Invariant (statement well-formedness): every equation reaching ↓ has both sides produced by elaboration at the stated type, in the stated context, under the assumptions active at that moment. Consequently each constraint entry is well-formed against its Σ PREFIX — exactly the premise shape of sig-eq — and the report order is always a valid discharge order. An obligation whose statement depends on earlier assumptions is annotated with them; prove those first (or in one joint lemma) and the later statement becomes statable in the base theory. Cyclic dependence cannot arise in this hole-free setting: assumption strictly precedes use, in file order.

Items

εTA type
εt  A
def x : T  t          extends Σ with (ε  x   : A)
εTA type
type x  T             extends Σ with (ε  x  A type)
εTA type
def x : T              extends Σ with (ε  x : A)
# A DECLARATION — a def without a definiens (Foundation: sig-decl at
# ε). Treated as a NAMED RIGID HOLE end to end: same Σ entry, same
# open-holes report row, same acceptance wall; references type by
# el-sig-decl and are stuck. One addition beyond a hole: a declared
# EQUATION (a Prf-of-≡ type, possibly under Π-binders) registers in
# the lemma store like any accepted lemma — its stuck reference is a
# proof element, so el-reflect makes the equation judgementally
# available. That is the abstract-interface idiom: declare the
# carrier and its laws, program against them, and everything checks
# relative to the interface (and is ACCEPTED only once the
# declarations are given definientia).

Parameters are Π-binders in T; partial application of an item is therefore first-class, which the telescoped form never was (x[e˲] demanded the full substitution back to Γ). The price is confined to TYPE items: a parameterized family must live in 𝕌 (a def returning 𝕌-codes, like vect) — a family whose result is genuinely large has no code and, in the empty-context discipline, no spelling. None is needed today; if one ever is, telescoped type items (and the substitution syntax, for them alone) are the designed escape hatch.

Duplicate entry names are a structural error. An entry elaborated under assumptions still enters Σ and the rest of the run builds on it — by design (see report semantics): one run surfaces ALL obligations, at the price that obligations surfaced downstream of an assumption are provisional until it is proven.

QIIT signatures: the data item

A data item is an ITEM MACRO. It elaborates its literal to a core signature 𝒮 (Foundation's qctx — a signature IS a closed qiit-context) over the item's PARAMETER telescope — the [x : T] groups realize Foundation's ambient Γ in Γ ⊦ 𝒮 qsig, with parameters in scope as external names throughout the literal — and then EXPANDS into a batch of ordinary defs, each Π-abstracted over the parameters (the carried 𝒮 weakened along each emitted binder); the macro itself adds nothing to Σ. Instantiated signatures still compare STRUCTURALLY (𝒮[a≔ℕ] is one piece of syntax wherever it arises), so a parameterized data item is a FAMILY of structurally-identified QIITs. This is Foundation's design surfacing: 𝒮 mints no names, "a NAME for a QIIT is an ordinary definition", so sorts, constructors, path lemmas and eliminators all reach the file as plain Σ entries whose bodies carry 𝒮 — and modules, imports, the lemma store and the report treat them like any other def. Two textually identical data items therefore yield JUDGEMENTALLY EQUAL types (the defs unfold to the same 𝒮 — structural identity, no generativity), and the elaborator compares same-name references before unfolding (rigid-rigid-before-δ) so the common case never looks inside 𝒮.

Elaborating the literal mirrors Foundation's qctx/qty/qtm rules, declaration by declaration. The ToS layer is syntax-directed and needs no annotations; the parser has already resolved each name to a ⬡-index or entry position (locals shadow, names(𝒮)-freshness is a parse error), and classified each Π domain (inductive iff its head is a sort of the same literal). All content is in the embedded NOVA pieces:

  Γx ⊢ TA type          # an EXTERNAL domain: an ordinary type over
                           # Γx, the external binders in scope — the
                           # Nova zone of Foundation's dual zone
  Γx ⊢ t  A[]        # an external APPLICATION argument likewise

— so obligations may surface inside a signature exactly as they do inside any type, and land in O with the data item as their site. Inductive codes and terms elaborate structurally (qtm-var/app against the resolved positions); the result heads classify each entry (sort / point / equation) per Foundation.

The EXPANSION, for each entry of the accepted 𝒮 (⌊·⌋, ⌊·⌋ᵗ, ·ᴰ⟨·⟩, ·ᴰᵗ, ⟦·⟧ are Foundation's meta-operations; δ the telescope variables):

  • SORT 𝕤 : 𝔎, 𝒮 small — def n : Π(⌊𝔎⌋ᵗ). 𝕌 ≔ λ…. 𝒮.𝕤 δ # code-qiit (a code-valued family; users write El (n ī). If 𝒮 is LARGE: a nullary sort becomes type n ≔ 𝒮.𝕤 · and an INDEXED large sort is a structural error — a large family has no spelling in the closed-item discipline; see the e-typedef note. The escape hatch is the same one designed there.)
  • POINT constructor 𝕔 : 𝔄 — def n : ⌊𝔄⌋ ≔ λ…. 𝒮.𝕔 δ # el-qiit-intro, the saturated former η-expanded once; partial application is thereby first-class at zero cost.
  • EQUATION constructor 𝕔 : 𝔄 ending in El (l ≡ r) — def n : Π(⌊𝔄⌋ᵗ). Prf (⌊l⌋ ≡ ⌊r⌋ ∈ ⌊El 𝕦⌋) ≔ λ…. ⋆ — the ⋆ is licensed by el-qiit-path (kernel: a refl-eq certificate whose single step is a path license, qpath). On every LATER item and run this def is an ACCEPTED LEMMA, so the imposed equations of a QIIT feed discharge through the standard E machinery — no new mechanism, and rewriting/matching treat them like any user lemma.
  • ELIMINATORS, two defs per sort 𝕤 (surface names cannot contain '-'). The CODE-VALUED one, named nElim: def nElim : (C₁ : Π(⌊𝔎₁⌋ᵗ). El (𝒮.𝕤₁ δ) → 𝕌) → … # motives, # one per sort → (m𝕔 : ⌊𝔄ᴰ⟨𝒮.𝕔 δ⟩ with El∘C for C⌋) → … # methods, one # per point ctor → (h𝕔 : Π(𝔄ᴰᵗ). Prf (⟦l⟧ ≡ ⟦r⟧ ∈ El (C… ))) → … # COHERENCES, # one per eq ctor → Π(⌊𝔎⌋ᵗ) → (w : El (𝒮.𝕤 δ)) → El (C_𝕤 δ w) ≔ λ…. 𝒮.𝕤-elim ℰ δ w # ℰ = the bound motive/method # variables, as Foundation's C̄ ; m̄
    COHERENCES ARE HYPOTHESES: extensionality lets the eprob premises
    be taken as ordinary Prf-typed arguments. Inside the generated
    body, each coherence premise reaching ↓ is discharged by the
    HYPOTHESIS source of E (the equality-hypothesis binder h𝕔, peeled
    — exactly the mechanism
    that makes induction hypotheses silent), and the kernel's qcoh
    certificates replay from those same binders by el-reflect. At USE
    sites there is no new judgement at all: supplying a coherence is
    supplying an argument, `` when the methods respect the equation
    by computation (e-star surfaces it as an ordinary obligation
    otherwise), a lemma reference when proven separately. This is
    quot-elim's f⁼ story, generalized and MOVED INTO THE TYPE — which
    is why the eliminator needs no inline-motive surface form.
  • The PROP-VALUED eliminator, named nElimP: same shape with Ω for 𝕌 and Prf ∘ C for El ∘ C — and NO coherence arguments at all: its coherence sides live at a Prf motive, where el-prf-prop closes them outright, so the emitted qcoh certificates are bare FProp finals. This is the induction principle for PROPOSITIONS — in particular for equality props, which is how open equational facts about a QIIT are proven now that equality has no 𝕌-code (e.g. plusQzr in qiitNat.nova: NElimP at the motive (λn. (plusQ n z ≡ n ∈ El N))): def nElimP : (C₁ : Π(⌊𝔎₁⌋ᵗ). El (𝒮.𝕤₁ δ) → Ω) → … # motives → (m𝕔 : ⌊𝔄ᴰ⟨𝒮.𝕔 δ⟩ with Prf∘C for C⌋) → … # methods → Π(⌊𝔎⌋ᵗ) → (w : El (𝒮.𝕤 δ)) → Prf (C_𝕤 δ w) ≔ λ…. 𝒮.𝕤-elim ℰ δ w

Motives in the generated eliminators are 𝕌- respectively Ω-valued — the closed-item discipline again; the CORE former supports arbitrary large motives and the kernel checks them, but beyond Prf no surface spelling reaches them today (future work, with telescoped items).

Worked example — finite multisets over a code a : 𝕌 (Foundation's Bag, here with a small external domain so the sort is codable):

  data ( Bag : U
       ; nil : El Bag
       ; ins : (x : El a) (m : El Bag)  El Bag
       ; swp : (x : El a) (y : El a) (m : El Bag)
                  ins x (ins y m)  ins y (ins x m)  El Bag )

expands to (𝒮 the elaborated signature, positions 0..3):

  def Bag  : 𝕌  𝒮.0 ·
  def nil  : El Bag  𝒮.1 ·
  def ins  : El a  El Bag  El Bag  λx. λm. 𝒮.2 (x, m)
  def swp  : (x : El a) (y : El a) (m : El Bag)
                ins x (ins y m)  ins y (ins x m)  El Bag
            λx. λy. λm.                        # qpath-licensed
  def BagElim :
        (C : El Bag  𝕌)
       (mnil : El (C nil))
       (mins : (x : El a) (m : El Bag)  El (C m)  El (C (ins x m)))
       (hswp : (x : El a) (y : El a) (m : El Bag) (m : El (C m))
                   mins x (ins y m) (mins y m m)
                     mins y (ins x m) (mins x m m)
                     El (C (ins x (ins y m))))
       (w : El Bag)  El (C w)
       λC. λmnil. λmins. λhswp. λw. 𝒮.0-elim  · w
                          # ℰ = (C ; mnil, mins) from the binders;
                          # the coherence discharges from hswp (E's
                          # hypothesis source) and replays as qcoh

A caller writing BagElim C z f h supplies h as ⋆ when f respects the swap by computation — e-star turns it into an ordinary obligation otherwise — or as a reference to a proven lemma. Nothing about obligations, discharge or the report is QIIT-aware.

Modules

A MODULE is a file; a dotted module name resolves against the root file's directory (import Data.Nat ⇝ <rootDir>/Data/Nat.nova). Import lines precede items. The import graph must be a DAG — cycles are reported by name — and diamonds are deduplicated by module name, so a shared dependency elaborates once per run.

Execution model: TRANSITIVE RE-ELABORATION. A run loads the graph, orders it dependency-first, and elaborates every module through the full pipeline — same elaborator, same kernel gate, one flat Σ. The reproducibility invariant lifts verbatim: THE ROOT FILE PLUS THE TRANSITIVE SOURCES OF ITS IMPORTS DETERMINE ACCEPTANCE. (A certificate cache — persist each accepted module's annotated items and replay them through the kernel alone, skipping elaboration — is the designed next step; it changes cost, not meaning, and never trust.)

Names: a module M's entries enter Σ under qualified names (M.x); the ROOT file's entries stay bare. An unqualified reference resolves locals → opened names → the module's own entries; `import M` alone makes M's names accessible QUALIFIED ONLY (M.x); `import M (a, b)` additionally opens a and b bare. Opening a name M does not define is an error. Qualification is purely a front-end affair — Σ names are flat strings, and the kernel is unchanged.

Acceptance is compositional: ONLY ACCEPTED MODULES ARE IMPORTABLE. A module elaborated with open obligations aborts the run with its own report — the file-internal rule that an assumption poisons every later item's kernel acceptance, promoted to a boundary. Corollaries: an obligation is always discharged within the module that surfaced it (imports precede items, so imported lemmas are in E before anything local elaborates), and the report is always local to one module.

Two consequences worth stating plainly:

  • Σ-inclusion is transitive (an imported entry's body references ITS imports, which the kernel must resolve), and so is qualified access; only bare-name visibility is per-module.
  • The lemma store is built from Σ, so importing a module imports its equalities as discharge candidates — that is the point — and import order, like item order, is semantic: candidate sides are normalized against the store at storage time.

The report

At end of run, obligations are reported in surfacing order:

  open obligations (2):
    [1] (n : ) ⊢ plus n Z  n : 
        at: vappend_nil, line 14 (checking )
    [2] (n m : ) (a : 𝕌) (xs : El (vect n a)) ⊢ ...
        at: vappend_assoc, line 22 (switch: inferred vs expected type)
        from composite: El (vect (plus n Z) a)  El (vect n a) type
        statement uses: [1]

Report conventions:

  • Statements are printed in named surface syntax, in their full context (binder names recovered from the name environment).
  • `from composite:` shows the pre-decomposition equation, for the case where the sufficient direction overshot.
  • `statement uses:` lists the earlier obligations under which this statement is well-formed; discharge those first. (Coarse approximation — "all earlier ones" — is a legal fallback.)
  • Deduplication is by statement, so each equation appears once no matter how many sites hit it.
  • Exit status: accepted iff the list is empty.

Discharging an obligation: prepend, before the item that surfaced it,

  def plus_zero : (n : )  plus n Z  n    λn. <proof>

— an ordinary def whose type is the obligation's statement as an equality type (generalized over its context by Π-binders). On rerun, its reflected equation is in E before the surfacing site elaborates, and step 7 discharges silently. The proof itself is whatever the theory requires — `⋆` when the equation is by computation, an ℕ-elim with an equality motive for inductive content — and elaborating IT may surface further (strictly smaller) obligations; the loop converges because each accepted lemma is content the file genuinely needed.

Metatheory: the soundness contract

Let T₀ be the theory of docs/NovaFoundation.txt over the accepted signature, and let O₁, ..., Oₙ be the obligations of a completed run in surfacing order. The contract every rule above must respect:

  (Stratification) For each i, the statement of Oᵢ is well-formed in
  T₀ + O₁ + ... + Oᵢ₋₁ (obligations adjoined as equality axioms — a
  conservative kind of extension to state, since equality proofs are
  irrelevant and axioms add no computational behavior).
  (Soundness) Every signature entry produced by the run is derivable in
  T₀ + O₁ + ... + Oₙ. In particular, a run with n = 0 yields Foundation
  derivations outright: Σ sig.
  (Discharge) If each Oᵢ is proven by a prepended lemma — elaborated
  earlier in the file, hence in a theory not containing Oᵢ...Oₙ — then
  by cut (replacing axiom leaves with the lemmas' reflections) the
  accepting run's entries are derivable in T₀ alone. File order
  witnesses non-circularity; no provenance tracking is needed beyond
  it. The accepting run is the sole authority: nothing computed by a
  dirty run — including Σ entries elaborated under assumptions — has
  any standing beyond guiding the user to the next edit.

Two corollaries worth keeping in view while implementing:

  • A SOUNDNESS HOLE, confirmed by exploit and since CLOSED architecturally: rewriting and matching are first-order and TYPE-BLIND — the equation store drops each equation's type, and parameter bindings are never type-checked. Two confirmed consequences: a parametric 𝟙-lemma (x y : 𝟙 ⊢ x ≡ y ∈ 𝟙, itself true) matches EVERY equation at EVERY type and would certify e.g. Z ≡ S Z ∈ ℕ; and a class-equation proven at one quotient would discharge the syntactically identical claim at another. The resolution was architectural, not a smarter matcher: the discharge engine sits outside the trusted boundary and emits certificates replayed by a dumb kernel — a bad discharge is a rejected trace, not an unsound acceptance, and both exploits are regression tests that end in obligations. See docs/NovaPipeline.txt ("Why this shape" and "Status") for the design.
  • Terms never contain transports: obligations are assumed, not materialized as coercion nodes, so an accepted file's core terms are exactly what the user wrote, and judgemental equality does all the moving. This is the extensionality dividend, and it is why the obligation mechanism composes: proving Oᵢ never changes any term, only the acceptability of the file.

Future work (explicitly out of scope here)

  • Holes / metavariables: pattern unification over the same constraint store, with two report goal kinds (fill / prove). Ground-only obligations; no erasure step (reflection, transitivity-through-a- midpoint, witness erasure) may fire on a premise whose statement mentions an unsolved hole — such steps postpone until the hole is filled. This restriction is what keeps occurs-checking a complete dependency criterion and the instantiation lemma stateable.
  • Congruence/transitivity closure of E (e-graph) for discharge completeness; `using <lemma>` hints for deterministic discharge.
  • Incremental re-elaboration (caching per item) — requires recording per-item assumption sets; whole-file re-runs make this unnecessary at current scale.
  • QIITs: large-motive elimination at the surface (an expression-level eliminator form, or telescoped items); inline signature literals in type/element positions (today a QIIT is reachable only through a data item's generated names); indexed sorts of LARGE signatures (unnameable in the closed-item discipline).

Nova Pipeline

Rendered from docs/NovaPipeline.txt — the plain text remains the source of truth.

NovaPipeline.txt — the processing pipeline and its trust story

Purpose

This file is the map: what the layers are, what artifact each one produces, where the trust boundary sits, and which document specifies each part. It records the architecture converged on after the elaborator's first implementation exposed a consistency-grade hole in trusted equality search (see "Why this shape" below); the individual layers are specified elsewhere:

  • docs/NovaFoundation.txt — the THEORY. Sole source of truth; every other layer answers to it.
  • docs/NovaKernel.txt — the KERNEL, rule by rule: fuel-bounded normalization, certificate replay, item-level checking over skeletons.
  • docs/NovaElaboration.txt — the elaborator: surface syntax, bidirectional rules, the obligation lifecycle.

(The derivation-era machinery — .rules sessions, its checker, parsers and docs — has been removed; the pipeline below replaced it.)

The pipeline

  .nova source (surface syntax)          — authored: by a human or AI
      │
      │  parse + scope resolution        (pure front end)
      ▼
  indexed surface AST                    — nameless; still carries
      │                                    ascriptions and motives
      │  ELABORATOR                      (untrusted)
      │    bidirectional pass; at each conversion site consults the
      │    DISCHARGE ENGINE (untrusted tactic); records everything it
      │    invents or is handed
      ▼
  per item: ANNOTATED TREE               — the certificate-carrying
      │                                    artifact (see below)
      │  KERNEL                          (trusted, total)
      │    synthesis over the annotated tree + fuel-bounded beta +
      │    certificate replay; no search, no choices, always a verdict
      ▼
  accept / reject                        — the only verdict that counts;
                                           accepted erasures extend the
                                           kernel's Σ (Foundation's Σ,
                                           exactly)

The trust boundary

Everything above the kernel is UNTRUSTED. The elaborator may be arbitrarily clever; the discharge engine may search, rewrite, and heuristically match; none of it is believed. The kernel re-establishes every judgement from its own Σ using only:

  • type synthesis over the annotated tree (annotations supply what synthesis cannot invent — see artifact format);
  • FUEL-BOUNDED beta conversion (Foundation's ≜ rules: the beta family, El-decoding, signature unfolding) — step budgets come from the certificate, exhaustion means REJECT, so the kernel is total: every artifact gets a verdict;
  • CERTIFICATE REPLAY: at a conversion site, apply the recorded trace steps mechanically — check each step's proof element, rewrite at the given path in the given orientation, compare normal forms (fuel-bounded normalization between the recorded extensional steps).

Consequences of the split:

  • A discharge-engine bug is INCOMPLETENESS (a failed trace → the obligation stands), never unsoundness. A bad emitted trace is rejected at replay. The engine's soundness is a quality property, not a safety property.
  • The same holds for elaborator bugs generally: a wrong core term, a mis-substituted type, a bogus motive all die in the kernel.
  • The kernel is small enough to audit against NovaFoundation.txt rule by rule, and is the only component with that obligation.

The artifact: annotated trees, not annotated terms

Foundation's core syntax stays BARE — and the kernel, checking spellings, necessarily works extrinsically even though the theory's official reading is intrinsic (docs/NovaSyntax.txt): a spelling inhabits many types at once (a spelling and its El-decoding; an index and its lemma-equal form), so "the type of a subterm" is not recoverable from the artifact — only a chosen spelling. Nothing judgmentally inert belongs in the theory's syntax: no coercion or transport term formers, no type annotations, no J. (Coercion is a RULE — el-ty-coe — and stays one. Equality proofs are consumed by reflection and produced as ⋆; the composition that J/sym/trans/cong would provide inside terms is provided by trace structure instead: chaining is a list, placement is a path, symmetry is a flag.)

The kernel's INPUT, however, is richer than a bare term: an ANNOTATED TREE — the elaborator's output where each node optionally carries exactly what the bidirectional pass invented or consumed there:

  • eliminator motives (ℕ-elim, quot-elim) — bare core is not even re-checkable without them;
  • the expected type at checked introduction forms;
  • conversion traces at switch sites: chains of (path, proof element, orientation) steps, plus the quotient-witness step kind carrying its witness element;
  • fuel budgets for the kernel's normalization (per item or per site; the elaborator knows its own step counts and writes in a margin).

An ERASURE function maps annotated trees to Foundation core terms, and the kernel invariant is: kernel accepts the annotated tree ⟹ the erasure is Foundation-derivable at the stated type. Equality, normalization, the lemma store, and printing all operate on erasures — the annotation layer is invisible to the theory. The slogan: type information travels WITH terms in the implementation, and is never OF terms in the theory.

Caveat recorded once, binding everywhere: an annotation is a REPRESENTATIVE, not a canonical type — canonicity is unavailable in principle (spellings are unique only up to a hypothesis-sensitive, undecidable equality). No consumer may compare annotations syntactically; only up to conversion.

Computation in the kernel: bounded, not certified

A design alternative was considered and recorded here deliberately:

move beta itself into the certificate (every -step a recorded

(rule, path) entry; the kernel a pure single-step replayer comparing terms syntactically). Its attractions are real — the kernel becomes structurally total, the certificate becomes a literally linearized Foundation equality derivation (finest possible audit granularity), and no strategy coupling between elaborator and kernel can exist.

It loses on measured grounds: computation-heavy discharges (numeral tests, unfolding recursive definitions) make traces proportional to reduction length with β-duplication blowups; the kernel sheds only the fixpoint driver anyway (single-step application is the same clauses, and substitution — the genuinely subtle part — stays trusted because TYPING needs it); and head-exposure traces would spread annotation plumbing to every elimination position.

The deciding observation: in this theory β was never the dangerous part of conversion. It is confluent, canonical, owned by the theory's

own  rules, and not user-extensible; the undecidable,

hypothesis-sensitive part of conversion is the EXTENSIONAL part, which is already certificate-side. β's only sin is potential divergence under inconsistent hypotheses — a liveness problem, cured by fuel.

Decision: the kernel keeps the -engine, FUEL-BOUNDED, budgets

supplied by the certificate, exhaustion = reject. Totality is preserved (the verdict gap is closed), certificates stay small (a number per site, not a computation log), and the audit story is

unchanged (the kernel's normalizer mirrors Foundation's  rules

clause for clause). Full trace-beta remains the documented FALLBACK, to be revisited only if per-step auditability is ever needed (e.g. exporting kernel derivations to an external checker) or fuel coupling bites. The floor in every variant: α-comparison and substitution stay trusted — no kernel design knows less than that.

Who produces what: the two tactic layers

The criterion is addressability and persistence.

  • The DISCHARGE ENGINE (built into the elaborator; rewriting, whole-equation matching, transitivity hops, quotient witnesses) emits CERTIFICATES. Its inputs are core-level equations at sites internal to elaboration — there is no surface position its output could occupy, by design: the surface has no coercion syntax. Certificates are machine-to-kernel format: ephemeral, regenerated each run, never authored, never read by the user.
  • AI-LEVEL TACTICS (the AI itself; any future synthesis script) emit SURFACE SYNTAX: lemma defs prepended to discharge obligations, proof bodies, hints. Obligations — the agent-facing interface — are statements, and statements are surface currency.

The boundary is hard: external agents may NOT inject certificate steps. If the engine finds no trace, the site surfaces as an obligation and the remedy is a surface lemma that makes the trace findable (typically turning a search into a one-step direct match). This preserves the reproducibility invariant:

  THE .nova FILE ALONE DETERMINES ACCEPTANCE.

The elaborator is deterministic, so certificates need no persistence for correctness — persisting them is a cache/audit policy. Nothing an agent did that is not in the source file can affect the verdict.

The obligation lifecycle (unchanged)

Discharge failure is never an error: the equation is assumed — as a CONSTRAINT ENTRY of the run's signature (Foundation: sig-eq/sig-ty-eq; Σ is OPEN mid-run) — deduplicated, and reported at end of run with its site and the composite it descended from. The user or AI discharges an obligation by prepending an ordinary def whose type is the obligation's statement as an equality type, and re-running. A file is accepted exactly when the run's final signature is DEFINITIONAL (no constraints, and — once surface holes land — no declarations) AND the kernel replays every certificate. Nothing survives between runs. (Full lifecycle, stratification and metatheory: docs/NovaElaboration.txt.)

Why this shape

The first elaborator implementation placed the discharge engine inside the trusted boundary: its rewriting and matching were type-blind (first-order, equation types discarded), and two confirmed exploits followed — a parametric 𝟙-lemma (x y : 𝟙 ⊢ x ≡ y) whose pattern matches EVERY equation at EVERY type, certifying Z ≡ S Z ∈ ℕ; and cross-quotient transport of syntactically identical class equations. Both are consistency-grade: acceptance authority with no kernel behind it means an unsound discharge is an unsound acceptance.

The lesson is the LCF lesson: search may not live inside the trusted boundary. But the opposite pole — no engine, AI-authored proof terms (J/transp combinators) everywhere, kernel-only checking — was examined and rejected on measured grounds: transport placement is dense (the derivation era's coercion ceremony, friction the whole design exists to eliminate), motives are the most error-prone objects agents write, statements would inherit the transports, and failures would degrade from "here is the missing equation" to "your combinator tower is mistyped." Equality reflection is what makes the middle available: because every coercion is judgmentally the identity, WHERE the transport lives is bureaucracy, not semantics — so it can live in a machine-written, machine-checked, erasure-invisible layer, and the surface stays exactly as clean as the theory promises.

Status

Implemented: the front end; the elaborator; the obligation lifecycle; the src/nova/ corpus; the MODULE SYSTEM (file = module, DAG imports resolved by transitive re-elaboration, qualified names as flat Σ strings, only accepted modules importable — docs/NovaElaboration.txt, "Modules"); the EQUATION KERNEL with the demotion of engine verdicts to proposals — Nova.Kernel provides

fuel-bounded normalization (mirroring the  rules clause for clause,

exhaustion = reject), proof-element inference/checking for elimination spines and intro forms, injectivity selectors, TYPED PATH DESCENT (every rewrite's licensed equation is verified against its position's locally determined expected type — intermediate hops need no type, congruence only demands the child equation at the rewrite point), and replay of the certificate finals (beta, el-zero-prop/el-one-prop, quotient witnesses, el-pi-eta/el-sigma-eta). The discharge engine emits certificates for every discharge (rewrite traces with parametric-context normalization bridging, whole-equation matches with condition witnesses, hop chains, injectivity-selector components), and convElem/convTy count a discharge ONLY if its certificate replays — a replay failure is reported on the resulting obligation. Both historical exploits are golden tests that now END IN OBLIGATIONS (elab-reject-prop-solvent, elab-reject-cross-quotient): the parametric 𝟙-lemma dies at proof argument checking, the cross-quotient transport dies at the positional type check.

The ITEM-LEVEL kernel is implemented: bidirectional re-checking of whole core items over ANNOTATION SKELETONS — trees positionally aligned with the core term carrying eliminator motives, expected types at checked intro forms, switch/refl-eq/well-definedness certificates, and head-exposure payloads (an expected type whose Π/Σ/quotient structure only lemma normalization exposes ships as the exposed type plus a type certificate). The kernel's Σ is the authoritative one: an item is admitted to it only when the item re-checks from kernel Σ alone, and a file is accepted exactly when the run's final signature is definitional and every item was so admitted. Two consequences of that discipline are load-bearing:

  • certificates carry a TYPE BRIDGE (the equation-level counterpart of the exposure payload): a conversion site whose replay steps land at positions only a lemma-normalized type determines is replayed at that exposed type, justified by a nested TYPE certificate — equal types have equal PERs, and a bogus bridge dies in replay like any other bad step;
  • a conversion the engine can only close by DECOMPOSING (children discharged, but no composite certificate expressible) is assumed, not silently accepted — the composite surfaces as an ordinary obligation and the remedy is the usual one, a lemma that makes it directly matchable. Likewise "clean" is a property of the RUN, not the item: an assumption anywhere poisons every later item's kernel acceptance (the kernel Σ cannot contain the earlier item, so references to it are unresolvable anyway).

Acknowledged approximations, now confined to EQUATION REPLAY (the item level carries real motives): ℕ-elim z/s rewrite positions and ℕ-elim proof arguments use the CONSTANT-MOTIVE reading — a valid congruence/elimination instance whose premises are demanded at the constant type.