Layer 3.3a: substantive unit/counit + typed-correctness for adjoint triple
#43 -Commit
391a048dcf
pushed by
max
Axiom debt cleanup: discharge or convert all 99 engine axioms
#42 -Commit
0a7228a8e5
pushed by
max
Refactor Phase 4: Rust ABI v6 → v7 (modal tag unification)
#41 -Commit
567d8722d5
pushed by
max
Refactor Phase 3a: Modal.lean rewrite — forModalityKind unification
#40 -Commit
cfabca3404
pushed by
max
Refactor Phase 2: modal unification — Lean engine cascade
#39 -Commit
6e4936d6ee
pushed by
max
Remove Test/Reify.lean — Phase 1 macro-debugging scratch
#38 -Commit
c334bf9784
pushed by
max
Refactor Phase 1: derive_reflect_reify macro — Reflect.lean elegance pass
#37 -Commit
2417ec667b
pushed by
max
Modal cascade Phase 3: Modal.lean module proper — Layer 0 complete
#36 -Commit
c7f91fa933
pushed by
max
Modal cascade Phase 2: Rust ABI v5 → v6 (modal constructors)
#35 -Commit
c6bc0aa68f
pushed by
max
Layer 0 substrate round 5: Tactic/EqContract.lean + barrel + Ω-call fixes
#32 -Commit
294e96633d
pushed by
max
Layer 0 substrate round 4: Reflect.lean — bidirectional CTerm/CType ↔ Lean.Expr
#31 -Commit
2f343b0980
pushed by
max
Omega.lean: upgrade operators to use CTerm.code (engine universe-code)
#30 -Commit
7ca4ac8d6a
pushed by
max
Layer 0 substrate round 3: Contract.lean — topos-internal contract framework
#29 -Commit
5de7d9e7d0
pushed by
max
Layer 0 substrate round 2: Subobject + SIP + Modality + Bridge/Set
#28 -Commit
7934275f68
pushed by
max
Layer 0 substrate (Truncation, Decidable, Omega, Category, Reify)
#27 -Commit
f6231f3e64
pushed by
max
REL2 universe stratification + topolei naming cleanup + Rust ABI v4
#26 -Commit
19928d040a
pushed by
max
Drop Infoductor dependency; cubical-transport is now pure cubical engine
#25 -Commit
d03746497b
pushed by
max
Extract Algebra/ foundation to Infoductor; require it from forgejo
#24 -Commit
e26ada2fbc
pushed by
max
Abstract the four ⚠️ tools into well-defined primitives
#22 -Commit
48b7326523
pushed by
max
algebra-restructure CLI + asyncMode .sync on registries
#21 -Commit
b88f6e6f62
pushed by
max
EngineMethodologies + cubical_close: ALGEBRA §9 closer set
#20 -Commit
333f31d4bc
pushed by
max
@[metaPath] + structured failure + engine-bound methodologies
#19 -Commit
60f7ecdf54
pushed by
max
ALGEBRA Phases A+B+C+D' + cubical_search tactic + doc state-of-play
#18 -Commit
7ccebb606d
pushed by
max
QUESTIONS Levels 1.5 + 2: full DecidableEq + simp routing
#17 -Commit
271b47102e
pushed by
max
QUESTIONS Level 1: CompQ reified + classifier-conditioned axioms
#16 -Commit
6adbce0c1b
pushed by
max
Document the question-form algebra + Dev_Algebra plan + Eulerian record
#15 -Commit
95f11020d7
pushed by
max