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>
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
quasireducible are also known as lazyreducible.
There is a lot of work to be done.
We still need to revise blast, and add a normalizer for type class
instances. This commit worksaround that by eagerly unfolding
quasireducible.
The theorems are mostly about the interaction between pointed equivalences and pointed homotopies
Some of these theorems were missing for (unpointed) equivalences, so I also added them there
more about pointed truncated types, including pointed sets.
also increase the priority of some basic instances that nat/num/pos_num/trunc_index have 0, 1 and + (in both libraries)
also move the notation + for sum into the namespace sum, to (sometimes) avoid overloading with add
Now the file hardly uses eq.rec explicitly anymore.
Also add the fact that horizontal and vertical inverses of paths are equal
Make one more argument explicit in eq.cancel_left and eq.cancel_right (to make it nicer to write 'apply cancel_right p')
Note: this is important. I proved a quite complicated equivalence with calc, by chaining these
equivalences. Now if I want to know the underlying function of this composite equivalence, I have to
unfold all these instances. Without the abstracts, this took 14 seconds, and afterwards, it took 2
seconds.
After this commit we need some more advanced theorems in init/wf, notably function extenstionality.
For this reason I had to refactor the init folder a little bit.
To keep the init folders in both libraries similar, I did the same refactorization in the standard library, even though that was not required for the standard library
