Nova Foundation

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

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 (⊦ : ≐ …) 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. The reading is adopted directly, with no separate formalisation document; canonicity-style consequences are stated as meta-properties where they are used.

THERE IS NO TYPE JUDGEMENT

Earlier presentations carried a separate judgement pair Γ ⊦ A type / Γ ⊦ A₀ ≐ A₁ type; both are DISSOLVED into the element judgements at the TOP UNIVERSE 𝕍 — Γ ⊦ A : 𝕍 and Γ ⊦ A₀ ≐ A₁ : 𝕍 — and the type and element grammars are merged into ONE term sort. 𝕍 is an ordinary term former with NO typing rule of its own (see THE TOP UNIVERSE in the type rules); "A is a type" everywhere below MEANS Γ ⊦ A : 𝕍. The dissolution is presentational except at one point, where it is an extension: the type slot of the equality proposition admits 𝕍, so type-equality props (A ≡ B ∈ 𝕍) exist and type equality is reflection-complete like element equality (see code-eq and its SEMANTICS note in the Ω block).

AND NO EQUALITY JUDGEMENT

The equality proposition fully internalizes judgemental equality, so the judgement dissolves into it: `Γ ⊦ a₀ ≐ a₁ : A` is DERIVED NOTATION for `Γ ⊦ ⋆ : (a₀ ≡ a₁ ∈ A)` — the prop IS the type of its proofs (Prf is retired, see PROP-CUMULATIVITY); A = 𝕍 giving type equality — and the remaining equality forms (contexts, substitutions, telescopes, spines) are META-DEFINITIONS over it (see EQUALITY in the conventions). ONE typed judgement remains. EQUALITY REFLECTION thereby stops being a principle and becomes the definition, and it leaves NO primitive residue: the rule kept under the name el-reflect — ⋆-canonicity, any inhabitant of an equality prop yields the ⋆-typing — is itself ADMISSIBLE, forced by Ω-valuedness (an inhabited prop is ≐-equal to ∥𝟙∥ by code-prop-eq, and ⋆ transports across; see its note in the Ω block). The setoid model interprets both spellings as the same relation, so this dissolution is purely presentational; every rule below keeps its ≐-spelling, read through the notation. (The DISSOLVED NAMES table at the end of this file maps every retired rule name to its replacement.)

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 : (A ≡ (A → A) ∈ 𝕌), the equation A ≐ A → A holds (and lifts to types by code-lift-eq), so self-application types and ω ω is well-formed at 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 and DEFINITIONALLY reflected — the judgemental spelling ≐ is notation for its ⋆-inhabitation — a prop IS its type of proofs (prop-lift); 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)
• The top universe: 𝕍 — the types are exactly its elements (Γ ⊦ A : 𝕍 is this theory's "A is a type"); 𝕍 itself is not typed: it has no typing rule, no code, and heads no context entry, Π-domain, or squash — see THE TOP UNIVERSE note
• 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 — TWO entry kinds; A ranges over terms INCLUDING 𝕍, so type definitions and type declarations are the A = 𝕍 instances. There is no constraint kind: an assumed equation is a HOLE at the equation's prop — a declaration at (a₀ ≡ a₁ ∈ A), read back through el-reflect and closed by INSTANTIATION with ⋆ (see DEFINITIONAL AND OPEN SIGNATURES)

Σ ::= ε
    | Σ (Γ ⊦ x ≔ a : A)     # definition
    | Σ (Γ ⊦ x : A)         # declaration (a HOLE — no definiens)

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

e˲, t˲, p˲ ::= · | t˲, t

term — ONE sort: the type and element grammars of earlier presentations are merged. A term is a TYPE when it is typed at 𝕍. DISPLAY CONVENTION: the metavariables T, A, B, C range over terms standing in type position, t, a, b, e over terms in element position — one grammar, two reading aids. The formers 𝟘 𝟙 ℕ → × ⊎ / (and the QIIT sorts and ν) are typed BOTH at 𝕌 (as codes) and at 𝕍 (as types): at 𝕌 by their code-* rules, whence at 𝕍 by CUMULATIVITY (code-lift — El is retired), and at 𝕍 with LARGE components by their ty-* rules. The Ω-formers ≡ and ∥·∥ are likewise typed both at Ω (as props) and at 𝕍 (as types), by PROP-CUMULATIVITY (prop-lift — Prf is retired: a proposition IS its type of proofs).

t, T ::= x [e˲]      # signature reference
    | ☐ᵢ             # i-th element in the typing context
    | 𝕌              # predicative universe (a type; not a code)
    | Ω              # universe of mere propositions (a type; not a code)
    | 𝕍              # THE TOP UNIVERSE — the one term with NO typing
                     #   rule: it stands only in the type slot of
                     #   judgements and in the ∈-slot of ≡ — see THE
                     #   TOP UNIVERSE note in the type rules
    | 𝟘              # empty type — code and type
    | 𝟙              # unit type — code and type
    | ℕ              # naturals — code and type
    | t → t          # dependent product (Π) — code and type
    | t × t          # dependent sum (Σ) — code and type
    | t ⊎ t          # non-dependent sum (disjoint union) — code and type
    | t / t          # quotient by an Ω-valued relation — code and type
    | λ 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)
    | t ≡ t ∈ T      # equality PROPOSITION — an Ω-element, and by
                     #   prop-lift a type; T an arbitrary type OR 𝕍
                     #   itself, so equality props exist at large
                     #   types and type equality is a proposition
                     #   (see the Ω block)
    | 𝟘-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 —
                     #   with Prf retired, the ONE mediator between
                     #   types and props, one-directional; a prop and
                     #   (by prop-lift) a type
    | ⋆              # the canonical proof of a true proposition
    | 𝒮.𝕤 ē          # sort 𝕤 of a QIIT signature 𝒮 at index spine ē —
                     #   a type, and a code when 𝒮 is SMALL; 𝒮 is
                     #   carried in the term, so QIIT equality is
                     #   structural (see "Quotient inductive-inductive
                     #   types")
    | 𝒮.𝕔 θ          # 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
    | ν 𝔽            # coinductive type at polynomial 𝔽 — a type and a
                     #   code (every polynomial is small); 𝔽 is carried
                     #   in the term, so ν-equality is structural (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 : 𝕍` and
  `Γ ▷ A ⊦ B : 𝕍`. 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).

• EQUALITY. There is ONE equality: the proposition (a₀ ≡ a₁ ∈ A). The judgemental spelling is DERIVED NOTATION —

    Γ ⊦ a₀ ≐ a₁ : A    ≜    Γ ⊦ ⋆ : (a₀ ≡ a₁ ∈ A)

— with A ranging over types AND 𝕍 (A = 𝕍 is TYPE equality). It is not a judgement form: its presuppositions are those of the unfolding, which close over code-eq's premises — exactly the two typings the retired form presupposed. The remaining equality spellings are META-DEFINITIONS over it:

    Γ₀ ≐ Γ₁ ctx             pointwise: ε ≐ ε, and
                            Γ₀ ▷ A₀ ≐ Γ₁ ▷ A₁ iff Γ₀ ≐ Γ₁ ctx and
                            Γ₁ ⊦ A₀ ≐ A₁ : 𝕍 (the old ctx-ext-cong,
                            now the defining clause)
    σ₀ ≐ σ₁ : Γ ⇒ Δ         EXTENSIONAL: Γ ⊦ ☐ᵢ[σ₀] ≐ ☐ᵢ[σ₁] : Δ‖ᵢ[σ₁]
                            for every i < |Δ| — the substitution
                            calculus's own equations (assoc, the id
                            laws, wk-ext, eta, ...) are then
                            META-LEMMAS, by the var-sub-* clauses
    e˲₀ ≐ e˲₁ : Γ ⇒ Δ norm  pointwise (sub-norm-ext-cong defining)
    Γ ⊦ Δ₀ ≐ Δ₁ tel         pointwise (tel-ext-cong defining)
    Γ ⊦ ē₀ ≐ ē₁ : Δ         pointwise (sp-ext-cong defining)

The EQUIVALENCE structure: for the ≐-notation it is three RULES, stated once here —

    Γ ⊦ a : A         Γ ⊦ a₀ ≐ a₁ : A       Γ ⊦ a₀ ≐ a₁ : A   Γ ⊦ a₁ ≐ a₂ : A
    ---------(el-refl) ---------------(el-sym) --------------------------------(el-trans, via a₁)
    Γ ⊦ a ≐ a : A     Γ ⊦ a₁ ≐ a₀ : A       Γ ⊦ a₀ ≐ a₂ : A

(transitivity's middle subject a₁, with its typing, is an input; ty-refl/-sym/-trans of earlier presentations are the A = 𝕍 instances). For the meta-defined spellings, refl/sym/trans are META-LEMMAS, pointwise from these (the former ctx-/sub-/sub-norm-/ tel-/sp- refl/sym/trans instances). Pointwise equality of 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 ≐-notation and additionally marks it as a computation step, oriented left to right. Its presuppositions are those of the underlying ≐ spelling.

• NAMES. Every rule carries a canonical name on its inference line, following one homogeneous scheme — <class>-<former>-<kind> — where the class prefix names the judgement class (ctx, sub, sub-norm, el, tel, sp, poly), EXCEPT that within the element class the prefix records the conclusion's universe: ty- for conclusions at 𝕍 (types), code- for conclusions at 𝕌 (codes), el- otherwise. (The ty judgement class is dissolved into el at 𝕍; the prefix survives as a naming convention precisely so that rule names are stable across the dissolution — see DISSOLVED NAMES at the end.) 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
  e˲ : Γ ⇒ Δ norm              Γ ctx;  Δ ctx
  Γ ⊦ A : 𝕍                   Γ ctx          (the A = 𝕍 instance)
  Γ ⊦ a : A                    Γ ⊦ A : 𝕍     (A ≠ 𝕍)
  # The typing judgement's presupposition is TWO-CASE, by the two rows
  # above: at A = 𝕍 only Γ ctx is presupposed — 𝕍 is the ONE term
  # that stands in type position without itself being typed (it has
  # no typing rule; see THE TOP UNIVERSE) — and at A ≠ 𝕍 the type's
  # own 𝕍-typing is. The rows are instances of one judgement form,
  # not separate forms. There are NO equality rows: Γ ⊦ a₀ ≐ a₁ : A
  # is derived notation for a ⋆-typing (its presuppositions unfold to
  # the two typings), and the other ≐-spellings are meta-definitions
  # — see EQUALITY in the conventions.
  Γ ⊦ Δ tel                    Γ ctx
  Γ ⊦ ē : Δ                    Γ ⊦ Δ tel
  Γ ⊦ Φ qctx                   Γ ctx        (qiit-context)
  Γ ; Φ ⊦ 𝔄 qty                Γ ⊦ Φ qctx   (qiit-type)
  Γ ; Φ ⊦ 𝕥 : 𝔄                Γ ; Φ ⊦ 𝔄 qty (qiit-term)
  Γ ⊦ ς : Φ₀ ⇒ Φ₁              Γ ⊦ Φ₀ qctx;  Γ ⊦ Φ₁ qctx   (qiit-substitution)
  Γ ⊦ 𝒮 qsig                   Γ ctx        (QIIT signature; ≜ Γ ⊦ 𝒮 qctx)
  Γ ⊦ C̄ : 𝒮 mot                Γ ⊦ 𝒮 qsig   (motive family)
  Γ ⊦ ℰ : 𝒮 dalg               Γ ⊦ 𝒮 qsig   (displayed algebra, ℰ = C̄ ; m̄)
  Γ ⊦ ℰ : 𝒮 eprob              Γ ⊦ ℰ : 𝒮 dalg   (elimination problem)
  Γ ⊦ φ : C̄ sect               Γ ⊦ C̄ : 𝒮 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 : 𝕍, so a premise stated under Γ ▷ A carries A's well-formedness with it (and likewise for iterated extensions). Because Γ ⊦ 𝕍 : 𝕍 is not derivable, Γ ▷ 𝕍 is ill-formed: contexts cannot bind a variable ranging over all types — a genuine 𝕍-typing derivation is demanded wherever a term is CONSUMED as a type (ctx-ext, Π/Σ components, telescope entries, motives), and only the type SLOT of judgements admits 𝕍 itself.

Rules (sig)

ε sig

Σ Γ ⊦ a : A
x ∉ Σ

Σ (Γ ⊦ x ≔ a : A) sig               #   the former sig-ty-def

Σ Γ ⊦ A : 𝕍
x ∉ Σ

Σ (Γ ⊦ x : A) sig

Σ Γ ctx
x ∉ Σ

Σ (Γ ⊦ x : 𝕍) sig                   #   hole) is NOT a sig-decl
                                    #   instance — 𝕍 admits no
                                    #   Σ Γ ⊦ 𝕍 : 𝕍 premise, so the
                                    #   two-case presupposition
                                    #   surfaces as a second rule,
                                    #   the one place it does

DEFINITIONAL AND OPEN SIGNATURES

A signature is DEFINITIONAL when every entry is a definition (sig-def). A DECLARATION makes it OPEN: a hole — a name with a type and no definiens, whose references x[e˲] are STUCK (el-sig-decl below; deliberately no -beta). Type holes are the A = 𝕍 instances. An assumed EQUATION is a hole at the equation's prop — an entry (Γ ⊦ h : (a₀ ≡ a₁ ∈ A)), A = 𝕍 for a type equation — whose reference h[e˲] yields the instantiated equation by el-reflect: what the retired constraint kind provided through its own rules (sig-eq/el-sig-eq) is one el-reflect away from an ordinary declaration, so the kind is gone. Open signatures are the working states of an elaboration run (docs/NovaElaboration.txt): the declarations 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 (the one admissible principle next); every judgement derived over the open signature holds over each refinement. The class may be EMPTY (a hole at ∥𝟘∥, or at (Z ≡ S Z ∈ ℕ)): judgements under unsatisfiable assumptions carry no absolute content — which is why acceptance demands a definitional signature and nothing weaker.

The refinement principle is a META-THEOREM (by induction on derivations), not a rule of the theory — the workflow it justifies 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˲]. The A = 𝕍 instance covers type declarations, filled by Σ Γ ⊦ T : 𝕍. 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[e˲] ≜ t[e˲].

DISCHARGING an equation obligation is the prop instance: the hole h : (a₀ ≡ a₁ ∈ A) fills with ⋆ exactly when the equation is derivable in its prefix (el-eq-i), the same condition the retired DISCHARGE meta-theorem demanded of a constraint — one open-entry kind, one closing move.

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

Rules (ctx)

ε ctx

Γ ⊦ A : 𝕍

Γ ▷ A ctx

Γ₀ ≐ Γ₁ ctx
Γ₁ ⊦ A₀ ≐ A₁ : 𝕍

Γ₀ ▷ A₀ ≐ Γ₁ ▷ A₁ ctx                  #   pointwise meta-notation
                                       #   (EQUALITY, conventions)

Rules (ctx substitution)

SUBSTITUTION EQUALITY IS THE EXTENSIONAL META-NOTATION

(EQUALITY, conventions): σ₀ ≐ σ₁ : Γ ⇒ Δ says the variable images agree. The equations of the calculus below (sub-empty-unique, sub-id-empty, sub-eta, sub-id-pre/-post, sub-assoc, sub-wk-ext, sub-empty-comp, sub-ext-post, sub-ext-unique, sub-comp-cong, sub-ext-cong, and the sub-eq-coe-* transports) are therefore META-LEMMAS, established by the var-sub-* clauses and el-sub-comp/el-sub-id — retained here, statements and names unchanged, because the kernel and the docs cite them as facts.

Γ ctx

· : Γ ⇒ ε

σ : Γ ⇒ ε

σ ≐ · : Γ ⇒ ε

σ : Γ₀ ⇒ Γ₁
Γ₀ ⊦ t : A[σ]

(σ, t) : Γ₀ ⇒ Γ₁ ▷ A

σ : Γ₀ ⇒ Γ₁
τ : Γ₁ ⇒ Γ₂

τ ∘ σ : Γ₀ ⇒ Γ₂

Γ ctx

id : Γ ⇒ Γ

Γ ⊦ A : 𝕍

↑ : Γ ▷ A ⇒ Γ

id ≐ · : ε ⇒ ε

Γ ⊦ A : 𝕍

↑, ☐₀ ≐ id : Γ ▷ A ⇒ Γ ▷ A

σ : Γ₀ ⇒ Γ₁

σ ∘ id ≐ σ : Γ₀ ⇒ Γ₁

σ : Γ₀ ⇒ Γ₁

id ∘ σ ≐ σ : Γ₀ ⇒ Γ₁

σ₁₀ : Γ₁ ⇒ Γ₀
σ₂₁ : Γ₂ ⇒ Γ₁
σ₃₂ : Γ₃ ⇒ Γ₂

σ₁₀ ∘ (σ₂₁ ∘ σ₃₂) ≐ (σ₁₀ ∘ σ₂₁) ∘ σ₃₂ : Γ₃ ⇒ Γ₀

σ : Γ₀ ⇒ Γ₁
Γ₀ ⊦ t : A[σ]

↑ ∘ (σ, t) ≐ σ : Γ₀ ⇒ Γ₁

σ : Γ₀ ⇒ ε

· ∘ σ ≐ · : Γ₀ ⇒ ε

τ : Γ₀ ⇒ Γ₁
σ : Γ₁ ⇒ Γ₂
Γ₁ ⊦ t : A[σ]

(σ, t) ∘ τ ≐ (σ ∘ τ, t[τ]) : Γ₀ ⇒ Γ₂ ▷ A

σ : Γ₀ ⇒ Γ₁
Γ₁ ⊦ A : 𝕍

σ⁺ ≜ (σ ∘ ↑, ☐₀) : Γ₀ ▷ A[σ] ⇒ Γ₁ ▷ A

σ : Γ₀ ⇒ Γ₁
Γ₀ ⊦ t : A[σ]
τ : Γ₀ ⇒ Γ₁ ▷ A
↑ ∘ τ ≐ σ : Γ₀ ⇒ Γ₁
Γ₀ ⊦ ☐₀[τ] ≐ t : A[↑ ∘ τ]

(σ, t) ≐ τ : Γ₀ ⇒ Γ₁ ▷ A
∎ (=>) τ ≐ id ∘ τ ≐ (↑, ☐₀) ∘ τ ≐ ↑ ∘ τ, ☐₀[τ] ≐ σ, t
  (<=)
      σ ≐ ↑ ∘ (σ, t) ≐ ↑ ∘ τ
      t ≐ ☐₀[σ, t] ≐ ☐₀[τ] ∎

σ₀ ≐ σ₁ : Γ₀ ⇒ Γ₁
τ₀ ≐ τ₁ : Γ₁ ⇒ Γ₂

τ₀ ∘ σ₀ ≐ τ₁ ∘ σ₁ : Γ₀ ⇒ Γ₂

σ₀ ≐ σ₁ : Γ₀ ⇒ Γ₁
Γ₀ ⊦ t₀ ≐ t₁ : A[σ₁]

(σ₀, t₀) ≐ (σ₁, t₁) : Γ₀ ⇒ Γ₁ ▷ A

Γ₀ ≐ Γ₁ ctx
σ : Γ₀ ⇒ Δ

σ : Γ₁ ⇒ Δ

Δ₀ ≐ Δ₁ ctx
σ : Γ ⇒ Δ₀

σ : Γ ⇒ Δ₁

Γ ≐ Γ' ctx
σ ≐ τ : Γ ⇒ Δ

σ ≐ τ : Γ' ⇒ Δ

Δ ≐ Δ' ctx
σ ≐ τ : Γ ⇒ Δ

σ ≐ τ : Γ ⇒ Δ'

Rules (normal substitution)

Γ ctx

· : Γ ⇒ ε norm

e˲ : Γ ⇒ ε norm

e˲ ≐ · : Γ ⇒ ε norm

e˲ : Γ₀ ⇒ Γ₁ norm
Γ₀ ⊦ t : A[e˲]

(e˲, t) : Γ₀ ⇒ Γ₁ ▷ A norm

e˲₀ ≐ e˲₁ : Γ₀ ⇒ Γ₁ norm
Γ₀ ⊦ t₀ ≐ t₁ : A[e˲₁]

(e˲₀, t₀) ≐ (e˲₁, t₁) : Γ₀ ⇒ Γ₁ ▷ A norm                       #   pointwise meta-notation

e˲ : Γ₀ ⇒ Γ₁ norm

e˲ : Γ₀ ⇒ Γ₁

e˲ : Γ₀ ⇒ Γ₁ norm
σ : Δ ⇒ Γ₀

e˲ ∘ σ : Δ ⇒ Γ₁ norm
    · ∘ σ ≜ ·
    (e˲, t) ∘ σ ≜ (e˲ ∘ σ, t[σ])

e˲₀ ≐ e˲₁ : Γ₀ ⇒ Γ₁ norm
σ : Δ ⇒ Γ₀

e˲₀ ∘ σ ≐ e˲₁ ∘ σ : Δ ⇒ Γ₁ norm

Γ₀ ≐ Γ₁ ctx
e˲ : Γ₀ ⇒ Δ norm

e˲ : Γ₁ ⇒ Δ norm

Δ₀ ≐ Δ₁ ctx
e˲ : Γ ⇒ Δ₀ norm

e˲ : Γ ⇒ Δ₁ norm

Γ ≐ Γ' ctx
e˲ ≐ t˲ : Γ ⇒ Δ norm

e˲ ≐ t˲ : Γ' ⇒ Δ norm

Δ ≐ Δ' ctx
e˲ ≐ t˲ : Γ ⇒ Δ norm

e˲ ≐ t˲ : Γ ⇒ Δ' norm

Rules (types — typing at 𝕍)

THE TOP UNIVERSE 𝕍. The types are the terms typed at 𝕍; the rules of this section are the old type-formation and type-equality rules, re-read as element rules whose conclusions sit at 𝕍. The design of 𝕍 in full:

• 𝕍 is an ordinary TERM FORMER with NO typing rule: no Γ ⊦ 𝕍 : 𝕍 (Girard), no code in 𝕌, no level tower above it. It stands only in the type slot of the judgements (licensed by the two-case presupposition row) and in the ∈-slot of ≡ (code-eq's endpoints are typing judgements, so their slot is a judgement slot too).
• Every EXCLUSION is by absence of a derivation, not by grammar:

   Γ ▷ 𝕍 (type variables in contexts), 𝕍-domain and 𝕍-codomain

Π-types (quantification over all types), ∥𝕍∥, telescope entries and motives at 𝕍 — each would need Γ ⊦ 𝕍 : 𝕍 through its premises, and 𝕍 has no typing at all. The theory's stratification (𝕌 predicative, Ω impredicative-but-irrelevant, the top unnamed-no-longer) is exactly what it was.

• 𝕍[σ] ≜ 𝕍 is a META-CLAUSE of the substitution action, not a judgemental rule — 𝕍 is not typed, so an equation about it has no judgemental home, and needs none: 𝕍 occurs only in judgement slots, where indices are computed by the meta-operations (the

   Γ‖ₙ precedent).

• The GENERAL rules of the old type judgement are now instances of the element rules at A = 𝕍 and are not restated: ty-sub, ty-sub-id, ty-sub-comp are el-sub, el-sub-id, el-sub-comp; ty-coe-ctx and ty-eq-coe-ctx are el-coe-ctx and el-eq-coe-ctx; ty-sub-cong(-fix) is el-sub-cong(-fix); ty-sig-var, ty-sig-beta, ty-sig-decl and ty-sub-sig-var are el-sig-var, el-sig-beta, el-sig-decl and el-sub-sig-var at an entry whose A is 𝕍 (their conclusion indices A[e˲], A[e˲ ∘ σ] compute to 𝕍 by the meta-clause). The FORMER-SPECIFIC rules below all remain: a conclusion at 𝕍 with component premises at 𝕍 is not an instance of its 𝕌-code sibling (whose components sit at 𝕌), so both members of each pair survive the merge — though the 𝕌-instances now also reach 𝕍 through code-lift.
• ty-zero-elim (type equality from absurdity) is DERIVABLE and retired: from Γ ⊦ t : 𝟘, el-zero-e at the type (A ≡ B ∈ 𝕍) — code-eq admits 𝕍, see the Ω block — gives 𝟘-elim t : (A ≡ B ∈ 𝕍), and el-reflect concludes Γ ⊦ A ≐ B : 𝕍. (The same derivation gives a ≐ b : C at ANY type under absurdity — absurdity collapses every equation, type equations included.)
• NAMING. Rules concluding at 𝕍 keep their ty- prefix (see NAMES in the conventions): the prefix now reads "typing at 𝕍", as code- reads "typing at 𝕌".

Γ ctx

Γ ⊦ 𝟘 : 𝕍   (ty-zero)   # ADMISSIBLE — code-lift at code-zero

Γ ⊦ 𝟙 : 𝕍   (ty-one)    # ADMISSIBLE — code-lift at code-one

Γ ⊦ ℕ : 𝕍   (ty-nat)    # ADMISSIBLE — code-lift at code-nat

Γ ⊦ 𝕌 : 𝕍

Γ ⊦ Ω : 𝕍

Γ ⊦ A : 𝕍
Γ ▷ A ⊦ B : 𝕍

Γ ⊦ A → B : 𝕍

Γ ⊦ A : 𝕍
Γ ▷ A ⊦ B : 𝕍

Γ ⊦ A × B : 𝕍

Γ ⊦ A : 𝕍
Γ ⊦ B : 𝕍

Γ ⊦ A ⊎ B : 𝕍

CUMULATIVITY

El is RETIRED: every element of 𝕌 IS a type, by the lift below, and its equality lifts and restricts. The three rules are the invisible remnant of the retired decoding former — code-lift is ty-el, code-lift-eq is ty-el-cong, code-restrict is ty-el-inj — and with nothing left to decode, the ty-el-* computation rules are VACUOUS (each equation's two sides are now one term). code-restrict is MANDATORY, not optional: it is what keeps the equality props (a ≡ b ∈ 𝕌) and (a ≡ b ∈ 𝕍) equi-true at codes (whence ≐-equal by code-prop-eq), so facts established at 𝕍 descend to 𝕌. SEMANTICS: the small codes are a sub-collection of the large ones (NovaModel's `el` embedding, now an inclusion); the lift is that inclusion, and type equality restricted to 𝕌's image is 𝕌's own — exactly code-restrict. Consequently ty-zero, ty-one and ty-nat above are ADMISSIBLE (code-lift at code-zero/-one/-nat), retained in the grouped display; ty-pi/-sigma/-sum/-quot remain primitive for their LARGE instances, their small instances now also arriving via code-lift — coherently, both routes conclude the same judgement.

Γ ⊦ a : 𝕌

Γ ⊦ a : 𝕍

Γ ⊦ a₀ ≐ a₁ : 𝕌

Γ ⊦ a₀ ≐ a₁ : 𝕍

Γ ⊦ a₀ : 𝕌
Γ ⊦ a₁ : 𝕌
Γ ⊦ a₀ ≐ a₁ : 𝕍

Γ ⊦ a₀ ≐ a₁ : 𝕌

PROP-CUMULATIVITY

Prf is RETIRED: a proposition IS its type of proofs, by the lift below, and its equality lifts and restricts. prop-lift is ty-prf with the wrapper deleted; prop-restrict is MANDATORY for the same reason code-restrict is (it keeps the props (p ≡ q ∈ Ω) and (p ≡ q ∈ 𝕍) equi-true at props, so the ∈-slot stays well-defined). THE ASYMMETRY with the 𝕌 triple, stated plainly: code-lift-eq imports nothing (𝕌's equality is the restriction of 𝕍's structural equality on the nose), but prop-lift-eq imports PROPOSITIONAL EXTENSIONALITY into 𝕍 — on the prop cluster, type equality is mere equivalence (code-prop-eq). Type equality at 𝕍 is thereafter MIXED: structural on the code cluster, extensional on the prop cluster. prop-lift-eq is PRIMITIVE, not an el-sub-cong instance (the master congruence at ☐₀ over Γ ▷ Ω concludes at Ω, not 𝕍 — nothing else lifts the coarse equality). CROSS-CLUSTER equations are underivable by absence: ∥𝟙∥ ≐ 𝟙 : 𝕍 has no derivation — prop-restrict needs both sides at Ω (𝟙 is not: Ω's only formers are ≡ and ∥·∥), code-restrict needs both at 𝕌 (∥𝟙∥ is not: there is no Ω-code in 𝕌) — and the model refutes them (disjoint summands, see SEMANTICS below). Both are contractible; the theory keeps them intensionally distinct, exactly as A / R vs A / R⁺. SEMANTICS: the top universe's codes gain a PROP summand, disjoint from the structural codes, whose constructor argument is QUOTIENTED by iff — 𝕍's PER is constructor-structural on one summand and extensional on the other; no-confusion BETWEEN the summands is the meta-property that refutes cross-cluster equalities. This is the boundary the retired Prf used to spell as a single non-injective former; retiring it moves the carve-out into 𝕍's own equality.

Γ ⊦ p : Ω

Γ ⊦ p : 𝕍

Γ ⊦ p₀ ≐ p₁ : Ω

Γ ⊦ p₀ ≐ p₁ : 𝕍

Γ ⊦ p₀ : Ω
Γ ⊦ p₁ : Ω
Γ ⊦ p₀ ≐ p₁ : 𝕍

Γ ⊦ p₀ ≐ p₁ : Ω

Γ ⊦ A : 𝕍
Γ ▷ A ▷ A[↑] ⊦ R : Ω

Γ ⊦ A / R : 𝕍

Signature references at type entries need no rules of their own: el-sig-var, el-sig-beta and el-sig-decl (in the element rules) cover the A = 𝕍 entries — e.g. for (Γ ⊦ x ≔ A : 𝕍) ∈ Σ, el-sig-var concludes Σ Δ ⊦ x[e˲] : 𝕍[e˲], and the index computes to 𝕍 by the meta-clause. As before, a type declaration types its references but never unfolds them (no -beta — the reference is stuck); an assumed type equation is a hole at (A₀ ≡ A₁ ∈ 𝕍), read back through el-reflect.

Substitution action: one meta-level induction on the (single) term sort defines t[σ]; the ≜-rules below assert its 𝕍-typings, their code-* siblings (el-sub-code-*, el-sub-atoms) its 𝕌-typings, and the Ω-side rules (el-sub-eq, el-sub-squash) its Ω-typings, whence 𝕍-typings by prop-lift (ty-prf-sub is dissolved with Prf) — one action, three families of well-typedness facts. The general rules (action typing, id, comp) are el-sub, el-sub-id, el-sub-comp at A = 𝕍 — see THE TOP UNIVERSE note. There is no ≜-line for 𝕍 itself: 𝕍[σ] ≜ 𝕍 is the meta-clause.

σ : Γ₀ ⇒ Γ₁

Γ₀ ⊦ 𝟘[σ] ≜ 𝟘 : 𝕍
Γ₀ ⊦ 𝟙[σ] ≜ 𝟙 : 𝕍
Γ₀ ⊦ ℕ[σ] ≜ ℕ : 𝕍
Γ₀ ⊦ 𝕌[σ] ≜ 𝕌 : 𝕍
Γ₀ ⊦ Ω[σ] ≜ Ω : 𝕍

Γ₁ ⊦ A : 𝕍
Γ₁ ▷ A ⊦ B : 𝕍
σ : Γ₀ ⇒ Γ₁

Γ₀ ⊦ (A → B)[σ] ≜ A[σ] → B[σ⁺] : 𝕍

Γ₁ ⊦ A : 𝕍
Γ₁ ▷ A ⊦ B : 𝕍
σ : Γ₀ ⇒ Γ₁

Γ₀ ⊦ (A × B)[σ] ≜ A[σ] × B[σ⁺] : 𝕍

Γ₁ ⊦ A : 𝕍
Γ₁ ⊦ B : 𝕍
σ : Γ₀ ⇒ Γ₁

Γ₀ ⊦ (A ⊎ B)[σ] ≜ A[σ] ⊎ B[σ] : 𝕍

Γ₁ ⊦ A : 𝕍
Γ₁ ▷ A ▷ A[↑] ⊦ R : Ω
σ : Γ₀ ⇒ Γ₁

Γ₀ ⊦ (A / R)[σ] ≜ A[σ] / R[σ⁺⁺] : 𝕍

(ty-sub-sig-var is el-sub-sig-var at a type entry; ty-zero-elim is derivable; ty-coe-ctx, ty-eq-coe-ctx, ty-sub-cong and ty-sub-cong-fix are el-coe-ctx, el-eq-coe-ctx, el-sub-cong and el-sub-cong-fix at A = 𝕍 — see THE TOP UNIVERSE note. The former-specific congruences follow.)

The four with a 𝕍-typed component (ty-pi-cong, ty-sigma-cong, ty-sum-cong, ty-quot-cong) are PRIMITIVE, and irreducibly so: the master congruence scheme (see the element congruence block) derives a former's congruence either as a substitution instance — needing a context entry at the slot's type, and nothing binds at 𝕍 — or from the former's η — and 𝕍, like 𝕌, deliberately has no eliminator. They are the downward duals of the ty-*-inj block: together the two families ARE the commitment that type equality is equality of structural codes — on the CODE cluster; the prop cluster's congruence is prop-lift-eq (PROP-CUMULATIVITY), which imports code-prop-eq's extensional equality wholesale, and the retired decoding congruences ty-el-cong and ty-prf-cong are exactly code-lift-eq and prop-lift-eq.

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ▷ A₁ ⊦ B₀ ≐ B₁ : 𝕍

Γ ⊦ A₀ → B₀ ≐ A₁ → B₁ : 𝕍

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ▷ A₁ ⊦ B₀ ≐ B₁ : 𝕍

Γ ⊦ A₀ × B₀ ≐ A₁ × B₁ : 𝕍

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ⊦ B₀ ≐ B₁ : 𝕍

Γ ⊦ A₀ ⊎ B₀ ≐ A₁ ⊎ B₁ : 𝕍

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ▷ A₁ ▷ A₁[↑] ⊦ R₀ ≐ R₁ : Ω

Γ ⊦ A₀ / R₀ ≐ A₁ / R₁ : 𝕍

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 : ((𝟙 → 𝟘) ≡ (ℕ → 𝟘) ∈ 𝕌) 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. (The PROP summand is the deliberate exception: its equality is extensional, and it has no injectivity — see PROP-CUMULATIVITY and the prop-cluster note below.) 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.
• The PROP cluster (∥-∥ and ≡, lifted by prop-lift) has NO injectivity rules: Ω is the anti-structural universe, compared by inhabitation alone (see the Ω block in the element rules) — with Prf retired this is a property of 𝕍's own equality on the prop summand, not of a wrapper. 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₀ : 𝕍
Γ ▷ A₁ ⊦ B₁ : 𝕍
Γ ⊦ A₀ → B₀ ≐ A₁ → B₁ : 𝕍

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ▷ A₁ ⊦ B₀ ≐ B₁ : 𝕍

Γ ▷ A₀ ⊦ B₀ : 𝕍
Γ ▷ A₁ ⊦ B₁ : 𝕍
Γ ⊦ A₀ × B₀ ≐ A₁ × B₁ : 𝕍

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ▷ A₁ ⊦ B₀ ≐ B₁ : 𝕍

Γ ⊦ A₀ ⊎ B₀ ≐ A₁ ⊎ B₁ : 𝕍

Γ ⊦ A₀ ≐ A₁ : 𝕍                              #   components over Γ
Γ ⊦ B₀ ≐ B₁ : 𝕍

Γ ▷ A₀ ▷ A₀[↑] ⊦ R₀ : Ω
Γ ▷ A₁ ▷ A₁[↑] ⊦ R₁ : Ω
Γ ⊦ A₀ / R₀ ≐ A₁ / R₁ : 𝕍

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ▷ A₁ ▷ A₁[↑] ⊦ R₀ ≐ R₁ : Ω

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 𝕌.

Γ ▷ a₀ ⊦ b₀ : 𝕌
Γ ▷ a₁ ⊦ b₁ : 𝕌
Γ ⊦ a₀ → b₀ ≐ a₁ → b₁ : 𝕌

Γ ⊦ a₀ ≐ a₁ : 𝕌
Γ ▷ a₁ ⊦ b₀ ≐ b₁ : 𝕌

Γ ▷ a₀ ⊦ b₀ : 𝕌
Γ ▷ a₁ ⊦ b₁ : 𝕌
Γ ⊦ a₀ × b₀ ≐ a₁ × b₁ : 𝕌

Γ ⊦ a₀ ≐ a₁ : 𝕌
Γ ▷ a₁ ⊦ b₀ ≐ b₁ : 𝕌

Γ ⊦ a₀ ⊎ b₀ ≐ a₁ ⊎ b₁ : 𝕌

Γ ⊦ a₀ ≐ a₁ : 𝕌
Γ ⊦ b₀ ≐ b₁ : 𝕌

Γ ▷ a₀ ▷ a₀[↑] ⊦ r₀ : Ω
Γ ▷ a₁ ▷ a₁[↑] ⊦ r₁ : Ω
Γ ⊦ a₀ / r₀ ≐ a₁ / r₁ : 𝕌

Γ ⊦ a₀ ≐ a₁ : 𝕌
Γ ▷ a₁ ▷ a₁[↑] ⊦ r₀ ≐ r₁ : Ω

Rules (tel)

Γ ctx

Γ ⊦ ε tel

Γ ⊦ A : 𝕍
Γ ▷ A ⊦ Δ tel

Γ ⊦ A ◁ Δ tel

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ▷ A₁ ⊦ Δ₀ ≐ Δ₁ tel

Γ ⊦ A₀ ◁ Δ₀ ≐ A₁ ◁ Δ₁ tel                      #   pointwise meta-notation

Γ₁ ⊦ Δ tel
σ : Γ₀ ⇒ Γ₁

Γ₀ ⊦ Δ[σ] tel

σ : Γ₀ ⇒ Γ₁

Γ₀ ⊦ ε[σ] ≜ ε tel

Γ₁ ⊦ A : 𝕍
Γ₁ ▷ A ⊦ Δ tel
σ : Γ₀ ⇒ Γ₁

Γ₀ ⊦ (A ◁ Δ)[σ] ≜ A[σ] ◁ Δ[σ⁺] tel

Γ₀ ≐ Γ₁ ctx
Γ₀ ⊦ Δ tel

Γ₁ ⊦ Δ tel

Γ₀ ≐ Γ₁ ctx
Γ₀ ⊦ Δ₀ ≐ Δ₁ tel

Γ₁ ⊦ Δ₀ ≐ Δ₁ tel

Γ ⊦ Δ₀ ≐ Δ₁ tel
σ₀ ≐ σ₁ : Ξ ⇒ Γ

Ξ ⊦ Δ₀[σ₀] ≐ Δ₁[σ₁] tel

Rules (elem)

Γ ctx

Γ ⊦ ☐ₙ : Γ‖ₙ                # derivation of ☐ₙ₋₁, ☐ₙ₋₂, ... is required first.

Universe codes.

Γ ctx

Γ ⊦ 𝟘 : 𝕌

Γ ⊦ 𝟙 : 𝕌

Γ ⊦ ℕ : 𝕌

Γ ⊦ A : 𝕌
Γ ▷ A ⊦ B : 𝕌

Γ ⊦ A → B : 𝕌

Γ ⊦ A : 𝕌
Γ ▷ A ⊦ B : 𝕌

Γ ⊦ A × B : 𝕌

Γ ⊦ A : 𝕌
Γ ⊦ B : 𝕌

Γ ⊦ A ⊎ B : 𝕌

Γ ⊦ A : 𝕌
Γ ▷ A ▷ A[↑] ⊦ R : Ω

Γ ⊦ A / R : 𝕌

𝟘 and 𝟙.

Γ ⊦ A : 𝕍
Γ ⊦ t : 𝟘

Γ ⊦ 𝟘-elim t : A

Γ ⊦ t₀ : 𝟘
Γ ⊦ t₁ : 𝟘

Γ ⊦ t₀ ≐ t₁ : 𝟘

Γ ctx

Γ ⊦ () : 𝟙

Γ ⊦ t₀ : 𝟙
Γ ⊦ t₁ : 𝟙

Γ ⊦ t₀ ≐ t₁ : 𝟙

ℕ.

Γ ctx

Γ ⊦ Z : ℕ

Γ ⊦ t : ℕ

Γ ⊦ S t : ℕ

Γ ▷ ℕ ⊦ A : 𝕍
Γ ⊦ z : A[id, Z]
Γ ▷ ℕ ▷ A ⊦ s : A[↑ ∘ ↑, S ☐₁]
Γ ⊦ t : ℕ

Γ ⊦ ℕ-elim z s t : A[id, t]

Γ ▷ ℕ ⊦ A : 𝕍
Γ ⊦ z : A[id, Z]
Γ ▷ ℕ ▷ A ⊦ s : A[↑ ∘ ↑, S ☐₁]

Γ ⊦ ℕ-elim z s Z ≜ z : A[id, Z]

Γ ▷ ℕ ⊦ A : 𝕍
Γ ⊦ 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 : 𝕍
Γ ▷ ℕ ⊦ 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 : ℕ

Γ ⊦ 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 : 𝕍
Γ ⊦ f : A → B
Γ ⊦ e : A

Γ ⊦ f e : B[id, e]

Γ ▷ A ⊦ f : B
Γ ⊦ e : A

Γ ⊦ (λ f) e ≜ f[id, e] : B[id, e]

Uniqueness (η), in the EXTENSIONAL (two-candidate) form every other former's η already takes (el-nat-eta's style): two functions that agree at the generic argument are equal. The classical single- candidate form λ (f[↑] ☐₀) ≐ f is the instance g₀ ≜ λ (g₁[↑] ☐₀), whose premise holds by el-pi-beta; conversely the two-candidate form is NOT derivable from it — the step from "equal at the generic argument" to "equal" is exactly ξ's content, so stating η this way is what makes el-lam-cong (ξ) admissible below. The kernel's FEtaPi final replays exactly this form.

Γ ⊦ g₀ : A → B
Γ ⊦ g₁ : A → B
Γ ▷ A ⊦ g₀[↑] ☐₀ ≐ g₁[↑] ☐₀ : B

Γ ⊦ g₀ ≐ g₁ : 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 proof of its unfolding equation — 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 ▷ (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b : B

Γ ⊦ let a b : B[id, a, ⋆]

Γ ⊦ a : A
Γ ▷ A ▷ (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b : B

Γ ⊦ let a b ≜ b[id, a, ⋆] : B[id, a, ⋆]

Σ.

Γ ▷ A ⊦ B : 𝕍
Γ ⊦ a : A
Γ ⊦ b : B[id, a]

Γ ⊦ (a , b) : A × B

Γ ⊦ t : A × B

Γ ⊦ t .π₁ : A

Γ ⊦ t : A × B

Γ ⊦ t .π₂ : B[id, t .π₁]

Γ ▷ A ⊦ B : 𝕍
Γ ⊦ a : A
Γ ⊦ b : B[id, a]

Γ ⊦ (a, b) .π₁ ≜ a : A

Γ ▷ A ⊦ B : 𝕍
Γ ⊦ 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 : 𝕍
Γ ⊦ a : A

Γ ⊦ inj₁ a : A ⊎ B

Γ ⊦ A : 𝕍
Γ ⊦ b : B

Γ ⊦ inj₂ b : A ⊎ B

Γ ▷ A ⊎ B ⊦ C : 𝕍
Γ ▷ A ⊦ l : C[↑, inj₁ ☐₀]
Γ ▷ B ⊦ r : C[↑, inj₂ ☐₀]
Γ ⊦ t : A ⊎ B

Γ ⊦ ⊎-elim l r t : C[id, t]

Γ ▷ A ⊎ B ⊦ C : 𝕍
Γ ▷ 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 : 𝕍
Γ ▷ 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 : 𝕍
Γ ▷ 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

Γ ⊦ 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, standing directly as the type of its proofs (prop-lift).

Quotients.

Γ ▷ A ▷ A[↑] ⊦ R : Ω
Γ ⊦ a : A

Γ ⊦ class a : A / R

Γ ▷ A ▷ A[↑] ⊦ R : Ω
Γ ⊦ a : A
Γ ⊦ b : A
Γ ⊦ r : R[id, a, b]

Γ ⊦ class a ≐ class b : A / R

Γ ▷ (A / R) ⊦ B : 𝕍
Γ ▷ A ⊦ f : B[↑, class ☐₀]
Γ ▷ A ▷ A[↑] ▷ R ⊦ f[↑ ∘ ↑ ∘ ↑, ☐₂] ≐ f[↑ ∘ ↑ ∘ ↑, ☐₁] : B[↑ ∘ ↑ ∘ ↑, class ☐₂]
Γ ⊦ q : A / R

Γ ⊦ quot-elim f q : B[id, q]

Γ ▷ (A / R) ⊦ B : 𝕍
Γ ▷ A ⊦ f : B[↑, class ☐₀]
Γ ▷ A ▷ A[↑] ▷ R ⊦ f[↑ ∘ ↑ ∘ ↑, ☐₂] ≐ f[↑ ∘ ↑ ∘ ↑, ☐₁] : B[↑ ∘ ↑ ∘ ↑, class ☐₂]
Γ ⊦ a : A

Γ ⊦ quot-elim f (class a) ≜ f[id, a] : B[id, class a]

Γ ▷ (A / R) ⊦ B : 𝕍
Γ ▷ (A / R) ⊦ g : B
Γ ▷ A ⊦ f : B[↑, class ☐₀]
Γ ▷ A ▷ A[↑] ▷ R ⊦ f[↑ ∘ ↑ ∘ ↑, ☐₂] ≐ f[↑ ∘ ↑ ∘ ↑, ☐₁] : B[↑ ∘ ↑ ∘ ↑, class ☐₂]
Γ ▷ A ⊦ g[↑, class ☐₀] ≐ f : B[↑, class ☐₀]
Γ ⊦ q : A / R

Γ ⊦ g[id, q] ≐ quot-elim f q : B[id, q]

el-quot-eq HAS NO CONVERSE at R: the relation slot is arbitrary while ≐ is an equivalence, so class equality is R's equivalence closure and nothing less. What IS recovered from class a ≐ class b — R⁺, exactly, and R itself when R is an equivalence — is EFFECTIVITY, derived in the Ω block below (Consequences for quotients, item 2); it needs Ω as a quot-elim motive, which is why B ranges over TYPES here and Ω is one (ty-prop).

Ω: 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 Ω in 𝕌, no prop is a 𝕌-code, and no Ω analogue of any inj rule. (At 𝕍 the two disciplines COEXIST on disjoint clusters — see PROP-CUMULATIVITY.) (And no code for 𝕍 ANYWHERE — 𝕍 is not typed at all; see THE TOP UNIVERSE.)

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 + prop-lift-eq + el-ty-coe move proofs between iff-equal props UNCHANGED (a true equation is ≐-equal to ∥𝟙∥ at Ω), so every inhabited prop must have literally the same canonical form.
• A is an ARBITRARY type — OR 𝕍 ITSELF: equality props exist at large types (a₀ ≡ a₁ ∈ 𝕌 : Ω), where the old code former could not go, and at the top, (A ≡ B ∈ 𝕍) : Ω — TYPE EQUALITY IS A PROPOSITION. code-eq needs no special case for this: its endpoint premises are typing judgements, whose type slot admits 𝕍 by the presupposition row. With el-eq-i and el-reflect at A = 𝕍, type equality is reflection-complete exactly like element equality — a type-equality hypothesis is an ordinary context entry h : (A ≡ B ∈ 𝕍), and ty-zero-elim of earlier presentations is derivable (see THE TOP UNIVERSE).
• Ω-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 + prop-lift-eq + el-ty-coe move an element between iff-equal props UNCHANGED, which is sound only if those props (as types) have literally the same canonical forms. So a prop never exposes the squashed proofs: its one canonical form is ⋆ (cf. NuPRL's Ax), and el-prf-prop equates all members. Consequently ∥A∥, as a type, does NOT reduce to A, and there is no code-squash-inj: ∥𝟙∥ ≐ (Z ≡ Z ∈ ℕ) : Ω holds by code-prop-eq while the squashees are structurally distinct. Ω adds no computation rules beyond substitution actions (squash's idempotence is ADMISSIBLE, not a

   ≜ — see code-squash-idem); 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 ≔ ∥p × q[↑]∥, p ⊃ q ≔ ∥p → q[↑]∥, ∀ over A ≔ ∥A → p∥, ∃ over A ≔ ∥A × p∥ (props stand directly in the domains and components — prop-lift) — equality (≡) is the one PRIMITIVE prop beside ∥-∥ (squashing it again is redundant by code-squash-idem). 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 : a) ⇛ U ; refl : (x : a) ⇛ El (Id x x) — a small signature, so Id â t u : 𝕌), take

       prf r ≜ Id (ℕ / r̂) (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. (Both steps quotient by a ∨-shaped
       relation, so both need el-quot-eq's witness SUPPLIED, not
       re-derived from the relation's shape —
       docs/NovaElaboration.txt, e-star-quot-wit.)
       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), A → 𝕌 is large, and
       quotient elements cannot store a proposition (coherence
       forces eliminators out of 𝟙/r̂-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, in the ONLY form it can take: quotient equality
        is the equivalence CLOSURE. For R : Ω over Γ ▷ A ▷ A[↑] with
        no assumption whatever,

          class a ≐ class b : A / R  ⟺  R⁺[id, a, b] inhabited

        (⟸) R⁺ is least among the equivalences containing R, and
        (class ☐₁ ≡ class ☐₀ ∈ A / R) is one — el-quot-eq for
        containment, the EQUIVALENCE RULES for the rest.
        (⟹) quot-elim at the constant motive Ω with f ≔ R⁺[id, a, ☐₀]:
        coherence is R⁺ a x ⟺ R⁺ a y under R[id, x, y], by
        code-prop-eq from R⁺'s OWN transitivity and symmetry (this is
        why the motive is the closure and not R: nothing about R is
        needed); then el-quot-beta at class a, congruence along the
        class equation, prop-lift-eq and el-ty-coe carry R⁺'s
        reflexivity proof to b. Both directions stay inside A / R — no
        transport to A / R⁺, which by item 1 is a DIFFERENT type.
        Corollary: where R is an equivalence, R⁺ collapses into it by
        leastness and effectivity holds ON THE NOSE — the familiar
        form, with the hypotheses that make it true.
        The naive form — R itself back, pointwise, for arbitrary R —
        is REFUTABLE, not merely unproved: ≐ is an equivalence at
        every judgement class while ty-quot's relation slot is
        arbitrary, so at R ≔ (S ☐₁ ≡ ☐₀ ∈ ℕ) one has
        class Z ≐ class (S (S Z)) by transitivity, whence a proof
        of (S Z ≡ S (S Z) ∈ ℕ), whence Z ≐ S Z by el-reflect and
        S-injectivity, whence 𝟘. Nothing may read R off a class
        equation; only R⁺.
     3. Equality proofs reflect directly: el-reflect reads
        a₀ ≐ a₁ : B off any s : (a₀ ≡ a₁ ∈ B) — no squash
        apparatus is involved.

• SEMANTICS. In the setoid model a prop, read as a type through prop-lift, denotes 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. THE ∈-𝕍 INSTANCE: (A ≡ B ∈ 𝕍) is true iff ⟦A⟧ and ⟦B⟧ are EQUAL CODES — the model's type equality (with Prf retired this PER is MIXED: structural on the code summand, iff on the prop summand — see PROP-CUMULATIVITY), which is exactly what el-reflect at 𝕍 reads back. This is the one point where the dissolution EXTENDS the theory, and it is sound by the same two-layer construction: prop-truth is defined against the full type system anyway, and code equality of the large universe is available at that stage; the new prop's type of proofs is the same subsingleton as every other, so nothing is storable through it (no Hurkens vector), ≡ still has no 𝕌-code (equality is Ω-valued), and 𝕍 itself remains untyped — the firewall clauses of the impredicativity note are untouched. 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 (⟦A / R⟧ keeps ⟦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. PRECISELY: the coarsened relation must still be an EQUIVALENCE (that is what a setoid is), so it is the equivalence closure of ⟦A⟧'s relation together with R's truth — exactly R⁺'s denotation. "Coarsens by the truth of R at each pair" is the closure's description only when R is already an equivalence containing ≐_A; in general read the closure, and effectivity (item 2 above) is the syntactic counterpart. This does NOT collapse A / R into A / R⁺: type equality is equality of CODES, the quotient code carries its relation, and R, R⁺ are not pointwise equi-inhabited — so ty-quot-inj is untouched, at the price that two quotient types may denote the same setoid while remaining distinct types.

Γ ⊦ A : 𝕍

Γ ⊦ ∥A∥ : Ω

Γ ⊦ a₀ : A
Γ ⊦ a₁ : A

Γ ⊦ (a₀ ≡ a₁ ∈ A) : Ω                 #   equality props exist at large
                                      #   types and at the top: type
                                      #   equality is a proposition

Γ ⊦ p : Ω

Γ ⊦ ∥p∥ ≐ p : Ω                                 #   props. ADMISSIBLE, by
                                                #   code-prop-eq: ∥p∥ and p
                                                #   are equi-inhabited —
                                                #   el-squash-i one way,
                                                #   el-squash-e-prf the
                                                #   other. NOT a ≜: with
                                                #   Prf retired the redex
                                                #   is no longer
                                                #   syntax-directed (its
                                                #   side condition is a
                                                #   typing), so the former
                                                #   code-squash-prf
                                                #   contraction is demoted
                                                #   to this equation —
                                                #   see DISSOLVED NAMES

Γ ⊦ A₀ ≐ A₁ : 𝕍
Γ ⊦ a₀ ≐ a₁ : A₁
Γ ⊦ b₀ ≐ b₁ : A₁

Γ ⊦ (a₀ ≡ b₀ ∈ A₀) ≐ (a₁ ≡ b₁ ∈ A₁) : Ω                      #   code-prop-eq +
                                                             #   el-reflect/el-eq-i
# (the ∈-𝕍 instance fixes A₀ = A₁ = 𝕍 and drops the first premise —
# 𝕍 admits no ≐-judgement of its own, and needs none: the same
# code-prop-eq derivation covers it, with endpoints at 𝕍)

Γ ▷ p ⊦ s : q[↑]
Γ ▷ q ⊦ t : p[↑]

Γ ⊦ p ≐ q : Ω                                #   mutually implied props are
                                             #   equal codes (the binders
                                             #   extend by the props
                                             #   directly — prop-lift)

Γ ⊦ t : A

Γ ⊦ ⋆ : ∥A∥

Γ ⊦ a₀ ≐ a₁ : A

Γ ⊦ ⋆ : (a₀ ≡ a₁ ∈ A)                    #   UNFOLDING: premise and
                                         #   conclusion are the SAME
                                         #   judgement. Displayed for
                                         #   the kernel's citations
                                         #   (its ⋆-at-an-equality
                                         #   checking replays under
                                         #   this name)

Γ ⊦ s : (a₀ ≡ a₁ ∈ A)

Γ ⊦ a₀ ≐ a₁ : A                         #   Ω-valuedness forces it, by
                                        #   the realizer-irrelevance
                                        #   argument above applied at
                                        #   the equation's prop p:
                                        #   code-prop-eq at p, ∥𝟙∥
                                        #   (s[↑] one way, el-squash-i
                                        #   with ()[↑] the other) gives
                                        #   p ≐ ∥𝟙∥ : Ω; prop-lift-eq
                                        #   and el-ty-coe then carry
                                        #   el-squash-i's ⋆ : ∥𝟙∥
                                        #   into p. (Nothing is
                                        #   equation-specific — any
                                        #   inhabited prop admits ⋆
                                        #   this way; the ⋆'s occurring
                                        #   in TERMS sit at reflexive
                                        #   equations and come from
                                        #   el-refl.) The name is
                                        #   historical — REFLECTION is
                                        #   definitional under the
                                        #   ≐-notation; kept because
                                        #   the kernel replays it
                                        #   directly

Γ ⊦ p : Ω
Γ ⊦ t₀ : p
Γ ⊦ t₁ : p

Γ ⊦ t₀ ≐ t₁ : p                       #   a PROPOSITION are equal. The
                                      #   p : Ω premise replaces the
                                      #   retired Prf head — it was
                                      #   always this premise's
                                      #   syntactic proxy

Γ ⊦ s : ∥A∥
Γ ▷ A ⊦ b₀[↑] ≐ b₁[↑] : B[↑]

Γ ⊦ b₀ ≐ b₁ : B

Γ ⊦ q : Ω
Γ ⊦ s : ∥A∥
Γ ▷ A ⊦ t : q[↑]

Γ ⊦ ⋆ : 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 : 𝕍      Γ ▷ A ; Φ[↑] ⊦ 𝔄 qty

Γ ; Φ ⊦ A ⇛ 𝔄 qty                                    #   the Nova zone grows

Γ ; Φ ⊦ 𝕥 : U      Γ ; Φ ▷ El 𝕥 ⊦ 𝔄 qty

Γ ; Φ ⊦ El 𝕥 ⇛ 𝔄 qty                                    #   the ToS zone grows

Φ‖ᵢ = 𝔄

Γ ; Φ ⊦ ⬡ᵢ : 𝔄

Γ ; Φ ⊦ 𝕥 : A ⇛ 𝔄      Γ ⊦ t : A

Γ ; Φ ⊦ 𝕥 t : 𝔄[t]

Γ ; Φ ⊦ 𝕥 : El 𝕦 ⇛ 𝔄      Γ ; Φ ⊦ 𝕥' : El 𝕦

Γ ; Φ ⊦ 𝕥 𝕥' : 𝔄[𝕥']

Γ ▷ A ; Φ[↑] ⊦ 𝕥 : 𝔄

Γ ; Φ ⊦ λ 𝕥 : A ⇛ 𝔄

Γ ; Φ ⊦ 𝕥₀ : El 𝕦      Γ ; Φ ⊦ 𝕥₁ : El 𝕦

Γ ; Φ ⊦ (𝕥₀ ≡ 𝕥₁) : U

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

Γ ⊦ Φ qctx

Γ ⊦ 𝕚𝕕 : Φ ⇒ Φ

Γ ; Φ ⊦ 𝔄 qty

Γ ⊦ ⇑ : Φ ▷ 𝔄 ⇒ Φ

Γ ⊦ ς : Φ₀ ⇒ Φ₁      Γ ⊦ τ : Φ₁ ⇒ Φ₂

Γ ⊦ τ ∘ ς : Φ₀ ⇒ Φ₂

Γ ⊦ ς : Φ₀ ⇒ Φ₁      Γ ; Φ₀ ⊦ 𝕥 : 𝔄[ς]

Γ ⊦ (ς, 𝕥) : Φ₀ ⇒ Φ₁ ▷ 𝔄

Γ ; Φ₁ ⊦ 𝕥 : 𝔄      Γ ⊦ ς : Φ₀ ⇒ Φ₁

Γ ; Φ₀ ⊦ 𝕥[ς] : 𝔄[ς]                              #   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)

Γ ⊦ ⌊𝔄⌋ : 𝕍

Γ ⊦ 𝒮 qsig      𝒮(𝕤) = 𝔎  (𝔎 U-ended)

Γ ⊦ ⌊𝔎⌋ᵗ tel

⌊El (𝕤 ī)⌋_𝑤     ≜ 𝒮[υ].𝕤 ⌊ī⌋_𝑤      # ī = 𝕤's application chain,
                                      #   read off as a Nova spine
⌊El (l ≡ r)⌋_𝑤   ≜ (⌊l⌋_𝑤 ≡ ⌊r⌋_𝑤 ∈ ⌊El 𝕦⌋_𝑤)       # 𝕦 the sides' common
                                                     #   code; ≡ is Ω-valued,
                                                     #   so the type is the
                                                     #   equality prop itself
                                                     #   (prop-lift)
⌊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 reflected prop 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 ≔ 𝒮.𝕤 : 𝕍 (which unfolds, el-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 : 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 — the code IS the type, by code-lift. 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)      Γ ⊦ ē : ⌊𝔎⌋ᵗ

Γ ⊦ 𝒮.𝕤 ē : 𝕍

A signature is SMALL when every Nova type it embeds (the external Π domains) is itself codable — TYPED AT 𝕌, or TYPED AT Ω (props are size-free: subsingleton setoids, per the Ω block). With El and Prf both retired the condition is a judgemental DISJUNCTION, not a syntactic shape (the kernel checks each domain at 𝕌, then at Ω). The disjunction is deliberate: Ω does NOT embed into 𝕌 (no prop-resize rule) — that would drag propext into 𝕌's own equality via code-restrict, infecting the small universe's structural discipline for nothing this side condition does not already give. 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)      Γ ⊦ ē : ⌊𝔎⌋ᵗ

Γ ⊦ 𝒮.𝕤 ē : 𝕌

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 λ — a meta-property of definitional signatures, by the usual gluing argument) — 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 PROP, whose one canonical form is ⋆ — a constructor form there would be a second canonical inhabitant, refuting witness irrelevance. Nothing is lost — the prop 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 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

CONGRUENCE AND INJECTIVITY

≐ is congruent at the QIIT formers as at every former; the saturated forms' instances are stated because their premises live at the reflected telescope — entry i's type instantiated by the LEFT spine's prefix, the sub-norm-ext-cong discipline. Both congruences are ADMISSIBLE: substitution instances at the saturated former over the reflected telescope (the element congruence block's first scheme; the carried 𝒮 is fixed). Injectivity: 𝕌's equality is STRUCTURAL and a signature is inert syntax, so equal saturated sort codes have equal spines, indexwise — the code-pi-inj block, extended to the QIIT former.

Γ ⊦ 𝒮 qsig      Γ ⊦ e₀ᵢ ≐ e₁ᵢ : Eᵢ   (entrywise; Eᵢ is entry i of
                ⌊𝒮(𝕤)⌋ᵗ, instantiated by ē₀'s prefix)

Γ ⊦ 𝒮.𝕤 ē₀ ≐ 𝒮.𝕤 ē₁ : 𝕍

Γ ⊦ 𝒮 qsig      Γ ⊦ e₀ᵢ ≐ e₁ᵢ : Eᵢ   (entrywise at a point
                constructor's telescope ⌊𝒮(𝕔)⌋ᵗ, same discipline)

Γ ⊦ 𝒮.𝕔 ē₀ ≐ 𝒮.𝕔 ē₁ : ⌊El (𝕤 ī)⌋[ē₀]

Γ ⊦ 𝒮.𝕤 ē₀ ≐ 𝒮.𝕤 ē₁ : 𝕌      e₀ⱼ = e₁ⱼ for j < i  (structurally)

Γ ⊦ e₀ᵢ ≐ e₁ᵢ : Eᵢ

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_𝕤 : 𝕍

Γ ⊦ C̄ : 𝒮 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.

Γ ⊦ C̄ : 𝒮 mot      𝒮(𝕜) = 𝔄  (𝔄 ending in El (𝕤 ī))
Γ ⋈ 𝔄 ⊦ e : ⌊El (𝕤 ī)⌋_{𝑤_𝔄}

Γ ⊦ 𝔄ᴰ⟨e⟩ : 𝕍

Γ ⊦ C̄ : 𝒮 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 (l≡r) ; π⁺)

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 (l≡r)⌋_𝑤[π]
                                 → 𝔄ᴰ_{(𝑤;π) ▷ᴰ El (l≡r)}⟨e⟩          # no IH

(El 𝕦)ᴰᵗ_{𝑤;π}            ≜ ε
(A ⇛ 𝔄)ᴰᵗ_{𝑤;π}           ≜ A[ρ][π] ◁ 𝔄ᴰᵗ_{(𝑤;π) ▷ᴰ A}
(El (𝕤 ī) ⇛ 𝔄)ᴰᵗ_{𝑤;π}    ≜ ⌊El (𝕤 ī)⌋_𝑤[π] ◁ C_𝕤[⌊ī⌋_𝑤[π][↑], ☐₀]
                               ◁ 𝔄ᴰᵗ_{(𝑤;π) ▷ᴰ El (𝕤 ī)}
(El (l ≡ r) ⇛ 𝔄)ᴰᵗ_{𝑤;π}  ≜ ⌊El (l≡r)⌋_𝑤[π] ◁ 𝔄ᴰᵗ_{(𝑤;π) ▷ᴰ El (l≡r)}
                                                            # 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:

Γ ⊦ C̄ : 𝒮 mot
for each point position 𝕔 of 𝒮 (𝒮(𝕔) = 𝔄; δ = ⌊𝔄⌋ᵗ's variables):
    Γ ⊦ m_𝕔 : 𝔄ᴰ⟨𝒮.𝕔 δ⟩

Γ ⊦ (C̄ ; 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:

Γ ⊦ (C̄ ; m̄) : 𝒮 dalg      𝒮(𝕜) = 𝔄  (𝔄 El-ended)
(Γ ; 𝒮) ⋉ 𝔄 ⊦ 𝕥 : El (𝕤 ī)

Γ·𝔄ᴰᵗ ⊦ ⟦𝕥⟧ : C_𝕤[⌊ī⌋[πᴰ], ⌊𝕥⌋[πᴰ]]