# _indexed Indexed/equality-aligned combinators (`muI`, `piI`, `recI`, `plusI`, `inrAt`, `fieldAt`) consumed by ornament construction and indexed-datatype test fixtures. ## `LiftAt` _LiftAt: HOAS cross-level type former — `LiftAt l m A : U(m)` for `A : U(l)` with `l ≤ m`; bound witness auto-emitted as `mkBootRefl` when convLevel decides `Eq Level (max l m) m`._ ``` LiftAt : Level -> Level -> Hoas -> Hoas -- l, m, A ``` Idempotent at equal levels: `LiftAt l l A ≡ A` (no wrapping when `sameLevelSyntax l l`). Use to transport a type from a lower universe to a higher one without changing inhabitation. For level-polymorphic binders where convLevel cannot decide, use `LiftAtWithEq` and supply the proof explicitly. ## `LiftAtWithEq` _LiftAtWithEq: LiftAt variant carrying an explicit bound-witness — `LiftAtWithEq l m eq A` supplies `eq : Eq Level (max l m) m` when convLevel cannot decide it._ ``` LiftAtWithEq : Level -> Level -> Hoas -> Hoas -> Hoas -- l, m, eq, A ``` ## `consAtExplicit` _consAtExplicit: internal List cons with hidden level + element type supplied explicitly for rigid/raw evaluation sites._ ``` consAtExplicit : Level -> Hoas -> Hoas -> Hoas -> Hoas -- level, elemTy, head, tail ``` ## `datatypeAt` _datatypeAt: universe-polymorphic ⊤-slice datatype — `datatypeAt name level [con …]` emits a datatype at sort level `level`._ ``` datatypeAt : String -> Level -> [Constructor] -> DataSpec ``` ## `datatypePAt` _datatypePAt: universe-polymorphic parametric datatype — `datatypePAt` extends `datatypeP` with explicit sort levels for parameters._ ``` datatypePAt : String -> Level -> [Param] -> (Hoas -> [Constructor]) -> DataSpec ``` ## `descArgAt` _descArgAt: universe-polymorphic descArg — `descArgAt I l k S T` builds the same with explicit sort level `l`._ ``` descArgAt : Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas ``` ## `descArgAtAtI` _descArgAtAtI: fully universe-explicit indexed descArg — `descArgAtAtI iLev I l k S T` threads both the index-universe level and payload sort level._ ``` descArgAtAtI : Level -> Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas ``` ## `descArgAtI` _descArgAtI: indexed descArg with explicit index-universe level — `descArgAtI iLev I k S T` for index types `I : U(iLev)`._ ``` descArgAtI : Level -> Hoas -> Level -> Hoas -> Hoas -> Hoas ``` ## `descArgWithEq` _descArgWithEq: descArgAt variant with explicit bound-witness — supplies the `eq : Eq Level (max l k) k` proof for level-polymorphic positions._ ``` descArgWithEq : Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas ``` ## `descAt` _descAt: universe-polymorphic ⊤-slice description — alias for `descIAt k unitPrim`; descriptions at level `k` over the unit index type._ ``` descAt : Level -> Hoas ``` ## `descI` _descI: indexed description type former — `descI I` builds `Desc I`, the universe of descriptions over index sort `I`; level defaults to 0._ ``` descI : Hoas -> Hoas ``` ## `descIAt` _descIAt: universe-polymorphic indexed description — `descIAt k I` builds `Desc^k I`; the level-omitting `descI` defaults to level 0._ ``` descIAt : Level -> Hoas -> Hoas ``` ## `descIAtAtI` _descIAtAtI: fully universe-explicit indexed description — `descIAtAtI iLev k I` builds `Desc^k I` for `I : U(iLev)`._ ``` descIAtAtI : Level -> Level -> Hoas -> Hoas ``` ## `descIAtI` _descIAtI: indexed description with explicit index-universe level — `descIAtI iLev I` builds `Desc I` for `I : U(iLev)`._ ``` descIAtI : Level -> Hoas -> Hoas ``` ## `descPiAt` _descPiAt: universe-polymorphic ⊤-slice descPi — `descPiAt l k S D` with explicit sort level `l`._ ``` descPiAt : Level -> Level -> Hoas -> Hoas -> Hoas ``` ## `descPiWithEq` _descPiWithEq: descPiAt variant with explicit bound-witness — supplies the `eq : Eq Level (max l k) k` proof for level-polymorphic descriptions._ ``` descPiWithEq : Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas ``` ## `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; } ``` ## `fieldAtWithEq` _fieldAtWithEq: fieldAt variant carrying an explicit bound-witness — supplies the `eq : Eq Level (max l k) k` proof for level-polymorphic positions._ ``` fieldAtWithEq : String -> Level -> Hoas -> Hoas -> { name; type; level; eq; } ``` ## `fieldDAt` _fieldDAt: universe-polymorphic dependent-field declarator — combines `fieldAt`'s explicit level with `fieldD`'s index dependence._ ``` fieldDAt : String -> Level -> Hoas -> (Hoas -> Hoas) -> { name; type; level; indexFn; } ``` ## `fieldDAtWithEq` _fieldDAtWithEq: universe-polymorphic dependent-field with explicit bound-witness — combines fieldDAt with explicit eq._ ``` fieldDAtWithEq : String -> Level -> Hoas -> Hoas -> (Hoas -> Hoas) -> { name; type; level; eq; indexFn; } ``` ## `inlAt` _inlAt: universe-polymorphic left-injection — `inlAt v` builds `Left v : Sum A B`; level, leftTy, rightTy inferred._ ``` inlAt : Hoas -> Hoas -- value ``` ## `inlAtExplicit` _inlAtExplicit: internal Sum left-injection with hidden parameters supplied explicitly for raw evaluation sites._ ``` inlAtExplicit : Level -> Hoas -> Hoas -> Hoas -> Hoas -- level, leftTy, rightTy, value ``` ## `inrAt` _inrAt: universe-polymorphic right-injection — `inrAt v` builds `Right v : Sum A B`; level, leftTy, rightTy inferred._ ``` inrAt : Hoas -> Hoas -- value ``` ## `inrAtExplicit` _inrAtExplicit: internal Sum right-injection with hidden parameters supplied explicitly for raw evaluation sites._ ``` inrAtExplicit : Level -> Hoas -> Hoas -> Hoas -> Hoas -- level, leftTy, rightTy, value ``` ## `liftAt` _liftAt: HOAS lift introduction — `liftAt l m A a` produces `LiftAt l m A` from `a : A`; idempotent at equal levels (no introducer when `l = m`)._ ``` liftAt : Level -> Level -> Hoas -> Hoas -> Hoas -- l, m, A, a ``` ## `liftAtWithEq` _liftAtWithEq: explicit-witness lift introduction — `liftAtWithEq l m eq A a` with the caller-provided `eq` term derived via `congSuc` / `maxSucDom` for level-polymorphic positions._ ``` liftAtWithEq : Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas -- l, m, eq, A, a ``` ## `lowerAt` _lowerAt: HOAS lift elimination — `lowerAt l m A x` extracts `a : A` from `x : LiftAt l m A`; β-reduces with `liftAt`, idempotent at equal levels._ ``` lowerAt : Level -> Level -> Hoas -> Hoas -> Hoas -- l, m, A, x ``` ## `lowerAtWithEq` _lowerAtWithEq: explicit-witness lift elimination — `lowerAtWithEq l m eq A x` mirroring `liftAtWithEq`; uses the supplied `eq` to discharge the level bound._ ``` lowerAtWithEq : Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas -- l, m, eq, A, x ``` ## `muI` _muI: indexed inductive carrier former — `muI I D i` builds `μ I D i`, the value type at index `i` of the description `D : Desc I`._ ``` muI : Hoas -> Hoas -> Hoas -> Hoas -- I, D, i ``` The carrier is constructed by `descCon D i d` from interpreted payloads. Eliminated via `descInd D Q step i x` for indexed induction. The kernel routes `mu` through the description- rule path, never as a bare `mu` constructor — every `muI` flow eventually applies the encoder cascade. ## `muIAtI` _muIAtI: indexed inductive carrier with explicit index-universe level — `muIAtI iLev I D i` builds `μ I D i` for `I : U(iLev)`._ ``` muIAtI : Level -> Hoas -> Hoas -> Hoas -> Hoas ``` ## `nilAtExplicit` _nilAtExplicit: internal List nil with hidden level + element type supplied explicitly for rigid/raw evaluation sites._ ``` nilAtExplicit : Level -> Hoas -> Hoas -- level, elemTy ``` ## `piFieldAt` _piFieldAt: universe-polymorphic Π-typed field — `piFieldAt name level sort body` with explicit level._ ``` piFieldAt : String -> Level -> Hoas -> (Hoas -> Hoas) -> { ... } ``` ## `piFieldAtIndex` _piFieldAtIndex: piFieldAt variant emitting an explicit-target-index — used when the recursive Π must specify the index of the resulting recursive child._ ``` piFieldAtIndex : String -> Level -> Hoas -> (Hoas -> Hoas) -> (Hoas -> Hoas) -> { ... } ``` ## `piFieldAtIndexWithEq` _piFieldAtIndexWithEq: piFieldAtIndex with explicit bound-witness._ ``` piFieldAtIndexWithEq : String -> Level -> Hoas -> Hoas -> (Hoas -> Hoas) -> (Hoas -> Hoas) -> { ... } ``` ## `piFieldAtWithEq` _piFieldAtWithEq: piFieldAt with explicit bound-witness — supplies the `eq` proof for level-polymorphic positions._ ``` piFieldAtWithEq : String -> Level -> Hoas -> Hoas -> (Hoas -> Hoas) -> { ... } ``` ## `piFieldDAt` _piFieldDAt: universe-polymorphic dependent Π-typed field — combines piFieldAt with piFieldD's dependence on prior fields._ ``` piFieldDAt : String -> Level -> Hoas -> (Hoas -> Hoas -> Hoas) -> { ... } ``` ## `piFieldDAtIndex` _piFieldDAtIndex: piFieldDAt variant emitting an explicit-target-index._ ``` piFieldDAtIndex : String -> Level -> Hoas -> (Hoas -> Hoas -> Hoas) -> (Hoas -> Hoas -> Hoas) -> { ... } ``` ## `piFieldDAtIndexWithEq` _piFieldDAtIndexWithEq: piFieldDAtIndex with explicit bound-witness._ ``` piFieldDAtIndexWithEq : String -> Level -> Hoas -> Hoas -> (Hoas -> Hoas -> Hoas) -> (Hoas -> Hoas -> Hoas) -> { ... } ``` ## `piFieldDAtWithEq` _piFieldDAtWithEq: universe-polymorphic dependent Π-typed field with explicit bound-witness._ ``` piFieldDAtWithEq : String -> Level -> Hoas -> Hoas -> (Hoas -> Hoas -> Hoas) -> { ... } ``` ## `piI` _piI: indexed piI-constructor — `piI I k S f D` builds a description that quantifies over `S` then continues with `D` parametrised by the chosen element via `f : S -> Tm` (the index function)._ ``` piI : Hoas -> Level -> Hoas -> Hoas -> Hoas -> Hoas -- I, k, sort, indexFn, continuation ``` ## `piIAt` _piIAt: universe-polymorphic piI — `piIAt I l k S f D` builds the same shape as `piI` but with explicit sort level `l` and continuation level `k`, used when level decisions cannot be left to convLevel._ ``` piIAt : Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas ``` ## `piIAtAtI` _piIAtAtI: fully universe-explicit indexed piI — `piIAtAtI iLev I l k S f D` threads the index-universe level and payload sort level._ ``` piIAtAtI : Level -> Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas ``` ## `piIAtI` _piIAtI: indexed piI with explicit index-universe level — `piIAtI iLev I k S f D` for descriptions over `I : U(iLev)`._ ``` piIAtI : Level -> Hoas -> Level -> Hoas -> Hoas -> Hoas -> Hoas ``` ## `piIWithEq` _piIWithEq: piIAt variant carrying an explicit bound-witness — `piIWithEq I l k S f eq D` supplies the `eq : Eq Level (max l k) k` proof when the elaborator cannot auto-decide via `convLevel`._ ``` piIWithEq : Hoas -> Level -> Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas ``` ## `plusI` _plusI: indexed description sum — `plusI I k A B` builds `A + B` at index sort `I` and level `k`; both `A` and `B` must share index sort and level._ ``` plusI : Hoas -> Level -> Hoas -> Hoas -> Hoas ``` ## `plusIAtI` _plusIAtI: indexed description sum with explicit index-universe level — `plusIAtI iLev I k A B` for descriptions over `I : U(iLev)`._ ``` plusIAtI : Level -> Hoas -> Level -> Hoas -> Hoas -> Hoas ``` ## `recI` _recI: indexed recI-constructor — `recI I k j D` adds a recursive child at target index `j` to the continuation description `D`; the recursive position contributes payload at `μ I D' j` for the inner D'._ ``` recI : Hoas -> Level -> Hoas -> Hoas -> Hoas -- I, k, targetIndex, continuation ``` ## `recIAtI` _recIAtI: indexed recI-constructor with explicit index-universe level — `recIAtI iLev I k j D` for `I : U(iLev)`._ ``` recIAtI : Level -> Hoas -> Level -> Hoas -> Hoas -> Hoas ``` ## `retIAtI` _retIAtI: indexed retI-constructor with explicit index-universe level — `retIAtI iLev I k j` for leaves over `I : U(iLev)`._ ``` retIAtI : Level -> Hoas -> Level -> Hoas -> Hoas ``` ## `sumAt` _sumAt: universe-polymorphic coproduct — `sumAt level A B` builds `A + B` at the given universe level, used when the homogeneous-level `sum` cannot decide the bound witness._ ``` sumAt : Hoas -> Hoas -> Hoas -> Hoas -- level, A, B ``` ## `sumElimAt` _sumElimAt: universe-polymorphic sum eliminator — `sumElimAt level k A B P L R s` runs the sum eliminator at the given universe level, matching `inlAt` / `inrAt` construction._ ``` sumElimAt : Hoas -> Level -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -- level, k, A, B, motive, onLeft, onRight, scrut ```