# _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`](/nix-effects/type-checker/hoas/_internal/_encoders)
- [`_forced`](/nix-effects/type-checker/hoas/_internal/_forced)
- [`_indexed`](/nix-effects/type-checker/hoas/_internal/_indexed)