max
0 followers · 0 following
  • Joined on 2026-04-25
Repositories
7
 Projects Packages Public activity Starred repositories
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 08:22:22 -05:00
e26ada2fbc Extract Algebra/ foundation to Infoductor; require it from forgejo
max created branch master in max/infoductor 2026-05-01 08:20:49 -05:00
max pushed to master at max/infoductor 2026-05-01 08:20:49 -05:00
ba0a49823b Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries
max created repository max/infoductor 2026-05-01 08:20:43 -05:00
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 07:23:38 -05:00
de56626059 Drop algebra-restructure exe — source code IS the CLI
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 03:57:49 -05:00
48b7326523 Abstract the four ⚠️ tools into well-defined primitives
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 02:17:09 -05:00
b88f6e6f62 algebra-restructure CLI + asyncMode .sync on registries
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 02:06:10 -05:00
333f31d4bc EngineMethodologies + cubical_close: ALGEBRA §9 closer set
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 02:03:35 -05:00
60f7ecdf54 @[metaPath] + structured failure + engine-bound methodologies
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 01:59:12 -05:00
7ccebb606d ALGEBRA Phases A+B+C+D' + cubical_search tactic + doc state-of-play
d6af78a564 Level 2 + Level 3 (lite): TranspQ + HCompQ + CompNQ + cubical_simp
Compare 2 commits »
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 01:34:16 -05:00
271b47102e QUESTIONS Levels 1.5 + 2: full DecidableEq + simp routing
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 01:22:27 -05:00
6adbce0c1b QUESTIONS Level 1: CompQ reified + classifier-conditioned axioms
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 01:04:48 -05:00
95f11020d7 Document the question-form algebra + Dev_Algebra plan + Eulerian record
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 00:22:27 -05:00
7152807b66 REL2 Phase 2: Bridge.lean — Eq ↔ Path interop
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-04-30 19:48:09 -05:00
ce2ee87723 REL2 Phase 1: CType.interval primitive
max created branch Dev_REL2 in max/cubical-transport-hott-lean4 2026-04-30 19:40:36 -05:00
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-04-30 19:40:36 -05:00
max pushed to main at max/cubical-transport-hott-lean4 2026-04-30 19:40:26 -05:00
915b7b3b68 REL2 plan: interval primitive → Bridge → K7 cubical encoding
50bb6660d6 REL1: typing rules + transp/comp derived theorems for .ind + Rust subst
4d6853a0ef REL1 Inductive.lean + Rust dispatch + 9 new smoke tests (25/25 + 46/46)
f27211f73f REL1 foundation: schema-based inductive + HIT CTypes (Lean side)
f9e79b7b0d REL1: design doc for schema-based inductive + HIT CTypes
Compare 5 commits »
max pushed to Dev_REL1 at max/cubical-transport-hott-lean4 2026-04-30 19:37:05 -05:00
915b7b3b68 REL2 plan: interval primitive → Bridge → K7 cubical encoding
max created branch Dev_REL1 in max/cubical-transport-hott-lean4 2026-04-30 19:07:59 -05:00