Add FORK_STRATEGY.md documenting:
- Purpose: HoTT-compatible kernel extensions (Path types without UIP,
transport, HITs) for polytropos's meta-theory.
- Why kernel-level: library encodings via Quot leak UIP, incompatible
with univalence. Mirrors Cubical Agda's precedent.
- Sync strategy: track upstream leanprover/lean4, merge (not rebase),
preserve HoTT additions on conflict.
- Modification strategy: locality principle (new files under hott/
+ src/kernel/hott/ + src/Init/HoTT/); LEAN4-HTT: tag for modifications
to upstream files; compile-time feature flag (LEAN_HOTT) gates HoTT.
- Patch-series organization for phased primitive additions.
- Forbidden moves: no UIP at kernel level, no Quot.sound dependency for
HoTT reductions, no Classical.choice in HoTT primitives.
Add hott/ directory structure:
- hott/README.md describing the fork-specific directory's purpose.
- hott/design/ for architectural decisions per phase.
- hott/tests/ for HoTT-specific test suites.
No kernel modifications in this phase. Subsequent phases:
Phase 1: Path + Refl + J primitives
Phase 2: transport with computational behavior
Phase 3: HIT support
Phase 4: cubical primitives if needed
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
