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