lean-hit-development
CommunityBlueprints for adding new HITs to ComputationalPaths.
AuthorArthur742Ramos
Version1.0.0
Installs0
System Documentation
What problem does it solve?
This Skill provides a blueprint for adding new Higher Inductive Types (HITs) to the ComputationalPaths Lean 4 library, including axiomatization, recursion principles, and encoding/decoding of π₁.
Core Features & Use Cases
- Define axioms for a new HIT type and its point/path constructors
- Add recursion principles and computation rules
- Build a group presentation and implement encode/decode between π₁ and the presentation
- Follow established HIT patterns (Circle, Torus, Sphere) to ensure consistency
Quick Start
Create a new HIT skeleton under ComputationalPaths/Path/HIT/YourHIT.lean with required axioms, a basic encode/decode, and register your piOneEquiv.
Dependency Matrix
Required Modules
None requiredComponents
Standard package💻 Claude Code Installation
Recommended: Let Claude install automatically. Simply copy and paste the text below to Claude Code.
Please help me install this Skill: Name: lean-hit-development Download link: https://github.com/Arthur742Ramos/ComputationalPathsLean/archive/main.zip#lean-hit-development Please download this .zip file, extract it, and install it in the .claude/skills/ directory.