Term

Syntax of the kernel's term language. All 48 constructors produce attrsets with a tag field (not _tag, to distinguish kernel terms from effect system nodes). Binding is de Bruijn indexed: mkVar i refers to the i-th enclosing binder (0 = innermost).

Name annotations (name parameter on mkPi, mkLam, mkSigma, mkLet) are cosmetic — used only in error messages, never in equality checking.

Constructors

Variables and Binding

• mkVar : Int → Tm — variable by de Bruijn index
• mkLet : String → Tm → Tm → Tm → Tm — let name : type = val in body
• mkAnn : Tm → Tm → Tm — type annotation (term : type)

Functions

• mkPi : String → Tm → Tm → Tm — dependent function type Π(name : domain). codomain
• mkLam : String → Tm → Tm → Tm — lambda λ(name : domain). body
• mkApp : Tm → Tm → Tm — application fn arg

Pairs

• mkSigma : String → Tm → Tm → Tm — dependent pair type Σ(name : fst). snd
• mkPair : Tm → Tm → Tm — pair constructor (fst, snd)
• mkFst : Tm → Tm — first projection
• mkSnd : Tm → Tm — second projection

Inductive Types

• mkUnit, mkTt — unit type and value
• mkBootSum, mkBootInl, mkBootInr, mkBootSumElim — bootstrap coproduct for descPlus
• mkBootEq, mkBootRefl, mkBootJ — identity type with J eliminator

Universes

• mkU : (Int | Tm) → Tm — universe U(level). Accepts either a concrete Int (wrapped via mkLevelLit) or a Level-typed Tm directly.
• mkLevelLit : Int → Tm — builds suc^n zero as a Level term.

Axiomatized Primitives

• mkString, mkInt, mkFloat, mkAttrs, mkPath, mkDerivation, mkFunction, mkAny — type formers
• mkStringLit, mkIntLit, mkFloatLit, mkAttrsLit, mkPathLit, mkDerivationLit, mkFnLit, mkAnyLit — literal values

funextTypeTm

funextTypeTm: pre-elaborated kernel term for the funext axiom's type ∀(j,k,A,B,f,g). (∀a. Eq (B a) (f a) (g a)) -> Eq (Π a:A. B a) f g.

mkAbsurd

mkAbsurd: empty-type eliminator — absurd P x discharges a stuck x : Empty to produce a value of any type P; well-typed only when x is a neutral (Empty has no canonical inhabitants).

mkAbsurd : Tm -> Tm -> Tm  -- type (P), term (x : Empty)

mkAllD

mkAllD: induction-hypothesis collector All D X P i payload — given motive P : (i:I) -> X i -> U(k), threads P through every recursive child in the payload.

mkAllD : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm  -- k, I, D, level, X, P, i, payload

mkAnn

mkAnn: type annotation (term : type) — fixes the checking direction at the kernel level; consumed by Sub and elaboration.

mkAnn : Tm -> Tm -> Tm  -- term, type

mkAnnTrusted

mkAnnTrusted: type annotation marked as elaborator-trusted — check skips re-validation of term against type since elaboration has already proved well-typedness.

mkAnnTrusted : Tm -> Tm -> Tm  -- term, type

mkAnnTrustedWithDescRef

mkAnnTrustedWithDescRef: trusted annotation carrying a _descRef sidecar — used by the HOAS elaborator to retain levitated description provenance across eval/quote round-trips.

mkAnnTrustedWithDescRef : Tm -> Tm -> Any -> Tm  -- term, type, descRef

mkAnnTrustedWithLabels

mkAnnTrustedWithLabels: trusted annotation carrying _label / _conLabel sidecars — used by H.withDescLabel / H.withConLabel to surface presentation labels on descView.

mkAnnTrustedWithLabels : Tm -> Tm -> { label?, conLabel? } -> Tm

mkAny

mkAny: axiomatised top primitive type Any — accepts every Nix value; used as the lossy-fallback kernel for approximate types.

mkAnyLit

mkAnyLit: kernel literal for an arbitrary Nix value v : Any — used by approximate types whose kernel slot is mkAny.

mkAnyLit : Any -> Tm

mkApp

mkApp: function application fn arg — head fn is checked first to infer Π type, then arg is checked against the domain.

mkApp : Tm -> Tm -> Tm  -- fn, arg

mkAttrs

mkAttrs: axiomatised primitive type Attrs — type former at U(0) inhabited by any Nix attribute set, including {}.

mkAttrsLit

mkAttrsLit: kernel literal for a Nix attribute set a : Attrs; the attrs are carried opaquely (no per-field validation at the kernel level).

mkAttrsLit : Attrs -> Tm

mkBootEq

mkBootEq: bootstrap identity type Eq(A, a, b) — propositional equality used by descRet's level transport and by the J eliminator.

mkBootEq : Tm -> Tm -> Tm -> Tm  -- A, a, b

mkBootInl

mkBootInl: left-injection of mkBootSum — inl(a) : A + B; carries both A and B for elaboration shape recovery.

mkBootInl : Tm -> Tm -> Tm -> Tm  -- leftTy, rightTy, value

mkBootInr

mkBootInr: right-injection of mkBootSum — inr(b) : A + B; carries both A and B for elaboration shape recovery.

mkBootInr : Tm -> Tm -> Tm -> Tm  -- leftTy, rightTy, value

mkBootJ

mkBootJ: J eliminator on mkBootEq — transports a property motive along a proof of equality, yielding a term at the other endpoint.

mkBootJ : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm  -- A, a, motive, identity, b, eq

mkBootRefl

mkBootRefl: bootstrap reflexivity refl : Eq(A, a, a) — the canonical inhabitant of every reflexive identity type; check-mode only at elaboration.

mkBootSum

mkBootSum: bootstrap coproduct type A + B — used by descPlus to encode sum-of-descriptions before generic sums become available.

mkBootSum : Tm -> Tm -> Tm  -- left, right

mkBootSumElim

mkBootSumElim: bootstrap sum eliminator — case-splits a A + B scrutinee through onLeft/onRight arms at motive (_:A+B) -> Q _.

mkBootSumElim : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm  -- leftTy, rightTy, motive, onLeft, onRight, scrut

mkCanonApp

mkCanonApp: generic identity-tagged application — canon-app id params body evaluates by currying-applying body to params and stamps the result VDescCon with _canonRef = { id; params; }; conv/quote short-circuit on the canonical identity instead of forcing .D.

mkCanonApp : String -> [Tm] -> Tm -> Tm  -- id, params, body

mkDerivation

mkDerivation: axiomatised primitive type Derivation — type former at U(0) inhabited by Nix derivation values (attrsets with type = "derivation"); the irreducible Nix-store-producing value category.

mkDerivationLit

mkDerivationLit: kernel literal for a Nix derivation d : Derivation; the value is carried opaquely (kernel never inspects derivation attrs).

mkDerivationLit : Derivation -> Tm

mkDesc

mkDesc: level-zero description type Desc I k at index sort I : U(0) and universe level k — the levitated algebra of constructors for datatypes.

mkDesc : Tm -> Tm -> Tm  -- k, I

mkDescAt

mkDescAt: Desc^k I carrying an explicit iLev for the universe of I. The kernel synthesises the desc-formation level as U(suc (max k iLev)).

mkDescAt : Tm -> Tm -> Tm -> Tm  -- iLev, k, I

mkDescCon

mkDescCon: constructor introduction for μ I D i — takes a payload typed by interpD D (μ I D) i and returns the corresponding μ value.

mkDescCon : Tm -> Tm -> Tm -> Tm  -- D, i, payload

mkDescConWithCert

mkDescConWithCert: mkDescCon carrying a Squash-truncated guard certificate — used by fx.types.Certified to thread refinement proofs through the kernel.

mkDescConWithCert : Tm -> Tm -> Tm -> Tm -> Tm  -- D, i, payload, cert

mkDescDescApp

mkDescDescApp: level-zero applied form of descDesc — Desc^(suc L) ⊤ whose mu-fixpoint is Desc^L I for I : U(0); bootstraps generic programming over descriptions themselves.

mkDescDescApp : Tm -> Tm -> Tm  -- I, L

mkDescDescAppAt

mkDescDescAppAt: applied form of descDesc carrying an explicit ℓ for the universe of I — generalised outer signature λℓ:Level. λI:U(ℓ). λL:Level. Desc^(suc (max L ℓ)) ⊤.

mkDescDescAppAt : Tm -> Tm -> Tm -> Tm  -- ℓ, I, L

mkDescInd

mkDescInd: levitated induction principle on μ I D — given a motive and step function, produces a generic recursor over the data described by D.

mkDescInd : Tm -> Tm -> Tm -> Tm -> Tm -> Tm  -- I, D, motive, step, scrut

mkEmpty

mkEmpty: empty type Empty — initial type at universe level 0; no constructors.

mkEverywhereD

mkEverywhereD: payload-traversal combinator over a description — applies a per-node f at every recursive position, producing a derived payload of the same shape.

mkEverywhereD : Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm -> Tm

mkFloat

mkFloat: axiomatised primitive type Float — type former at U(0) inhabited by Nix floats (excludes integers).

mkFloatLit

mkFloatLit: kernel literal for a Nix float x : Float.

mkFloatLit : Float -> Tm

mkFnLit

mkFnLit: kernel literal for an opaque Nix function f : Function — wraps the function in an fnBox for thunk-identity-preserving conversion.

mkFnLit : Function -> Tm

mkFst

mkFst: first-projection eliminator on a Σ-typed term — yields the dependent fst component; Σ-eta is exercised in conv.

mkFst : Tm -> Tm

mkFunction

mkFunction: axiomatised primitive type Function — type former at U(0) inhabited by opaque Nix-level functions wrapped via mkOpaqueLam.

mkFunext

mkFunext: function-extensionality axiom — given pointwise-equal f, g at every argument, produces an equality proof Eq (Π a:A. B a) f g.

mkFunext : Tm -> Tm -> Tm -> Tm -> Tm -> Tm  -- A, B, f, g, hypothesis

mkInt

mkInt: axiomatised primitive type Int — type former at U(0) inhabited by Nix integers (excludes floats).

mkIntLit

mkIntLit: kernel literal for a Nix integer n : Int.

mkIntLit : Int -> Tm

mkInterpD

mkInterpD: interpret a description D : Desc I k against a recursive carrier X : I -> U(k) at index i, yielding the payload type interpD D X i.

mkInterpD : Tm -> Tm -> Tm -> Tm -> Tm  -- k, I, D, X, i

mkLam

mkLam: lambda abstraction λ(name : domain). body — domain annotation is optional at check time (overridden by expected Π's domain).

mkLam : String -> Tm -> Tm -> Tm  -- name, domain, body

mkLet

mkLet: let-binding let name : type = val in body — name is cosmetic, the binder is introduced into body's de Bruijn context as index 0.

mkLet : String -> Tm -> Tm -> Tm -> Tm  -- name, type, val, body

mkLevel

mkLevel: universe-level sort Level : U(0) — the type former whose inhabitants are level expressions used in mkU.

mkLevelLit

mkLevelLit: concrete Level literal from an Int — builds suc^n zero as a Level term; entry point for level-polymorphism-free code.

mkLevelLit : Int -> Tm

mkLevelMax

mkLevelMax: pointwise max of two levels max(l, r) : Level — used to compute the universe of Σ / Π types whose components inhabit distinct universes.

mkLevelMax : Tm -> Tm -> Tm  -- l, r

mkLevelSuc

mkLevelSuc: successor suc(level) : Level — increment a Level expression by one.

mkLevelSuc : Tm -> Tm

mkLevelZero

mkLevelZero: level-zero literal 0 : Level — base case of Level's inductive structure.

mkLift

mkLift: Tarski lift LiftAt l m A : U(m) with l ≤ m — non-cumulative cross-level transport of a type at level l into level m.

mkLift : Tm -> Tm -> Tm -> Tm  -- l, m, A

mkLiftElim

mkLiftElim: elimination of Lift l m A — lowers a lifted term back to its original level; the inverse pairing with mkLiftIntro.

mkLiftElim : Tm -> Tm -> Tm -> Tm -> Tm  -- l, m, A, x

mkLiftIntro

mkLiftIntro: introduction of Lift l m A — lifts a term a : A at level l to a term at level m; eq witness is auto-emitted via mkBootRefl.

mkLiftIntro : Tm -> Tm -> Tm -> Tm -> Tm  -- l, m, A, a

mkLitVal

mkLitVal: closed-Val splice — opaque Val carrier whose eval is identity on the carried value. O(1) Val→Tm reflection; sound iff val is closed.

mkLitVal : Val -> Tm

mkMu

mkMu: levitated fixpoint μ I D i — carrier type of values whose constructors are described by D : Desc I k at index i.

mkMu : Tm -> Tm -> Tm -> Tm  -- I, D, i

mkOpaqueLam

mkOpaqueLam: lambda over an opaque Nix function — kernel never inspects or applies it; fnBox thunk identity preserves conv reflexivity across eval/quote rounds.

mkOpaqueLam : FnBox -> Tm -> Tm  -- fnBox, piType

mkPair

mkPair: pair constructor (fst, snd) — both components are checked against the corresponding Σ slots at the expected type.

mkPair : Tm -> Tm -> Tm  -- fst, snd

mkPath

mkPath: axiomatised primitive type Path — type former at U(0) inhabited by Nix path values.

mkPathLit

mkPathLit: kernel literal for a Nix path p : Path.

mkPathLit : Path -> Tm

mkPi

mkPi: dependent function type Π(name : domain). codomain — name is cosmetic, the binder is introduced into codomain's de Bruijn context as index 0.

mkPi : String -> Tm -> Tm -> Tm  -- name, domain, codomain

mkSigma

mkSigma: dependent pair type Σ(name : fst). snd — name is cosmetic, the binder is introduced into snd's de Bruijn context as index 0.

mkSigma : String -> Tm -> Tm -> Tm  -- name, fst, snd

mkSnd

mkSnd: second-projection eliminator on a Σ-typed term — yields the snd component with fst substituted; Σ-eta is exercised in conv.

mkSnd : Tm -> Tm

mkSquash

mkSquash: propositional truncation Squash A — quotient of A collapsing all inhabitants to one, used for proof-irrelevant fields.

mkSquash : Tm -> Tm

mkSquashElim

mkSquashElim: eliminator for Squash restricted to Squash-typed motives — preserves proof irrelevance by forbidding motives that distinguish inhabitants.

mkSquashElim : Tm -> Tm -> Tm -> Tm -> Tm  -- A, motive, fn, scrut

mkSquashIntro

mkSquashIntro: introduction of Squash A — lifts any a : A to a single inhabitant of Squash A.

mkSquashIntro : Tm -> Tm

mkStrEq

mkStrEq: decidable equality on String literals strEq a b : Bool — used by indexed datatypes whose constructor selection branches on string keys.

mkStrEq : Tm -> Tm -> Tm  -- a, b

mkString

mkString: axiomatised primitive type String — type former at U(0) inhabited by Nix string values.

mkStringLit

mkStringLit: kernel literal for a Nix string s : String.

mkStringLit : String -> Tm

mkTt

mkTt: unit value tt — sole inhabitant of mkUnit; eta-converts every term of type Unit to itself.

mkU

mkU: universe type U(level) at the given level expression — accepts either a concrete Int (wrapped via mkLevelLit) or a Level-typed Tm.

mkU : (Int | Tm) -> Tm

mkUnit

mkUnit: unit type Unit — terminal type with single inhabitant tt; backs fx.types.Unit at universe level 0.

mkVar

mkVar: variable reference by de Bruijn index — 0 is the innermost binder; higher indices reach outer binders.

mkVar : Int -> Tm