max/cubical-transport-hott-lean4
1
0
Fork 0
Code Issues 1 Pull requests Projects Releases Packages Wiki Activity Actions

Commit graph

  • 391a048dcf Layer 3.3a: substantive unit/counit + typed-correctness for adjoint triple Dev_REL2 Maximus Gorog 2026-05-06 06:32:39 -06:00
  • 0a7228a8e5 Axiom debt cleanup: discharge or convert all 99 engine axioms Maximus Gorog 2026-05-06 05:07:50 -06:00
  • 567d8722d5 Refactor Phase 4: Rust ABI v6 → v7 (modal tag unification) Maximus Gorog 2026-05-06 02:25:10 -06:00
  • cfabca3404 Refactor Phase 3a: Modal.lean rewrite — forModalityKind unification Maximus Gorog 2026-05-06 02:13:16 -06:00
  • 6e4936d6ee Refactor Phase 2: modal unification — Lean engine cascade Maximus Gorog 2026-05-06 02:01:52 -06:00
  • c334bf9784 Remove Test/Reify.lean — Phase 1 macro-debugging scratch Maximus Gorog 2026-05-06 01:43:00 -06:00
  • 2417ec667b Refactor Phase 1: derive_reflect_reify macro — Reflect.lean elegance pass Maximus Gorog 2026-05-06 01:42:33 -06:00
  • c7f91fa933 Modal cascade Phase 3: Modal.lean module proper — Layer 0 complete Maximus Gorog 2026-05-05 23:28:01 -06:00
  • c6bc0aa68f Modal cascade Phase 2: Rust ABI v5 → v6 (modal constructors) Maximus Gorog 2026-05-05 23:18:33 -06:00
  • b9ca1d8875 Modal cascade Phase 1: Syntax + Lean engine cascade Maximus Gorog 2026-05-05 22:22:03 -06:00
  • 825d8af68d Layer 0 substrate round 6: contract auto-registration Maximus Gorog 2026-05-05 15:56:03 -06:00
  • 294e96633d Layer 0 substrate round 5: Tactic/EqContract.lean + barrel + Ω-call fixes Maximus Gorog 2026-05-05 15:19:35 -06:00
  • 2f343b0980 Layer 0 substrate round 4: Reflect.lean — bidirectional CTerm/CType ↔ Lean.Expr Maximus Gorog 2026-05-05 14:50:51 -06:00
  • 7ca4ac8d6a Omega.lean: upgrade operators to use CTerm.code (engine universe-code) Maximus Gorog 2026-05-05 14:05:01 -06:00
  • 5de7d9e7d0 Layer 0 substrate round 3: Contract.lean — topos-internal contract framework Maximus Gorog 2026-05-05 09:45:16 -06:00
  • 7934275f68 Layer 0 substrate round 2: Subobject + SIP + Modality + Bridge/Set Maximus Gorog 2026-05-05 09:26:57 -06:00
  • f6231f3e64 Layer 0 substrate (Truncation, Decidable, Omega, Category, Reify) + CType.El / CTerm.code constructors (universe-coding); ABI v5 Maximus Gorog 2026-05-05 09:11:29 -06:00
  • 19928d040a REL2 universe stratification + topolei naming cleanup + Rust ABI v4 Maximus Gorog 2026-05-04 00:21:14 -06:00
  • d03746497b Drop Infoductor dependency; cubical-transport is now pure cubical engine Maximus Gorog 2026-05-01 07:52:59 -06:00
  • e26ada2fbc Extract Algebra/ foundation to Infoductor; require it from forgejo Maximus Gorog 2026-05-01 07:22:20 -06:00
  • de56626059 Drop algebra-restructure exe — source code IS the CLI Maximus Gorog 2026-05-01 06:23:36 -06:00
  • 48b7326523 Abstract the four ⚠️ tools into well-defined primitives Maximus Gorog 2026-05-01 02:57:48 -06:00
  • b88f6e6f62 algebra-restructure CLI + asyncMode .sync on registries Maximus Gorog 2026-05-01 01:17:02 -06:00
  • 333f31d4bc EngineMethodologies + cubical_close: ALGEBRA §9 closer set Maximus Gorog 2026-05-01 01:06:04 -06:00
  • 60f7ecdf54 @[metaPath] + structured failure + engine-bound methodologies Maximus Gorog 2026-05-01 01:03:29 -06:00
  • 7ccebb606d ALGEBRA Phases A+B+C+D' + cubical_search tactic + doc state-of-play Maximus Gorog 2026-05-01 00:59:06 -06:00
  • d6af78a564 Level 2 + Level 3 (lite): TranspQ + HCompQ + CompNQ + cubical_simp Maximus Gorog 2026-05-01 00:46:13 -06:00
  • 271b47102e QUESTIONS Levels 1.5 + 2: full DecidableEq + simp routing Maximus Gorog 2026-05-01 00:34:14 -06:00
  • 6adbce0c1b QUESTIONS Level 1: CompQ reified + classifier-conditioned axioms Maximus Gorog 2026-05-01 00:21:58 -06:00
  • 95f11020d7 Document the question-form algebra + Dev_Algebra plan + Eulerian record Maximus Gorog 2026-05-01 00:04:48 -06:00
  • 7152807b66 REL2 Phase 2: Bridge.lean — Eq ↔ Path interop Maximus Gorog 2026-04-30 23:22:24 -06:00
  • ce2ee87723 REL2 Phase 1: CType.interval primitive Maximus Gorog 2026-04-30 18:47:13 -06:00
  • 915b7b3b68 REL2 plan: interval primitive → Bridge → K7 cubical encoding main Dev_REL1 Maximus Gorog 2026-04-30 18:36:58 -06:00
  • 50bb6660d6 REL1: typing rules + transp/comp derived theorems for .ind + Rust subst Maximus Gorog 2026-04-30 18:05:32 -06:00
  • 4d6853a0ef REL1 Inductive.lean + Rust dispatch + 9 new smoke tests (25/25 + 46/46) Maximus Gorog 2026-04-30 15:15:50 -06:00
  • f27211f73f REL1 foundation: schema-based inductive + HIT CTypes (Lean side) Maximus Gorog 2026-04-30 15:09:39 -06:00
  • f9e79b7b0d REL1: design doc for schema-based inductive + HIT CTypes Maximus Gorog 2026-04-30 14:57:22 -06:00
  • 58330df245 Add NOTICE: AI tooling acknowledgement; proprietary rights stand on human-directed whole Maximus Gorog 2026-04-27 23:10:32 -06:00
  • 5e9be0ffe2 Add proprietary LICENSE; move CI to .forgejo/workflows/, run cubical-test Maximus Gorog 2026-04-27 23:04:16 -06:00
  • 92bd67ac4a Regenerate lake-manifest.json: package name cubicalTransport (was stale 'topolei') Maximus Gorog 2026-04-27 23:00:01 -06:00
  • d9f952fa6c Reorganize: move non-README docs into docs/ subfolder Maximus Gorog 2026-04-27 22:57:10 -06:00
  • 8561e19467 Docs cleanup: archive PHASE1, accept ZIGZAG_PORT, fix stale paths Maximus Gorog 2026-04-27 22:52:14 -06:00
  • 31d19f655e Split: engine = cubical-transport HoTT only Maximus Gorog 2026-04-27 21:35:01 -06:00
  • c2e3ecb3e3 Initial commit: topolei — cubical-transport HoTT in Lean 4 + Rust FFI Maximus Gorog 2026-04-27 20:40:45 -06:00