_internal

Unstable internal surface — boot-sum/boot-eq helpers, kernel-Tm encoders, and indexed-variant scaffolding; prefer SumDT/EqDT-generated forms in user code.

bootEq

bootEq: bootstrap propositional-equality type former at the description layer — bootEq T a b is the kernel-internal Eq used before EqDT is available. Prefer the SumDT/EqDT-generated eq for end-user code.

bootEq : Hoas -> Hoas -> Hoas -> Hoas  -- type, lhs, rhs

bootInl

bootInl: bootstrap left-injection at the description layer — bootInl L R v introduces a boot-sum L R from v : L. Used by the freer-monad-as-description encoding to build μ-values where no SumDT-generated inl applies.

bootInl : Hoas -> Hoas -> Hoas -> Hoas  -- L, R, v

bootInr

bootInr: bootstrap right-injection at the description layer — bootInr L R v introduces a boot-sum L R from v : R. See bootInl.

bootInr : Hoas -> Hoas -> Hoas -> Hoas  -- L, R, v

bootJ

bootJ: bootstrap J-eliminator at the description layer — bootJ T a P b c eq transports b : P a a refl along eq : bootEq T a c to P a c eq. Prefer EqDT-generated j for end-user code.

bootJ : Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- T, a, motive, base, c, eq

bootRefl

bootRefl: bootstrap reflexivity witness at the description layer — checkable against any bootEq T a a. Prefer EqDT-generated refl for end-user code.

bootRefl : Hoas

bootSum

bootSum: bootstrap binary coproduct type former at the description layer — bootSum L R is the kernel-internal Sum used before SumDT is available; arises inside descPlus interpretation.

bootSum : Hoas -> Hoas -> Hoas  -- L, R

bootSumElim

bootSumElim: bootstrap sum eliminator at the description layer — bootSumElim L R P onL onR scrut discharges scrut : bootSum L R to P scrut. Prefer SumDT-generated sumElim for end-user code.

bootSumElim : Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas -> Hoas  -- L, R, motive, onLeft, onRight, scrut

Sub-namespaces

• _encoders
• _forced
• _indexed