v1.8.2

Phase 8 soundness fixes - see CHANGELOG for details

v1.8.0-pre

Phase 8: Elaboration and Tactics (Pre-release)

This pre-release implements the elaboration and tactics systems for HoTTGo.

Elaboration System (internal/elab/)

• Surface syntax with implicit arguments and holes
• Bidirectional type checking (synth/check modes)
• Metavariable store for unification
• Zonking for metavariable substitution

Unification (internal/unify/)

• Miller pattern unification
• Constraint solving with occurs check
• Support for all term types (Pi, Sigma, Path, etc.)

Tactics (tactics/)

• Proof state management with goals
• Core tactics: Intro, Exact, Assumption, Apply, Reflexivity, Split, Rewrite
• Tactic combinators: Seq, OrElse, Try, Repeat, First, All
• Go Prover API for programmatic proof construction

Parser Integration

• Surface syntax parsing (holes, implicit arguments)
• S-expression format support

Test Coverage

Package	Coverage
internal/unify	95.0%
tactics/proofstate	97.5%
tactics	90.9%
internal/elab	88.7%
internal/parser	86.5%

Stats

• 20 files changed
• 11,102 lines added
• 1,764 test functions
• 68.6% overall coverage

v1.7.1

What's Changed

Highlights

• Extensive test coverage improvements across all packages
• README rewrite with "Because I love stats" badge section (24 metrics)
• docs/index.md updated with Phase 7 (HITs) completion status
• Badge workflow fixes for accurate commit/release/age metrics
• DIAGRAMS.md updated with HIT architecture diagrams

Test Coverage Improvements

• internal/eval: 80.8% → 91.5%
• internal/ast: 87.8% → 98.8%
• internal/core: 70.4% → 99.1%
• internal/parser: 52.5% → 94.6%
• kernel/check: 75.8% → 93.1%
• kernel/subst: 59.4% → 93.6%

Phase 8 Ready

All Phase 7 audit recommendations addressed. Ready for Phase 8: Elaboration and tactics.

See CHANGELOG.md for full details.

v1.7.0

Higher Inductive Types (Phase 7)

Added

• Higher Inductive Types (HITs) - Full HIT support

  • PathConstructor type for path-level constructors
  • HITApp term for path constructor application
  • evalHITApp for HIT evaluation with boundary reduction
  • DeclareHIT for validating and registering HITs
  • checkHITPositivity for strict positivity checking
  • GenerateHITRecursorType for eliminator type generation

• Built-in HITs

  • Circle (S1): base point and loop path
  • Truncation (Trunc): propositional truncation
  • Suspension (Susp): north, south points with merid path
  • Integers (Int): pos, neg constructors with zeroPath
  • Set Quotient (Quot): quot constructor with eq path

Test Coverage

• 1151 test functions
• 11 packages passing
• Comprehensive cubical type theory tests

v1.6.1

Fixed

• Chocolatey package review issues - Removed unnecessary chocolatey dependency, excluded .tmpl template file from package
• Alpha-equality completeness for cubical types - Added cases for Face formulas, Partial types, Composition, Glue types, and Univalence
• Type synthesis improvements - Better handling of UABeta, Comp, HComp, Fill type checking

Added

• Comprehensive composition tests for cubical operations

Changed

• Revamped architecture diagrams with 3-column layout

See CHANGELOG.md for full details.

v1.6.0

Computational Univalence (Phase 7)

• Univalence axiom (ua): ua A B e : Path Type A B
  • Computation: (ua e) @ i0 = A, (ua e) @ i1 = B
• Glue types: Glue A [φ ↦ (T, e)] : Type
• Composition operations: comp, hcomp, fill
• Face formulas and partial types: Partial φ A, System
• Cubical types always enabled (no -tags cubical needed)

Mutual Inductive Types

• DeclareMutual API for mutually recursive types (e.g., Even/Odd)
• CheckMutualPositivity for cross-type validation
• Separate eliminators per type

Fixes

• golangci-lint cleanup (30 issues resolved)

v1.5.9

Changelog

• efe3531: fix(eval): extract IH indices from constructor args for indexed inductives (@watchthelight)
• 1767bc9: fix(eval): use precomputed IndexArgPositions for robust IH construction (@watchthelight)
• 81b04ba: feat(kernel): add indexed inductive types support (@watchthelight)
• 32e5f13: fix(eval): require complete IndexArgPositions before using metadata (@watchthelight)
• 1006e6a: test(kernel): add computed-index fallback and property tests (@watchthelight)

v1.5.8

Changelog

• 672a4be: All LICENSE links now point to LICENSE.md. (@watchthelight)
• 7e2dc5c: feat(kernel): add parameterized inductive types support (@watchthelight)
• 41c2727: fix: copy assets to docs folder for MkDocs (@watchthelight)
• 39f3d5e: fix: copy assets to docs folder for MkDocs (@watchthelight)
• 8090800: v1.5.8 Release (@watchthelight)

v1.5.7

Added

• Higher-order recursive detection (kernel/check/recursor.go)

  • Extended isRecursiveArgType to detect Pi types with inductive in codomain
  • Correctly identifies (A -> T) as recursive when T is the inductive type

• Parameterized/indexed inductive infrastructure (internal/eval/recursor.go)

  • Extended RecursorInfo with NumParams and NumIndices fields
  • Updated tryGenericRecursorReduction for parameters/indices support

Tests

• Higher-order recursive detection tests
• buildCaseType verification tests (Nat, List, Tree)
• Concurrent registry tests with race detector

v1.5.2

Changelog