_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 element type supplied explicitly for rigid/raw evaluation sites.

consAtExplicit : Hoas -> Hoas -> Hoas -> Hoas  -- 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 element type supplied explicitly for rigid/raw evaluation sites.

nilAtExplicit : Hoas -> Hoas  -- 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