Hoas

Higher-Order Abstract Syntax layer that lets you write kernel terms using Nix lambdas for variable binding. The lower function compiles HOAS trees to de Bruijn indexed Tm terms.

Example

# Π(A:U₀). A → A
H.forall "A" (H.u 0) (A: H.forall "x" A (_: A))

Type Combinators

• nat, bool, unit, void — base types
• string, int_, float_, attrs, path, derivation, function_, any — primitive types
• thunk (parametric: thunk : Hoas -> Hoas) — generic deepSeq-safe carrier
• listOf : Hoas → Hoas — List(elem)
• sum : Hoas → Hoas → Hoas — Sum(left, right)
• eq : Hoas → Hoas → Hoas → Hoas — generated EqDT(type, lhs, rhs)
• u : Int → Hoas — Universe at level
• forall : String → Hoas → (Hoas → Hoas) → Hoas — Π-type (Nix lambda for body)
• sigma : String → Hoas → (Hoas → Hoas) → Hoas — Σ-type

Compound Types (Sugar)

• record : [{ name; type; }] → Hoas — nested Sigma (sorted fields)
• maybe : Hoas → Hoas — Sum(inner, Unit)
• variant : [{ tag; type; }] → Hoas — nested Sum (sorted tags)
• product : String → [Field] → DataSpec — named single-constructor μ-datatype

Term Combinators

• lam : String → Hoas → (Hoas → Hoas) → Hoas — λ-abstraction
• let_ : String → Hoas → Hoas → (Hoas → Hoas) → Hoas — let binding
• zero, succ, true_, false_, tt, refl — intro forms; refl is check-mode only
• nil, cons, pair, inl, inr — data constructors
• stringLit, intLit, floatLit, attrsLit, pathLit, derivationLit, fnLit, anyLit — primitive literals
• absurd, ann, app, fst_, snd_ — elimination/annotation

Eliminators

• ind — generated natural eliminator adapter
• boolElim — (k : Level) → (Q : bool → U(k)) → Q true_ → Q false_ → (b : bool) → Q b
• listElim — generated list eliminator adapter
• sumElim — generated sum eliminator adapter
• j — EqDT eliminator adapter with J-shaped arguments

Ornaments

• ornI, ornDesc, ornForget — first-class ornaments compiled to existing Desc, mu, and descInd programs; ornaments are not kernel primitives
• ornPullback, ornLiftFold — transport base programs to ornamented datatypes by composing with ornForget
• ornLiftProducer, ornLiftTransform — lift base producers/transforms through functional ornament output sections
• algOrn — algebraic ornament builder for descRet/descArg/descRec/keep-only descPi/descPlus, generating an ornament indexed by an algebra result
• functionalOrnament, ornBuild — manual sections of ornForget for explicit base-to-ornamented construction
• validateFunctionalLaws, functionalCompose — law metadata checks and composition for sectioned ornaments
• validateOrnament, tryOrnament, validateAlgOrn, tryAlgOrn — total structured diagnostics for user-facing ornament construction

Lowering

• lower : Int → Hoas → Tm — compile at given depth
• elab : Hoas → Tm — compile from depth 0

Convenience

• checkHoas : Hoas → Hoas → Tm|Error — elaborate type+term, type-check
• inferHoas : Hoas → { term; type; }|Error — elaborate and infer
• natLit : Int → Hoas — build S^n(zero)

Stack Safety

Binding chains (pi/lam/sigma/let), succ chains, and cons chains are elaborated iteratively via genericClosure — safe to 8000+ depth.

False

False: propositional falsehood — alias for the kernel-primitive void (empty) per HoTT Book, section 1.7 (False = ⊥); the initial-object dual of True.

False : Hoas

True

True: propositional truth — alias for unit per HoTT Book, section 1.7 (True = ⊤). Distinct from BoolDT's data-level true_.

True : Hoas

WDT

WDT: W-type description macro — packages shape sort + position family into a DataSpec for arbitrary-branching inductive trees outside the description layer.

WDT : Hoas -> (Hoas -> Hoas) -> DataSpec

absurd

absurd: HOAS empty-type eliminator — absurd P x discharges x : Empty to a value of any type P at any universe level; the unique map from the initial object.

absurd : Hoas -> Hoas -> Hoas  -- targetType P, scrutinee x

absurdFin0

absurdFin0: vacuous-fin 0 eliminator — absurdFin0 P x discharges x : fin 0 to any type P via no-confusion on the impossible Eq Nat (succ m) zero.

absurdFin0 : Hoas -> Hoas -> Hoas  -- P, x

fin 0 is vacuous because both fzero and fsuc constructor payloads carry Eq Nat (succ m) i leaves, which at i = 0 give Eq Nat (succ m) zero — uninhabited. The implementation uses a single J transport at motive λx _. natCaseU P Unit x, landing at Unit for succ cases (filled by tt) and at P at the goal case i = zero. Used by void and surface absurd.

absurdPrim

absurdPrim: HOAS kernel-primitive empty-type eliminator — absurdPrim P x discharges a stuck x : Empty to produce a value of any type P at any universe level; the unique map from the initial object.

absurdPrim : Hoas -> Hoas -> Hoas  -- targetType P, scrutinee x

algArg

algArg: arg algebra — consumes the descArg's payload via body : s -> Algebra, recursing into the rest of the description through the resulting algebra.

algArg : (Tm -> Algebra) -> Algebra

algOrn

algOrn: build an Ornament from an algebra over a base description — indexed by the algebra's result, so each ornamented value carries its algebra trace as the J-index.

algOrn : { I?, J, baseD | D, erase, algebra, resultTy?, pack?, proof?, level?, meta? } -> Ornament

algOrnDiagnosticRecords

algOrnDiagnosticRecords: total structured diagnostics describing every shape mismatch between an algebra and its target description; returns [] on success.

algOrnDiagnosticRecords : Attrs -> [Diagnostic]

algOrnDiagnostics

algOrnDiagnostics: human-readable text forms of algOrnDiagnosticRecords for inclusion in error messages and test assertions.

algOrnDiagnostics : Attrs -> [String]

algPiKeep

algPiKeep: pi-keep algebra — body consumes the Π-quantified branch using branchIndex (or full { branchIndex, ... } record), generating an algebra per branch.

algPiKeep : (Tm | { branchIndex, ... }) -> (Tm -> Algebra) -> Algebra

algPlus

algPlus: plus algebra — sum of two sub-algebras, mirroring descPlus; routes the algebra into left or right depending on the constructor arm taken.

algPlus : Algebra -> Algebra -> Algebra

algRec

algRec: rec algebra — handles a descRec arm by giving body : recResult -> Algebra over the recursive child's algebra result; threads results upward.

algRec : (Tm -> Algebra) -> Algebra

algRet

algRet: ret algebra — terminates an algebraic ornament arm by returning a constant result value for the leaf description; used over descRet shapes.

algRet : Tm -> Algebra

allD

allD: induction-hypothesis collector — allD level I D K X M i d produces the type All D X M i d, threading motive M through every recursive position in payload d.

allD : Level -> Hoas -> Hoas -> Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas

and

and: propositional conjunction — and P Q := Σ (_:P). Q per HoTT Book, section 1.7. Elaborates to a sigma.

and : Hoas -> Hoas -> Hoas

ann

ann: HOAS type annotation — ann term type produces (term : type); fixes the checking direction so the kernel verifies term against type rather than inferring.

ann : Hoas -> Hoas -> Hoas

Essential at every position where the kernel would otherwise need to infer a type from a checkable form (e.g. lambda bodies producing data constructors). The elaborator emits mkAnn; check consumes the annotation and validates the term against the declared type. Default — re-checks the body at every use site. For named-definition / δ-rule discipline on smart constructors whose bodies are well-typed by construction (and where re-checking would diverge through mutual recursion), see annTrusted.

annTrusted

annTrusted: HOAS type annotation that propagates the declared type without re-checking the body — the δ-rule analogue. annTrusted term type declares (term : type) as a named definition whose body is well-typed by construction.

annTrusted : Hoas -> Hoas -> Hoas

Use this for smart constructors that wrap closed expressions whose well-typedness follows compositionally from the kernel-typed combinators used to build them. The infer rule's trusted branch skips the body re-check that ann performs, making this the only viable annotation form for mutually recursive smart constructors (e.g. freeFxApp ↔ kontQueueApp in experimental/desc-interp/desc.nix, where each body references the other through μ(…App …)).

Discipline: the caller is responsible for verifying the body against the declared type at definition time (manually, or via a separately-checkable test fixture). At use sites the kernel propagates the declared type unconditionally.

Elaborates to mkAnnTrusted. Equivalent in spirit to Coq's Definition foo : T := body or Agda's signature-then-body form — the type is looked up at use sites, not re-derived.

any

any: kernel-primitive Any type — top type covering every Nix value; used as a fallback when no narrower type fits.

any : Hoas

anyLit

anyLit: HOAS Any-literal marker — placeholder term checkable against any; covers any kernel-opaque Nix value.

anyLit : Hoas

app

app: HOAS function application — app f arg builds the redex; β-reduces during normalisation when f is a lambda.

app : Hoas -> Hoas -> Hoas

attrs

attrs: kernel-primitive Attrs type — opaque Nix attrset axiomatised at the kernel level; literal-only entry via attrsLit.

attrs : Hoas

attrsLit

attrsLit: HOAS Attrs-literal marker — placeholder term checkable against attrs; the actual Nix attrset is not embedded in the kernel term.

attrsLit : Hoas

bool

bool: HOAS Bool type former — generated by BoolDT.T; isomorphic to Sum Unit Unit under the description encoding.

bool : Hoas

boolElim

boolElim: HOAS Bool eliminator — boolElim k Q onT onF b runs BoolDT.elim k; the motive Q : bool -> U(k) may depend on the scrutinee.

boolElim : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- k, motive, onTrue, onFalse, scrut

For constant motives use tc.verified.if_ which auto- generates λ_:bool.resultTy. Dependent motives are needed when the result type differs between true and false cases — e.g. dispatching to different datatypes via natCaseU.

canonApp

canonApp: generic identity-tagged HOAS application — canonApp id params body produces a VDescCon stamped with _canonRef = { id; params; } at eval time, so conv/quote short-circuit on the canonical identity instead of forcing the recursive .D slot. Use to add cycle-safe outer references for user-defined recursive descriptions (freer monads, FTCQueues, ...).

canonApp : String -> [Hoas] -> Hoas -> Hoas

checkFunctionalLaws

checkFunctionalLaws: identity on F when every law-check passes, otherwise throws the concatenated diagnostic text — the assertive sibling of validateFunctionalLaws.

checkFunctionalLaws : FunctionalOrnament -> FunctionalOrnament  -- throws on failure

checkHoas

checkHoas: HOAS-driven type-checker — checkHoas typeHoas termHoas elaborates both, runs the kernel check rule, and returns the checked term or a structured Error.

checkHoas : Hoas -> Hoas -> Tm | Error

The principal entry for verifying a HOAS term against a HOAS type. Elaborates type and term in tandem (so binders align), then invokes the kernel check rule which produces a verified Tm or a structured Error carrying the failing rule and contextual Detail. Returns the Error directly (does not throw); callers route through ?error for fast dispatch.

con

con: HOAS constructor declarator — con name fields packages an ordered list of field declarations into a constructor specification consumed by datatype.

con : String -> [Field] -> Constructor

conI

conI: indexed-constructor declarator — conI name fields targetIndex declares a constructor whose carrier targets a specific index of the datatype's index family.

conI : String -> [Field] -> (Hoas -> Hoas) -> Constructor

cong

cong: User-Eq congruence — proof of ∀A B (f:A→B) x y. Eq A x y -> Eq B (f x) (f y); one J application transporting refl through the function. Composes with trans for diagram-chase proofs on derived equalities.

cong : Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- A, B, f, x, y, p

congSuc

congSuc: Level-suc congruence — proof of ∀a b. Eq Level a b -> Eq Level (suc a) (suc b); derived via J transporting refl along the supplied equality.

congSuc : Hoas

cons

cons: HOAS list-cons constructor — cons h t prepends h : A to t : listOf A; element type inferred.

cons : Hoas -> Hoas -> Hoas  -- head, tail

datatype

datatype: HOAS datatype macro — datatype name [con …] declares a named ⊤-slice datatype, emitting { D, T, elim, <constructors> } with _dtypeMeta for walker dispatch.

datatype : String -> [Constructor] -> DataSpec

The macro builds the description from constructor field lists, synthesises the type former (T = mu D tt), generated constructors that introduce values, and an eliminator specialised for the description. The result attrset's _dtypeMeta field carries the constructor list for walker dispatch (used by recoverConstructor / walkAttrsetDatatype). Surface entry point for declaring new datatypes — prefer over manual mu + descCon construction.

datatypeI

datatypeI: indexed-datatype macro — datatypeI name indexSort [conI …] declares a datatype indexed by indexSort; each constructor must declare its target index.

datatypeI : String -> Hoas -> [ConI] -> DataSpec

Indexed counterpart to datatype. The index sort I parametrises the carrier family, and each constructor's conI declares the index it produces. The resulting T : I -> U is the family type former; app T idx is the carrier at a specific index. Prelude fin, vec use this form.

datatypeP

datatypeP: parametric-datatype macro — datatypeP name [param …] [con …] declares a datatype parametric in zero or more sort parameters.

datatypeP : String -> [Param] -> (Hoas -> [Constructor]) -> DataSpec

Parameters are sorts external to the datatype; the constructor list is a function of the parameter binders. Resulting T takes parameters before producing the carrier type. Prelude listOf, sum would be expressed via this macro (in practice they're macro-generated via ListDT, SumDT at fixed parameter shapes).

datatypePI

datatypePI: parametric + indexed datatype — datatypePI name [param …] indexSortFn [conI …] combines parameters and indices in one macro.

datatypePI : String -> [Param] -> (Hoas -> Hoas) -> (Hoas -> [ConI]) -> DataSpec

The most general datatype declarator: takes external parameters AND an index sort that can depend on those parameters, AND constructors whose index decisions depend on both. Used by vec (parameter A, index n : nat) and similar prelude families.

dec

dec: decidability proposition — dec P := P ⊎ ¬ P per Agda Relation.Nullary.Dec. Defined as sum P (not P); inhabitants built via yes / no and eliminated via decElim.

dec : Hoas -> Hoas

decAnd

decAnd: conjunction decidability — decAnd P Q dp dq : dec (and P Q) given dp : dec P and dq : dec Q. Both yes ⇒ yes (pair); either no ⇒ no (refute via fst/snd).

decAnd : Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- P, Q, decP, decQ

decElim

decElim: eliminator for dec P — decElim P motive oy on d discharges d : dec P against motive M : dec P -> U(0) with branches oy : (p:P) -> M (yes _ p) and on : (r: not P) -> M (no _ r). Forwards to sumElim at level 0.

decElim : Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- P, motive, oyes, ono, d

decNot

decNot: negation decidability — decNot P dp : dec (not P). yes ⇒ no (negation contradicts the proof); no ⇒ yes (the refutation IS the negation witness).

decNot : Hoas -> Hoas -> Hoas  -- P, decP

decOr

decOr: disjunction decidability — decOr P Q dp dq : dec (or_ P Q). Either yes ⇒ yes (inl/inr); both no ⇒ no (refute via sumElim).

decOr : Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- P, Q, decP, decQ

decideEqIntZ

decideEqIntZ: decidability of IntZ equality — decideEqIntZ m n : dec (Eq IntZ m n). Four-case intzElim sign cascade; same-sign quadrants delegate to decideEqNat and lift via cong / injectivity; cross-sign quadrants refute via signsDiffer / signsDifferRev. Agda Data.Integer.Properties._≟_.

decideEqIntZ : Hoas  -- closed kernel function Π m. Π n. dec (Eq IntZ m n)

decideEqNat

decideEqNat: decidability of Nat equality — decideEqNat m n : dec (Eq Nat m n). Closed kernel lam-term performing simultaneous structural recursion on both arguments. Agda Data.Nat.Properties._≟_.

decideEqNat : Hoas  -- closed kernel function Π m. Π n. dec (Eq Nat m n)

decideLeIntZ

decideLeIntZ: decidability of intzLe — decideLeIntZ m n : dec (intzLe m n). Four-case intzElim sign cascade following intzLe's quadrant table; pos-pos delegates to decideLeNat, pos-negSucc returns no (target reduces to void), negSucc-pos returns yes tt (target reduces to unit), negSucc-negSucc delegates to decideLeNat at flipped arguments. Agda Data.Integer.Properties._≤?_.

decideLeIntZ : Hoas  -- closed kernel function Π m. Π n. dec (intzLe m n)

decideLeNat

decideLeNat: decidability of Le — decideLeNat m n : dec (le m n). Closed kernel lam-term following Agda Data.Nat.Properties._≤?_ four-case recipe (zero-zero, zero-suc, suc-zero, suc-suc).

decideLeNat : Hoas  -- closed kernel function Π m. Π n. dec (le m n)

derivation

derivation: kernel-primitive Derivation type — Nix derivation values (attrsets carrying type = "derivation"); the store-producing irreducible Nix value category, axiomatised at the kernel level with literal-only entry via derivationLit.

derivation : Hoas

derivationLit

derivationLit: HOAS Derivation-literal marker — placeholder term checkable against derivation; the Nix derivation is not embedded in the kernel term.

derivationLit : Hoas

desc

desc: ⊤-slice description type former — alias for descI unitPrim; descriptions over the kernel-primitive unit index type.

desc : Hoas

descArg

descArg: argument-position description-encoder — descArg I k S T extends a description with a non-recursive field of sort S, with T the continuation under the bound value.

descArg : Hoas -> Level -> Hoas -> Hoas -> Hoas

descCon

descCon: description-constructor introduction — descCon D i d builds an element of μ I D i from payload d matching D's shape at index i.

descCon : Hoas -> Hoas -> Hoas -> Hoas  -- D, index, payload

Used internally by the elaborator to emit mu carriers from interpreted payloads. Surface code building inductive values typically routes through generated constructors (zero/succ/true_/nil/etc.) which call descCon with the right payload shape. Direct use is for advanced ornament-bridging code.

descDesc

descDesc: levitated description-of-descriptions — descDesc I k is the description whose μ-carrier is Desc^k I; foundational for description encoding.

descDesc : Hoas -> Level -> Hoas  -- I, k

The plus-tree of descDesc has five summands corresponding to the description constructors (retI, descArg, recI, piI, plusI). Every encoded HOAS description elaborates through descDesc so each VDescCon value carries its constructor tag explicitly. Universe-polymorphic over k.

descElim

descElim: encoded description eliminator — descElim I k L motive onRet onArg onRec onPi onPlus scrut walks the cascade over descDesc I k's plus-tree to dispatch on scrut's constructor summand.

descElim : Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas

The deep machinery for analysing description shapes. Each on* callback handles one summand of the description encoding. Surface code rarely needs this directly — descInd is the friendlier face for value-level induction; descElim is needed for type-level dispatch over description shape (e.g. inside ornament machinery).

descInd

descInd: description-induction principle — descInd D motive step i scrut eliminates scrut : μ I D i against motive Q : ∀i:I. μ I D i -> U, using step to handle each summand with its inductive hypotheses.

descInd : Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- D, motive, step, index, scrut

Generic indexed induction. The step argument receives the index, the payload, and the inductive hypotheses (allD- wrapped). Generated eliminators like NatDT.elim, ListDT.elim are pre-applied specialisations of descInd.

descPi

descPi: ⊤-slice piI alias — descPi k S D quantifies over sort S and continues with D under a constant-index function; the index-of-payload defaults to ttPrim.

descPi : Level -> Hoas -> Hoas -> Hoas  -- k, sort, continuation

descRec

descRec: ⊤-slice recI alias — recI unitPrim 0 ttPrim D; adds a ⊤-indexed recursive child to a description.

descRec : Hoas -> Hoas  -- continuation

descRet

descRet: ⊤-slice retI alias — retI unitPrim 0 ttPrim; the standard leaf of a ⊤-indexed description, used by prelude descriptions like natDesc.

descRet : Hoas

elab

elab: closed-term HOAS-to-Tm compiler — lowers a HOAS term from depth 0, runs meta-aware synthesis + zonking, and surfaces unsolved metas as a throw at the elaborator boundary.

elab : Hoas -> Tm

elab2

elab2: pair-producing elaborator — runs elab and sourceMapOf together, returning { tm, sourceMap }; used by the diagnostic shell which consumes both outputs.

elab2 : Hoas -> { tm : Tm, sourceMap : SourceMap }

embedTm

embedTm: opaque HOAS carrier for a closed kernel Tm — embedTm tm wraps an already-elaborated term so it can sit inside a surrounding HOAS tree; elaborate returns the carried tm verbatim regardless of binding depth.

embedTm : Tm -> Hoas

Use when a pre-built Tm needs to flow back through the HOAS surface. For Val embedding, prefer H.litVal (or fx.tc.elaborate.embedVal), which reflects the Val directly in O(1) without the quote 0 walk.

Soundness depends on the carried Tm being closed under the binders surrounding the embed site.

Elaborates via the pre-elab rule in tc/hoas/lower.nix.

empty

empty: HOAS empty type — alias for the kernel-primitive emptyPrim; the initial-object dual of unit.

empty : Hoas

eq

eq: HOAS propositional equality — eq A a b builds EqDT A a b, the levitated identity type over a sort A; refl introduces, j eliminates.

eq : Hoas -> Hoas -> Hoas -> Hoas

eqCongSucc

eqCongSucc: congruence of suc — eqCongSucc m n e : Eq Nat (suc m) (suc n) given e : Eq Nat m n. bootJ at motive λx _. Eq Nat (suc m) (suc x); base case satisfied by bootRefl.

eqCongSucc : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, eq

eqDT

eqDT: prelude equality type — eqDT A a b is μ A (eqDesc A a) b, the indexed datatype carrier of equality at sort A.

eqDT : Hoas -> Hoas -> Hoas -> Hoas  -- A, lhs, rhs

eqDTToEq

eqDTToEq: datatype equality → bootstrap equality — eqDTToEq A a b x extracts a bootEq A a b witness from x : eqDT A a b via descInd at motive Q i x = bootEq A a i.

eqDTToEq : Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- A, lhs, rhs, x

eqDesc

eqDesc: prelude equality description — eqDesc A a builds the single-constructor retI-only description of EqDT A a : A -> U, used as the carrier description of equality at sort A.

eqDesc : Hoas -> Hoas -> Hoas  -- A, lhs

eqInjSucc

eqInjSucc: injectivity of suc — eqInjSucc m n e : Eq Nat m n given e : Eq Nat (suc m) (suc n). bootJ at motive λx _. Eq Nat m (predNat x); base case Eq Nat m m via β-reduction of predNat (suc m).

eqInjSucc : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, eqSucc

eqIsoBwd

eqIsoBwd: backward leg of the eq ↔ eqDT iso — proves bootEq (eqDT A a b) (eqToEqDT (eqDTToEq x)) x; descInd on x reduces to the diagonal via inner J transport.

eqIsoBwd : Hoas -> Hoas -> Hoas -> Hoas  -- A, lhs, rhs

eqIsoFwd

eqIsoFwd: forward leg of the eq ↔ eqDT iso — proves bootEq (bootEq A a b) (eqDTToEq (eqToEqDT e)) e; J on e collapses both sides at the base case.

eqIsoFwd : Hoas -> Hoas -> Hoas -> Hoas  -- A, lhs, rhs

eqRefutSuccZero

eqRefutSuccZero: McBride no-confusion — eqRefutSuccZero m e : void refutes e : Eq Nat (suc m) zero. bootJ at motive λx _. natCaseU void unit x; base tt at unit, result void at zero.

eqRefutSuccZero : Hoas -> Hoas -> Hoas  -- m, eq

eqRefutZeroSucc

eqRefutZeroSucc: symmetric McBride no-confusion — eqRefutZeroSucc n e : void refutes e : Eq Nat zero (suc n). bootJ at motive λx _. natCaseU unit void x.

eqRefutZeroSucc : Hoas -> Hoas -> Hoas  -- n, eq

eqToEqDT

eqToEqDT: bootstrap equality → datatype equality — eqToEqDT A a b e converts e : bootEq A a b to eqDT A a b via J transporting reflDT along the witness.

eqToEqDT : Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- A, lhs, rhs, eq

everywhereD

everywhereD: induction-hypothesis constructor — everywhereD level I D K X M ih i d builds the allD … witness by applying ih at every recursive subposition.

everywhereD : Level -> Hoas -> Hoas -> Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas

false_

false: HOAS Bool constructor false — generated by BoolDT; corresponds to the left summand of bool-as-Sum Unit Unit._

false_ : Hoas

field

field: HOAS datatype field declarator — field name type declares a non-recursive constructor field; the macro routes through descArg.

field : String -> Hoas -> { name; type; }

fieldD

fieldD: dependent-field declarator — fieldD name type indexFn declares a field whose type can depend on prior fields via the index function.

fieldD : String -> Hoas -> (Hoas -> Hoas) -> { name; type; indexFn; }

fin

fin: prelude Fin type family — forwarder for FinDT.T; app fin n is the type of natural numbers strictly less than n.

fin : Hoas  -- application yields fin n : Hoas

finDesc

finDesc: prelude Fin description — forwarder for FinDT.D, the indexed description of the finite-natural family Fin : nat -> U.

finDesc : Hoas

finElim

finElim: prelude Fin eliminator — finElim k P Pz Ps n x discharges x : fin n against motive P : ∀n:nat. fin n -> U(k) with branches for fzero / fsuc.

finElim : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas

floatLit

floatLit: HOAS Float literal — floatLit f lifts a Nix float to a kernel floatLit Tm checkable against float_.

floatLit : Float -> Hoas

float_

float: kernel-primitive Float type — Nix-meta floats axiomatised at the kernel level; literals enter via floatLit._

float_ : Hoas

fnLit

fnLit: HOAS Function-literal marker — placeholder term checkable against function_; the Nix function is not embedded in the kernel term.

fnLit : Hoas

forall

forall: HOAS Π-type former — forall name dom body builds Π(name:dom). body with body a Nix function receiving the bound variable as a HOAS term.

forall : String -> Hoas -> (Hoas -> Hoas) -> Hoas

The body is a Nix function so the binder is a real Nix-level variable inside the user's scope. elaborate converts it to a de Bruijn Tm with the correct index. Chains of forall are elaborated iteratively via genericClosure, so deeply-nested Π-types are stack-safe to depths of 8000+. The name is cosmetic — used only in error messages and never in equality checking.

fst_

fst: HOAS Σ-pair first projection — extracts the left component; reduces by π₁ during normalisation when the argument is a pair._

fst_ : Hoas -> Hoas

fsuc

fsuc: prelude Fin successor constructor — fsuc k lifts k : fin m to succ k : fin (succ m); predecessor inferred.

fsuc : Hoas -> Hoas  -- fin-predecessor

function_

function: kernel-primitive Function type — opaque Nix function axiomatised at the kernel level; literal-only entry via fnLit._

function_ : Hoas

functionalCompose

functionalCompose: compose two functional ornaments outer over inner, producing a functional ornament whose section threads through both chooseIndex/section pipelines.

functionalCompose : FunctionalOrnament -> FunctionalOrnament -> FunctionalOrnament

functionalLawDiagnosticRecords

functionalLawDiagnosticRecords: run every check in F.laws.checks, collecting structured diagnostics for every law that fails to evaluate or returns non-true; total.

functionalLawDiagnosticRecords : FunctionalOrnament -> [Diagnostic]

functionalLawDiagnostics

functionalLawDiagnostics: human-readable string forms of functionalLawDiagnosticRecords for surfacing law-check failures in test output and error reports.

functionalLawDiagnostics : FunctionalOrnament -> [String]

functionalOrnament

functionalOrnament: package { ornament, chooseIndex, section, indexProof?, laws?, meta? } into a validated FunctionalOrnament record, the section/builder bundle that bridges base producers to ornamented outputs.

functionalOrnament : { ornament, chooseIndex, section, indexProof?, laws?, meta? } -> FunctionalOrnament

functionalOrnamentDiagnosticRecords

functionalOrnamentDiagnosticRecords: total structured diagnostics describing every missing / ill-typed field of a candidate functionalOrnament spec; returns [] when the spec is valid.

functionalOrnamentDiagnosticRecords : Attrs -> [Diagnostic]

functionalOrnamentDiagnostics

functionalOrnamentDiagnostics: human-readable strings derived from functionalOrnamentDiagnosticRecords for surfacing in error messages and test assertions.

functionalOrnamentDiagnostics : Attrs -> [String]

fzero

fzero: prelude Fin zero constructor — fzero : fin (succ m); predecessor inferred from the expected type.

fzero : Hoas

iff

iff: propositional biconditional — iff P Q := (P → Q) × (Q → P) per HoTT Book, section 1.7. Built as and (P→Q) (Q→P).

iff : Hoas -> Hoas -> Hoas

implicitApp

Implicit application — caller passes implicit explicitly. Same kernel Tm as app, plus _plicity sidecar.

Hoas -> Hoas -> Hoas

implicitForall

Implicit Π-binder. Same kernel Tm as forall, plus _plicity sidecar.

String -> Hoas -> (Hoas -> Hoas) -> Hoas

implicitLam

Implicit λ-binder. Same kernel Tm as lam, plus _plicity sidecar.

String -> Hoas -> (Hoas -> Hoas) -> Hoas

ind

ind: HOAS Nat induction principle wrapper — ind k P B S n runs NatDT.elim k after binding motive P, base B, and step S at their required types.

ind : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- k, motive, base, step, scrut

The motive P : nat -> U(k) may depend on the scrutinee; for constant motives drop to tc.verified.match which auto- generates λ_:nat.resultTy. The wrapper inserts three let_ bindings before the application spine so the kernel can infer each leg of the dependent application chain. Level k accepts a Nix Int, a HOAS Level term, or a kernel Tm.

inferHoas

inferHoas: HOAS-driven type inference — inferHoas termHoas elaborates and runs the kernel infer rule, returning { term, type } or a structured Error.

inferHoas : Hoas -> { term : Tm, type : Val } | Error

Complement to checkHoas for the synthesis direction. Many HOAS forms are inference-friendly (annotated values, applications with inferable heads); pure inference fails on checking-only forms like bare lambdas or data constructors without an enclosing annotation.

inl

inl: HOAS sum left-injection — inl v builds Left v : Sum A B; level, leftTy, rightTy inferred. Alias of inlAt post-implicit-migration.

inl : Hoas -> Hoas  -- value

inr

inr: HOAS sum right-injection — inr v builds Right v : Sum A B; level, leftTy, rightTy inferred. Alias of inrAt post-implicit-migration.

inr : Hoas -> Hoas  -- value

intLit

intLit: HOAS Int literal — intLit n lifts a Nix integer to a kernel intLit Tm checkable against int_.

intLit : Int -> Hoas

int_

int: kernel-primitive Int type — Nix-meta integers axiomatised at the kernel level; distinct from nat, which is the description-derived Nat._

int_ : Hoas

interpD

interpD: description interpreter — interpD level I D X i produces the payload type ⟦D⟧ X i at level level, the fibre over index i when the recursive position is filled by X.

interpD : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- level, I, D, X, i

intz

intz: prelude IntZ type — IntZDT.T. Literature-canonical 2-constructor inductive integer with unique representation.

intz : Hoas

intzDecode

intzDecode: sign-erasing payload extractor intz -> Nat. intzPos n and intzNegSucc n both yield n. Used as the bootJ motive discriminator in intzPosInjective / intzNegSuccInjective.

intzDecode : Hoas

intzDesc

intzDesc: prelude IntZ description — IntZDT.D. Two-summand description with one Nat field per constructor (pos / negSucc).

intzDesc : Hoas

intzElim

intzElim: prelude IntZ eliminator — intzElim k Q onPos onNegSucc z runs IntZDT.elim k; the motive Q : intz -> U(k) may depend on the scrutinee. Mirrors boolElim's shape with two payload-carrying case branches over a Nat field each.

intzElim : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- k, motive, onPos, onNegSucc, scrut

intzLe

intzLe: prelude IntZ ordering type-family — intzLe m n : U(0) follows Agda Data.Integer.Base._≤_ four cases: pos-pos delegates to Nat le; pos-negSucc is void (positives never ≤ negatives); negSucc-pos is unit (negatives always ≤ positives); negSucc-negSucc flips arguments and delegates back to Nat le (negSucc is monotonically decreasing in its argument).

intzLe : Hoas -> Hoas -> Hoas  -- m, n

intzLit

intzLit: Nix-meta bridge from a Nix integer to IntZ — intzLit n returns intzPos (natLit n) for n >= 0 and intzNegSucc (natLit (-n - 1)) for n < 0. Boundary cases: intzLit 0 = intzPos 0; intzLit (-1) = intzNegSucc 0.

intzLit : Int -> Hoas

intzNegSucc

intzNegSucc: prelude IntZ negative constructor — intzNegSucc n : intz encodes the integer -(n+1) for n : Nat. intzNegSucc 0 is -1.

intzNegSucc : Hoas -> Hoas  -- n

intzNegSuccCong

intzNegSuccCong: congruence of intzNegSucc — intzNegSuccCong m n e : Eq IntZ (negSucc m) (negSucc n) lifts e : Eq Nat m n.

intzNegSuccCong : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, natEq

intzNegSuccInjective

intzNegSuccInjective: symmetric injectivity of intzNegSucc via the same intzDecode motive.

intzNegSuccInjective : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, intzEq

intzPos

intzPos: prelude IntZ non-negative constructor — intzPos n : intz encodes the integer n for n : Nat. intzPos 0 is the canonical zero.

intzPos : Hoas -> Hoas  -- n

intzPosCong

intzPosCong: congruence of intzPos — intzPosCong m n e : Eq IntZ (pos m) (pos n) lifts e : Eq Nat m n. bootJ at motive λx _. Eq IntZ (pos m) (pos x); mirrors eqCongSucc.

intzPosCong : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, natEq

intzPosInjective

intzPosInjective: injectivity of intzPos — intzPosInjective m n e : Eq Nat m n from e : Eq IntZ (pos m) (pos n). bootJ at motive λx _. Eq Nat m (intzDecode x); β on the decoder collapses base case to Eq Nat m m.

intzPosInjective : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, intzEq

isLeafOrn

isLeafOrn: predicate identifying leaf functional ornaments via the _leafOrnTag = "leaf-ornament" tag.

isLeafOrn : Value -> Bool

j

j: HOAS J-eliminator for EqDT — j A a P base b e discharges e : EqDT A a b against motive P : ∀x:A. EqDT A a x -> U, computing the goal type at b.

j : Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- type, lhs, motive, base, rhs, eq

The classic Martin-Löf J: given a base case at the diagonal (base : P a refl), transports along any equality. Used by transNat, congSuc, maxSucDom, eqToEqDT, etc. The motive must accept both the right-hand side and the equality term; for substitution-only patterns, write a constant-in-eq motive λx _. ....

just

just: HOAS Maybe just-injection — just innerTy v is inl v : maybe innerTy.

just : Hoas -> Hoas -> Hoas  -- innerTy, value

lam

lam: HOAS lambda — lam name dom body builds λ(name:dom). body with body a Nix function receiving the bound variable; the principal term-binding form.

lam : String -> Hoas -> (Hoas -> Hoas) -> Hoas

Body is a Nix function, so the variable binding flows through Nix's own scope. elaborate produces a de Bruijn Tm with index 0 for the innermost binder. Chains of lam are elaborated iteratively (stack-safe to 8000+). Use opaqueLam when wrapping a non-HOAS Nix function for which kernel checking would otherwise require recovering structure.

le

le: prelude Le curried type family — le m n is the type of proofs that m ≤ n over Nat. The Agda Data.Nat.Base._≤_ inductive predicate (z≤n / s≤s constructors).

le : Hoas -> Hoas -> Hoas  -- m, n

leDesc

leDesc: prelude Le description — forwarder for LeDT.D, the indexed description of the order family Le : Σ Nat (_: Nat) -> U (curried at surface as le m n).

leDesc : Hoas

leElim

leElim: prelude Le eliminator with curried-motive adapter — leElim K P Pz Ps m n pf discharges pf : le m n against motive P : (m n : nat) -> le m n -> U(K) with branches for leZ / leSS. Internally adapts the Σ-indexed motive of LeDT.elim.

leElim : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas

leInjSS

leInjSS: injectivity of leSS — leInjSS m n pf : Le m n given pf : Le (suc m) (suc n). leElim at motive λm' n' _. Le (predNat m') (predNat n'); leZ fills via leZ ∘ predNat, leSS fills with the recursive witness directly (via β on predNat (suc _)).

leInjSS : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, leSuccSucc

leRefutSuccZero

leRefutSuccZero: refutation of Le (suc m) zero — leElim at motive λm' n' _. natCaseU unit (natCaseU void unit n') m'; both leZ and leSS case targets collapse to unit, while the refutation target at (suc m, 0) collapses to void.

leRefutSuccZero : Hoas -> Hoas -> Hoas  -- m, leProof

leSS

leSS: prelude Le step constructor (s≤s) — leSS lemn : Le (suc m) (suc n) for lemn : Le m n; m, n inferred. Lifts ≤-witnesses through simultaneous successor.

leSS : Hoas -> Hoas  -- lemn

leZ

leZ: prelude Le base constructor (z≤n) — leZ : Le 0 n; bound n inferred. Decidability witness for decideLeNat 0 n.

leZ : Hoas

leafOrnament

leafOrnament: constructor for a leaf functional ornament — a refinement of a primitive HOAS type former (one with _htag ≠ "mu") carrying Nix-meta forget : Refined → Base and section : Base → Refined. The leaf case is the literature-faithful specialisation of Dagand–McBride 2014 (JFP) functional ornaments to type formers without a μ-encoded description. The canonical instance is thunkOrnament.

leafOrnament : { primitive : HoasType, forget : Refined -> Base, section : Base -> Refined, sectionProof? : Refined -> Bool, meta? : Attrs } -> LeafOrnament

leafOrnamentDiagnosticRecords

leafOrnamentDiagnosticRecords: total structured diagnostics for a candidate leaf-ornament spec — codes leaf.invalid-spec | leaf.missing-{primitive,forget,section} | leaf.invalid-{primitive,forget,section,section-proof}.

leafOrnamentDiagnosticRecords : Attrs -> [Diagnostic]

leafOrnamentDiagnostics

leafOrnamentDiagnostics: human-readable text forms of leafOrnamentDiagnosticRecords for surfacing in error messages and test assertions.

leafOrnamentDiagnostics : Attrs -> [String]

let_

let: HOAS let binding — let_ name ty val body builds let name : ty = val in body with body a Nix function receiving the bound variable._

let_ : String -> Hoas -> Hoas -> (Hoas -> Hoas) -> Hoas

Used internally by eliminator wrappers (ind, listElim, sumElim) to bind motive / base / step at their required types before the application spine, making each subterm inferable. User code typically uses let_ to share subexpressions or to name intermediate values for clarity.

level

level: HOAS universe-level type former — inhabits U(0); lets users quantify over universes via forall "k" level (k: …) and build level expressions inline.

level : Hoas

levelMax

levelMax: HOAS Level join — levelMax l m produces max(l, m); the semilattice operation used by descArg / descPi and the universe of dependent products.

levelMax : Hoas -> Hoas -> Hoas

levelSuc

levelSuc: HOAS Level successor — levelSuc l produces l + 1; used to build closed level expressions and inside congSuc for Eq-on-Level transport.

levelSuc : Hoas -> Hoas

levelZero

levelZero: HOAS Level constant 0 — the base universe level; combines with levelSuc / levelMax to form arbitrary closed level expressions.

levelZero : Hoas

listDesc

listDesc: prelude List description constructor — listDesc A produces the two-summand description descRet + descArg A (_: descRec descRet) of List A.

listDesc : Hoas -> Hoas

listElim

listElim: HOAS list eliminator wrapper — listElim k A P N C xs runs ListDT.elim k A after binding motive / nil-branch / cons-step at their required types.

listElim : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- k, A, motive, onNil, onCons, scrut

The cons step has type ∀h:A. ∀t:listOf A. ∀_:P t. P (cons h t) — the inductive hypothesis is the recursive call's result. For constant motives use tc.verified.matchList. The level argument threads into the motive's codomain universe.

listOf

listOf: HOAS list type former — listOf elemTy is μ Unit listDesc tt at element type elemTy; the description-derived counterpart to Nix-native lists.

listOf : Hoas -> Hoas

litVal

litVal: closed-Val splice — litVal v reflects a closed kernel Val into HOAS without structural reconstruction; eval ρ (mkLitVal v) = v independent of ρ. O(1) Val→HOAS lift, contrasted with embedTm (quote 0 v) which is O(size v).

litVal : Val -> Hoas

Splice in the sense of two-level type theory (Kovács, POPL 2024; Annenkov–Capriotti–Kraus–Sattler 2019): reflects a value from the semantic domain back into syntax with eval as the identity. Sound iff the carried Val is closed — eval discards the environment, so any free de Bruijn level would never resolve.

The canonical Val→HOAS lift in the bridge; replaces the embedTm (quote 0 v) composition when v will only be re-evaluated.

lower

lower: depth-parameterised HOAS-to-Tm compiler — lower depth h converts a HOAS term to its de Bruijn Tm representation; depth is the binding level at the call site.

lower : Int -> Hoas -> Tm

The principal HOAS-side compilation entry. Binding chains are lowered iteratively via genericClosure for stack safety to 8000+ depth. Use directly when controlling the binding depth (e.g. when re-lowering an open HOAS subterm). For the closed-term case, prefer elab which fixes depth = 0.

maxSucDom

maxSucDom: Level-max-suc transport — proof of ∀a b. Eq Level (max a b) b -> Eq Level (max a (suc b)) (suc b); lifts max-bound witness through suc on the right operand.

maxSucDom : Hoas

maybe

maybe: HOAS optional type — maybe inner is Sum inner Unit; left payload carries a value, right marks absence.

maybe : Hoas -> Hoas

mu

mu: ⊤-slice inductive carrier — alias for muI unitPrim D i; the unit-indexed special case used by prelude datatypes like nat, list, bool.

mu : Hoas -> Hoas -> Hoas  -- D, i

nat

nat: HOAS Nat type former — generated by NatDT.T from the macro-derived natural-number datatype; serves as the index sort for vector / list-length families.

nat : Hoas

natCaseU

natCaseU: nat-case at the universe level — natCaseU A B is λn:nat. case n { zero => A; succ _ => B; }; built on descInd nat.D with sum-branching on the per-constructor payload.

natCaseU : Hoas -> Hoas -> Hoas  -- zeroBranch, succBranch

The discriminator's result type is U(0) regardless of scrutinee; the inductive hypothesis is discarded since discrimination is value-shape-driven, not recursive. Used by vhead to make the vnil/vcons branches target different types (unit vs the element type), and by absurdFin0 to target the goal type at zero and Unit at succ.

natDesc

natDesc: prelude Nat description — descRet + descRec descRet; the canonical two-summand description of natural numbers as zero + succ(Nat).

natDesc : Hoas

natLit

natLit: Nix integer to HOAS Nat — natLit n builds succ^n zero as a HOAS term; convenience wrapper around iterated succ application.

natLit : Int -> Hoas

natPredCase

natPredCase: nat-case with predecessor-dependent succ branch — natPredCase A n returns unit at zero and vec A m at succ m; generalises natCaseU to payload-dependent succ cases.

natPredCase : Hoas -> Hoas  -- elemTy

Used by vtail to build the vecElim motive P n xs = natPredCase A n so the vnil branch targets unit (filled by tt) and the vcons branch targets vec A pred (filled by the tail). Implementation extracts the predecessor via fst_ r on the inr summand.

natToLevel

natToLevel: meta-level integer-to-Level helper — natToLevel n produces levelSuc^n levelZero; throws on non-Int input; emits closed Level syntax only.

natToLevel : Int -> Hoas

nil

nil: HOAS empty-list constructor — nil : listOf A; element type inferred from the expected type.

nil : Hoas

no

no: negative decidability witness — no P r : dec P for a refutation r : not P. Routes through the right injection of P ⊎ ¬ P.

no : Hoas -> Hoas -> Hoas  -- P, refutation

not

not: propositional negation — not P := P → ⊥ per HoTT Book, section 1.7. Elaborates to a pi with void codomain.

not : Hoas -> Hoas

nothing

nothing: HOAS Maybe none-injection — nothing innerTy is inr tt : maybe innerTy.

nothing : Hoas -> Hoas  -- innerTy

opaqueLam

opaqueLam: HOAS opaque-lambda wrapper — opaqueLam nixFn piHoas packages a non-HOAS Nix function with its declared Π-type; the kernel treats the body as an unverified trust boundary.

opaqueLam : (Any -> Any) -> Hoas -> Hoas

Use only when the body cannot be expressed as HOAS — e.g. wrapping a recursion-irregular helper produced outside the kernel. The elaborator emits mkOpaqueLam; the type-checker cannot recover the body's HOAS shape, so it accepts the declared piHoas without re-validation. Prefer verifiedFn from tc.verified when the body IS expressible as HOAS — that path keeps body verification.

or_

or: propositional disjunction — or_ P Q := P + Q per HoTT Book, section 1.7. Trailing underscore avoids the Nix or keyword in identifier position (mirrors true_ / false_)._

or_ : Hoas -> Hoas -> Hoas

ornArgInsert

ornArgInsert: argInsert-node spec for ornI.node — inserts a fresh arg S field absent from the base description; body binds the inserted witness recursively.

ornArgInsert : Tm -> (Tm -> OrnNode) -> { tag = "argInsert"; S; body }

ornArgKeep

ornArgKeep: argKeep-node spec for ornI.node — keeps a base descArg S body field unchanged in the ornament; body re-binds the same s : S recursively.

ornArgKeep : Tm -> (Tm -> OrnNode) -> { tag = "argKeep"; S; body }

ornBuild

ornBuild: build the ornamented value at index i from baseValue by invoking F.section; the canonical entry point for ornament construction from a base witness.

ornBuild : FunctionalOrnament -> Tm -> Tm -> Tm

ornCompose

ornCompose: vertical composition of ornaments — given inner : I -> J and outer : J -> K, produce outer ∘ inner : I -> K; sequential refinement.

ornCompose : Ornament -> Ornament -> Ornament  -- outer, inner

ornDesc

ornDesc: compile an Ornament to its annotated Desc J term — the levitated description of the ornamented datatype, ready for muI / interpD.

ornDesc : Ornament -> Tm  -- Desc J

ornForget

ornForget: produce the forgetting morphism mu (ornDesc O) ~> mu (baseD O), mapping every ornamented value back to its underlying base-description value.

ornForget : Ornament -> Tm  -- J -> ornMu -> baseMu

ornI

ornI: master constructor of an Ornament over a base description, packaging { I, J, erase, baseD, node } and optional level/meta into the canonical ornament record consumed by ornDesc / ornMu / ornForget.

ornI : { I, J, erase, baseD, node, level?, meta? } -> Ornament

ornId

ornId: identity ornament on D : Desc I — forget is the identity at every index; the unit of ornCompose. Recovers D as its own ornament.

ornId : Tm -> Tm -> Ornament  -- I, D

ornIndexProof

ornIndexProof: extract the indexProof slot of a functional ornament — the proof i -> baseValue -> erase (chooseIndex i baseValue) ≡ i certifying the section commutes with forget.

ornIndexProof : FunctionalOrnament -> (Tm -> Tm -> Tm)

ornLiftFold

ornLiftFold: alias for ornPullback specialised to folds — composes a base fold with ornForget so it runs on ornamented carriers without re-deriving the algebra.

ornLiftFold : Ornament -> (Tm -> Tm) -> Tm -> Tm  -- resultTy, baseFold -> lifted

ornLiftProducer

ornLiftProducer: lift a base producer baseFn through a functional ornament F — run the producer on the base input, then build the ornamented output via F.section.

ornLiftProducer : FunctionalOrnament -> (Tm -> Tm) -> Tm -> Tm -> Tm

ornLiftTransform

ornLiftTransform: lift a base transform through paired input/output functional ornaments — forget the ornamented input, run the base transform, build the ornamented output.

ornLiftTransform : { input : OrnLike, output : FunctionalOrnament, fn } -> Tm -> Tm -> Tm -> Tm

ornMu

ornMu: build the ornamented mu at index j, i.e. muI J (ornDesc O) j — the carrier type of values living over the ornament at that index.

ornMu : Ornament -> Tm -> Tm  -- index in J yields kernel type

ornPiKeep

ornPiKeep: piKeep-node spec for ornI.node — keeps a Π-quantified field over S; branch supplies the base/ornament index functions and proof, defaulting to identity.

ornPiKeep : Tm -> (Tm | { baseF, ornF, proof }) -> OrnNode -> { tag = "piKeep"; S; tail; baseF; ornF; proof; l }

ornPlus

ornPlus: plus-node spec for ornI.node — sum of two ornament arms left and right, mirroring descPlus at the ornament level.

ornPlus : OrnNode -> OrnNode -> { tag = "plus"; left; right }

ornPullback

ornPullback: transport a base program baseFn : I -> baseMu -> R(i) along ornForget, yielding the same program over ornamented inputs at every J index.

ornPullback : Ornament -> (Tm -> Tm) -> Tm -> Tm  -- resultTy, baseFn -> lifted

ornRec

ornRec: rec-node spec for ornI.node — a recursive child at index j with proof erase j ≡ baseIndex and a tail ornament for the remainder of the constructor.

ornRec : Tm -> (Tm | { proof, baseIndex }) -> OrnNode -> { tag = "rec"; j; proof; baseIndex; tail }

ornRet

ornRet: ret-node spec for ornI.node — terminates an ornament arm at index j in J with a base-index witness baseIndex and proof erase j ≡ baseIndex.

ornRet : Tm -> Tm -> Tm -> { tag = "ret"; j; proof; baseIndex }

ornSection

ornSection: extract the section builder from a functional ornament — the function i -> baseValue -> ornamentedValue that realises the section morphism.

ornSection : FunctionalOrnament -> (Tm -> Tm -> Tm)

ornTargetIndex

ornTargetIndex: extract the chooseIndex slot of a functional ornament — the function i -> baseValue -> J that picks the ornamented index for each base input.

ornTargetIndex : FunctionalOrnament -> (Tm -> Tm -> Tm)

ornament

ornament: master surface — given a monomorphic generated DataSpec (base) and a constructor-by-constructor spec, produce the ornamented Datatype plus forget morphism.

ornament : DataSpec -> OrnamentSpec -> Datatype

ornamentDiagnosticRecords

ornamentDiagnosticRecords: total structured diagnostics covering every surface error in an ornament spec — missing constructors, unknown arms, malformed fields, out-of-order keeps.

ornamentDiagnosticRecords : DataSpec -> OrnamentSpec -> [Diagnostic]

ornamentDiagnostics

ornamentDiagnostics: human-readable text forms of ornamentDiagnosticRecords for surfacing in error messages and test assertions.

ornamentDiagnostics : DataSpec -> OrnamentSpec -> [String]

pair

pair: HOAS Σ-pair introduction — pair fst snd packages two HOAS values; the surrounding type annotation pins which Σ-type the pair inhabits.

pair : Hoas -> Hoas -> Hoas

path

path: kernel-primitive Path type — opaque Nix path axiomatised at the kernel level; literal-only entry via pathLit.

path : Hoas

pathLit

pathLit: HOAS Path-literal marker — placeholder term checkable against path; the Nix path is not embedded in the kernel term.

pathLit : Hoas

piField

piField: Π-typed field declarator — piField name sort body declares a function-typed field where every element of sort indexes into the body description.

piField : String -> Hoas -> (Hoas -> Hoas) -> { name; sort; body; pi; }

piFieldD

piFieldD: dependent Π-typed field — piFieldD extends piField with the ability for the body to depend on prior constructor fields.

piFieldD : String -> Hoas -> (Hoas -> Hoas -> Hoas) -> { name; sort; body; pi; indexFn; }

plicity

Plicity tag namespace: explicit/implicit values + predicates.

{ explicit : Plicity; implicit : Plicity; isPlicity : Any -> Bool; isImplicit : Plicity -> Bool; }

plus

plus: ⊤-slice description sum — alias for plusI unitPrim 0 A B; the standard form for combining prelude descriptions like nat = retI + recI(retI).

plus : Hoas -> Hoas -> Hoas

predNat

predNat: saturating Nat predecessor — predNat zero ≡ zero, predNat (suc m) ≡ m. Built via ind with constant nat motive. Consumed by eqInjSucc and leInjSS.

predNat : Hoas  -- closed function nat -> nat

product

product: HOAS named single-constructor μ-datatype — product name [H.field …] is sugar for datatype name [(con name fields)]; returns the full DataSpec so deriveSchema/deriveDescriptor and validateValue work unchanged.

product : String -> [Field] -> DataSpec

The named parallel to record (anonymous, .T-only) and variant (n-con sum). The single constructor's name is the type name, since a product has no constructor to disambiguate. Fields project flat, with no inner value wrapper. Use when the domain type has a stable user-supplied name and consumers need the full DataSpec (.T, .cons, .<name> ctor, .elim).

recField

recField: recursive-field declarator — recField name indexFn declares a recursive position whose target index is computed from prior fields.

recField : String -> (Hoas -> Hoas) -> { name; indexFn; recursive; }

Marks the field as a recursive child via _recursive = true, routing through descRec rather than descArg in the description-emission step. The indexFn extracts the target index from prior fields, supporting indexed datatypes whose recursive children reference different indices.

recFieldAt

recFieldAt: universe-polymorphic recursive-field declarator — recFieldAt name level indexFn with explicit level for the recursive position.

recFieldAt : String -> Level -> (Hoas -> Hoas) -> { name; indexFn; recursive; level; }

record

record: HOAS record type — record [{name; type}…] builds a mono-constructor μ-datatype whose single constructor takes the listed fields in order; surface for v.field projection.

record : [{ name : String; type : Hoas; }] -> Hoas

Compiled to a mono-constructor μ-datatype carrying _dtypeMeta with one constructor named mk whose fields match the input list. The type's canonical name is Record{fieldName1, …} sorted alphabetically. Use v.field recordTy "name" record to project a field by name; the eliminator is derived once and reused across projections.

refinementPred

refinementPred: Σ-encoded refinement-predicate carrier refinementPred dom predFn = Σ (x : dom) (Dec (predFn x)). McBride & McKinna 2004 'The view from the left'. predFn is a Nix-meta Hoas -> Hoas predicate following the surface convention of sigma / forall / lam. Inhabitants pair a value with a decision proof; the decision procedure is supplied at the value level rather than encoded in the type.

refinementPred : Hoas -> (Hoas -> Hoas) -> Hoas  -- domain, predFn

refl

refl: HOAS reflexivity introduction for EqDT — emitted in check-mode against a goal EqDT A a a; the elaborator handles the level/index inference.

refl : Hoas

reflDT

reflDT: prelude equality reflexivity — reflDT A a : eqDT A a a; the canonical inhabitant of the diagonal.

reflDT : Hoas -> Hoas -> Hoas  -- A, value

reifyLevel

reifyLevel: HOAS Level → kernel Level Tm — converts a HOAS-side level expression (Int, level term, or already-reified Tm) to the kernel's canonical Level representation.

reifyLevel : Level -> Tm

retI

retI: indexed retI-constructor — retI I k j builds a Desc^k I leaf returning index j; level-polymorphic over k.

retI : Hoas -> Level -> Hoas -> Hoas  -- I, k, targetIndex

sigma

sigma: HOAS Σ-type former — sigma name fst body builds Σ(name:fst). body; the dependent-pair counterpart to forall.

sigma : String -> Hoas -> (Hoas -> Hoas) -> Hoas

Stack-safe like forall (iterative genericClosure elaboration). Pairs enter via pair, project via fst_ / snd_. For records of more than two fields, prefer record which is encoded as a mono-constructor μ-datatype with named projections via v.field.

signsDiffer

signsDiffer: no-confusion refutation (m n : Nat) -> Eq IntZ (pos m) (negSucc n) -> void. McBride 2000 PhD, section 3.5 discriminator-motive technique applied to the IntZ sign discriminator (unit on pos, void on negSucc) plus bootJ transport.

signsDiffer : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, e

signsDifferRev

signsDifferRev: symmetric no-confusion refutation (m n : Nat) -> Eq IntZ (negSucc m) (pos n) -> void. Same discriminator-motive technique as signsDiffer with the pos / negSucc targets swapped.

signsDifferRev : Hoas -> Hoas -> Hoas -> Hoas  -- m, n, e

snd_

snd: HOAS Σ-pair second projection — extracts the right component; reduces by π₂ during normalisation when the argument is a pair._

snd_ : Hoas -> Hoas

sourceMapOf

sourceMapOf: HOAS surface → SourceMap walker — produces a structural map from the HOAS term's positions to source-form metadata; consumed by the diagnostic shell to associate errors with source positions.

sourceMapOf : Hoas -> SourceMap

squash

squash: HOAS propositional truncation — squash A is the type ‖A‖ whose elements are all conv-equal; collapses A's content to mere inhabitation.

squash : Hoas -> Hoas

Two squashIntro _ values inhabiting the same squash A are conv-equal by definitional irrelevance — equality holds without inspecting payloads. Use to express subsingleton propositions or to enforce proof-irrelevance on otherwise relevant data.

squashElim

squashElim: HOAS truncation eliminator — squashElim A B f x lifts f : A -> squash B over x : squash A; restricted to squash-typed motives so irrelevance is preserved.

squashElim : Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- A, B, f, x

Restricted to motives whose target is squash B — eliminating out of a squash into a relevant type is forbidden (would violate irrelevance). For relevant-target elimination, the only path is constructing a derivation that requires no inspection of the squashed value.

squashIntro

squashIntro: HOAS truncation introduction — squashIntro a wraps a : A into squash A; the resulting witness ignores the underlying value under conv.

squashIntro : Hoas -> Hoas

strEq

strEq: HOAS kernel string equality — strEq a b produces a bool HOAS term; reflects the mkStrEq primitive of the kernel.

strEq : Hoas -> Hoas -> Hoas

string

string: kernel-primitive String type — axiomatised; literals enter via stringLit, equality is decidable via strEq.

string : Hoas

stringLit

stringLit: HOAS String literal — stringLit s lifts a Nix string to a kernel stringLit Tm checkable against string.

stringLit : String -> Hoas

succ

succ: HOAS Nat successor — succ n builds n + 1; introduces nat at the descRec descRet summand.

succ : Hoas -> Hoas

sum

sum: HOAS coproduct type former — sum A B builds A + B via SumDT.T at the implicit base level; inhabitants enter via inl / inr.

sum : Hoas -> Hoas -> Hoas

sumDesc

sumDesc: prelude Sum description constructor — sumDesc A B produces the two-summand description descArg A (_: descRet) + descArg B (_: descRet) of Sum A B.

sumDesc : Hoas -> Hoas -> Hoas

sumElim

sumElim: HOAS sum eliminator wrapper — sumElim k A B P L R s runs SumDT.elim k at the base universe level; L and R are dependent on the injected payload.

sumElim : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- k, A, B, motive, onLeft, onRight, scrut

Calls sumElimAt levelZero … for the homogeneous-level common case. For sums constructed via inlAt / inrAt at a non-zero level, use sumElimAt directly with the matching level. For constant motives use tc.verified.matchSum.

sup

sup: HOAS W-type constructor sup s t — supplies the node-shape s and the recursive-children family t : pos s → W.

sup : Hoas -> Hoas -> Hoas

surfacePlicity

Read the plicity sidecar, defaulting to explicit.

Any -> Plicity

thunk

thunk: generic deepSeq-safe carrier type former — thunk a is { _tag = "Thunk"; _force = _: a }. Lazy structural check: walker verifies _force is a closure but does NOT invoke it; inner-type validation runs post-forget. Forget map: t._force null. Use as a payload type wherever values must survive trampoline deepSeq while remaining recoverable.

thunk : Hoas -> Hoas

thunkOrnament

thunkOrnament: derived leaf-functional-ornament constructor for H.thunk inner with forget = forceThunk and section = mkThunk. The functional ornament induced by forceThunk : Thunk A → A per Dagand–McBride 2014 (JFP), section 3, specialised to the primitive Thunk carrier from fx.state.thunk.

thunkOrnament : HoasType -> LeafOrnament

trans

trans: User-Eq transitivity — proof of ∀A x y z. Eq A x y -> Eq A y z -> Eq A x z; one J application transporting pxy along pyz. Chains with cong to build diagram-chase witnesses without expanding either equality's RHS through the kernel.

trans : Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- A, x, y, z, pxy, pyz

true_

true: HOAS Bool constructor true — generated by BoolDT; corresponds to the right summand of bool-as-Sum Unit Unit._

true_ : Hoas

tryAlgOrn

tryAlgOrn: total constructor — returns { ok, diagnostics, value? } where value is the algOrn-built ornament when ok, otherwise diagnostics-only.

tryAlgOrn : Attrs -> { ok : Bool, diagnostics : [Diagnostic], value? : Ornament }

tryFunctionalOrnament

tryFunctionalOrnament: total constructor — returns { ok, diagnostics, value? } where value is the built functional ornament when ok, otherwise diagnostics-only.

tryFunctionalOrnament : Attrs -> { ok : Bool, diagnostics : [Diagnostic], value? : FunctionalOrnament }

tryLeafOrnament

tryLeafOrnament: total constructor — returns { ok, diagnostics, value? } where value is the built leaf ornament when ok, otherwise diagnostics-only.

tryLeafOrnament : Attrs -> { ok : Bool, diagnostics : [Diagnostic], value? : LeafOrnament }

tryOrnament

tryOrnament: total constructor — returns { ok, diagnostics, value? } where value is the built ornamented datatype when ok, otherwise diagnostics-only.

tryOrnament : DataSpec -> OrnamentSpec -> { ok : Bool, diagnostics : [Diagnostic], value? : Datatype }

tt

tt: HOAS unit value — the unique inhabitant of unit; ⊤-slice convention places this at every retI leaf of description scaffolding.

tt : Hoas

u

u: HOAS universe former — u level builds U(level), the universe of types at the given level; level accepts a Nix Int, a HOAS Level term, or a kernel Tm.

u : Level -> Hoas

unit

unit: HOAS unit type — alias for the kernel-primitive unitPrim; the ⊤-slice index sort for description machinery and refinement bound markers.

unit : Hoas

validateAlgOrn

validateAlgOrn: total predicate { ok, diagnostics } over a candidate algOrn spec — checks every algebra arm against its description shape without throwing.

validateAlgOrn : Attrs -> { ok : Bool, diagnostics : [Diagnostic] }

validateFunctionalLaws

validateFunctionalLaws: total predicate { ok, diagnostics } over a functional ornament's law-check bundle; reports which checks failed without throwing.

validateFunctionalLaws : FunctionalOrnament -> { ok : Bool, diagnostics : [Diagnostic] }

validateFunctionalOrnament

validateFunctionalOrnament: total predicate over candidate functional-ornament specs returning { ok, diagnostics }; never throws, intended for upstream try* and surface validators.

validateFunctionalOrnament : Attrs -> { ok : Bool, diagnostics : [Diagnostic] }

validateLeafOrnament

validateLeafOrnament: total predicate { ok, diagnostics } over a candidate leaf-ornament spec; rejects μ-encoded primitives, already-ornamented primitives, and missing/malformed forget/section/sectionProof fields.

validateLeafOrnament : Attrs -> { ok : Bool, diagnostics : [Diagnostic] }

validateOrnament

validateOrnament: total predicate { ok, diagnostics } over (base, spec) for the user-facing ornament surface; never throws.

validateOrnament : DataSpec -> OrnamentSpec -> { ok : Bool, diagnostics : [Diagnostic] }

variant

variant: HOAS tagged-union type — variant [{tag; type}…] builds an n-constructor μ-datatype whose tags become single-field constructor names.

variant : [{ tag : String; type : Hoas; }] -> Hoas

Each branch becomes a single-field constructor named after the tag, so a value { _tag = "Left"; value = v; } walks via the recovery _tag branch finding constructor "Left" and reading its value field. The canonical type name is Variant{tag1, tag2, …} with tags sorted alphabetically.

variantInject

variantInject: HOAS variant-value injection — variantInject ty tag inner produces the nested inl/inr chain that injects inner into tag's branch of ty.

variantInject : Hoas -> String -> Hoas -> Hoas  -- variantTy, tag, value

vcons

vcons: prelude Vec cons constructor — vcons x xs prepends x : A to xs : vec A m, producing vec A (succ m); element type and predecessor inferred.

vcons : Hoas -> Hoas -> Hoas  -- head, tail

vec

vec: prelude Vec type family — forwarder for app VecDT.T A; app (vec A) n is the type of vectors of length n carrying elements of type A.

vec : Hoas -> Hoas  -- elemTy

vecDesc

vecDesc: prelude Vec description — forwarder for app VecDT.D A; the indexed description of length-indexed vectors over element type A.

vecDesc : Hoas -> Hoas  -- elemTy

vecElim

vecElim: prelude Vec eliminator — vecElim k A P Pn Pc n xs discharges xs : vec A n against motive P : ∀n:nat. vec A n -> U(k).

vecElim : Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas

vhead

vhead: prelude Vec head extractor — vhead A n xs returns the first element of xs : vec A (succ n); eliminator-driven via the natCaseU unit A motive.

vhead : Hoas -> Hoas

vnil

vnil: prelude Vec empty constructor — vnil : vec A zero; element type inferred.

vnil : Hoas

void

void: HOAS empty type — alias for empty / emptyPrim; the initial-object dual of unit, eliminated via absurd.

void : Hoas

vtail

vtail: prelude Vec tail extractor — vtail A n xs returns the tail of xs : vec A (succ n) at type vec A n; eliminator-driven via the natPredCase A motive.

vtail : Hoas -> Hoas

w

w: W-type former — generalised inductive type for trees with arbitrary branching; foundational for encoding finitely-branching datatypes outside the description layer.

w : Hoas -> Hoas -> Hoas  -- shapeTy, posFn

wDesc

wDesc: W-type description forwarder — alias for WDT.D, the description of W-type trees over shape S and position family pos.

wDesc : Hoas -> (Hoas -> Hoas) -> Hoas

wElim

wElim: W-type eliminator forwarder — alias for WDT.elim, the dependent recursor for W-type trees.

wElim : Level -> Hoas -> (Hoas -> Hoas) -> Hoas -> Hoas -> Hoas -> Hoas

withConLabel

withConLabel: attach a surrounding-constructor label to a description-encoding HOAS form — withConLabel label form adds _conLabel = label; conv-irrelevant.

withConLabel : String -> Hoas -> Hoas

Set by the datatype macro at each constructor's spine site, so each summand carries its constructor name. Surfaces through descView's .conLabel field. Orthogonal to withDescLabel (separate slot) so labeling a field-labeled description with a constructor name doesn't overwrite the field's identity.

withDescLabel

withDescLabel: attach a presentation label to a description-encoding HOAS form — withDescLabel label form adds _label = label; conv-irrelevant, idempotent under re-labeling.

withDescLabel : String -> Hoas -> Hoas

Surfaces back through descView's .label field. Used by renderers (pretty-printers, doc generators) to surface field names without affecting type equality — two descriptions differing only in labels are conv-equal. Orthogonal to withConLabel, which lives in a separate _conLabel slot.

yes

yes: positive decidability witness — yes P p : dec P for a proof p : P. Routes through the left injection of P ⊎ ¬ P.

yes : Hoas -> Hoas -> Hoas  -- P, proof

zero

zero: HOAS Nat constructor — the natural-number zero; introduces nat at the descRet summand of natDesc.

zero : Hoas

Sub-namespaces

• _internal

Source

• src/tc/hoas/combinators.nix
• src/tc/hoas/datatype.nix
• src/tc/hoas/decidable.nix
• src/tc/hoas/desc.nix
• src/tc/hoas/forced.nix
• src/tc/hoas/lower.nix
• src/tc/hoas/ornament.nix
• src/tc/hoas/plicity.nix
• src/tc/hoas/source_map.nix