Hott

Domain knowledge for dependent type theory, homotopy type theory (HoTT), and univalent foundations: a reasoning toolkit plus topic-indexed digests of Egbert Rijke's Introduction to Homotopy Type Theory, covering identity types, path induction, transport and paths-over, the fundamental theorem of identity types, equivalences, contractibility and fibers, truncation levels (propositions, sets, k-types), function extensionality, univalence, propositional truncation and the logic of mere existence, higher inductive types, the circle and loop spaces, W-types, set quotients, universes, finite types, and groups. This skill should be loaded whenever the work turns on these concepts and the exact statement or the correct technique matters, and not only when the user asks about them: before characterizing an identity type, choosing an induction principle, claiming a type is a proposition or a set, asserting what is or is not provable (UIP, axiom K), invoking function extensionality or univalence, distinguishing judgmental from propositional equality, or reasoning about a higher inductive type. It applies to informal prose mathematics and to the univalent-foundations content behind a proof-assistant development alike, since the concepts are the same either way. It should also be used when the user asks directly about any of these topics, including conceptual and comparative questions about foundations.

mkdir -p ~/.claude/skills/hott
curl -L https://claudskills.com/skills/hott/SKILL.md \
  -o ~/.claude/skills/hott/SKILL.md

@misc{hott-2026,
  author    = {biocini},
  title     = {Hott [Claude Code skill]},
  year      = {2026},
  publisher = {ClaudSkills},
  url       = {https://claudskills.com/skills/hott/}
}