# 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

```nix
# Π(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
```

## `descCataBool`

_descCataBool: constant-Bool-motive description catamorphism — `descCataBool { D, carrier, onArg }` folds `onArg`'s per-field Boolean decisions over `μ ⊤ D`, conjoining every `descArg` field and recursive child. The non-dependent specialisation of `descInd`._

```
descCataBool : { D : Hoas; carrier : Hoas; onArg : Int -> Hoas -> Hoas -> Hoas } -> Hoas  -- result : carrier -> Bool
```

## `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; }
```

## `fieldAt`

_fieldAt: universe-polymorphic field declarator — `fieldAt name level type` declares a field at an explicit sort level._

```
fieldAt : String -> Level -> Hoas -> { name; type; level; }
```

## `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
```

## `intEq`

_intEq: HOAS kernel int equality — `intEq a b` produces a `bool` HOAS term; reflects the `mkIntEq` primitive (host `==`)._

```
intEq : Hoas -> Hoas -> Hoas
```

## `intLe`

_intLe: HOAS kernel int order — `intLe a b` produces a `bool` HOAS term; reflects the `mkIntLe` primitive (host `<=`)._

```
intLe : Hoas -> Hoas -> Hoas
```

## `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
```

## `justAt`

_justAt: universe-polymorphic Maybe just-injection — `justAt k innerTy v` is `inl v : maybeAt k innerTy`._

```
justAt : Level -> Hoas -> Hoas -> Hoas  -- level, 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
```

## `listOfAt`

_listOfAt: universe-polymorphic list type former — `listOfAt level A` builds `List A` at the given universe level, used when the homogeneous-level `listOf` cannot carry an element type above U(0)._

```
listOfAt : Hoas -> Hoas -> Hoas  -- level, A
```

## `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
```

## `maybeAt`

_maybeAt: universe-polymorphic optional — `maybeAt k inner` is `Sum inner (LiftAt 0 k Unit)` at level k; `maybe` is the level-zero default._

```
maybeAt : Level -> Hoas -> Hoas  -- level, inner
```

## `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
```

## `nothingAt`

_nothingAt: universe-polymorphic Maybe none-injection — `nothingAt k innerTy` is `inr (lift tt) : maybeAt k innerTy`._

```
nothingAt : Level -> Hoas -> Hoas  -- level, 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
```

## `strLen`

_strLen: HOAS kernel string length — `strLen s` produces an `int_` HOAS term; reflects the `mkStrLen` primitive (host string length)._

```
strLen : 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.

## `variantAt`

_variantAt: universe-polymorphic tagged-union — `variantAt k [{tag; type}…]` nests `sumAt k` over branches already at U(k); `variant` is the level-zero default._

```
variantAt : Level -> [{ tag : String; type : Hoas; }] -> Hoas
```

## `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
```

## `variantInjectAt`

_variantInjectAt: universe-polymorphic variant-value injection — `variantInjectAt k ty tag inner` nests `inl/inr` at level k to inject `inner` into `tag`'s branch of `ty`._

```
variantInjectAt : Level -> Hoas -> String -> Hoas -> Hoas  -- level, 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`](/nix-effects/type-checker/hoas/_internal)

## Source

- [`src/tc/hoas/combinators.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/combinators.nix)
- [`src/tc/hoas/datatype.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/datatype.nix)
- [`src/tc/hoas/decidable.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/decidable.nix)
- [`src/tc/hoas/desc.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/desc.nix)
- [`src/tc/hoas/forced.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/forced.nix)
- [`src/tc/hoas/lower.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/lower.nix)
- [`src/tc/hoas/ornament.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/ornament.nix)
- [`src/tc/hoas/plicity.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/plicity.nix)
- [`src/tc/hoas/source_map.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/hoas/source_map.nix)