hott

Development of homotopy type theory in Agda

An introductory course to Homotopy Type Theory

Ground Zero: Lean 4 HoTT Library

HoTT in Lean 3

Constructive Interpretations of HoTT

Anders: Cubical Type Checker

Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda

Castle Bravo: Experimental HoTT Implementation

《The HoTT Book》 中文翻译

ZFC的问题的形式化与机器证明，人类也会集体活在数学幻觉中：选择数学幻觉P加在ZFC上，是数学社区与魔鬼达成了交易，从而社区得到了A型数学便利，但是魔鬼要的从来都是“灵魂”。 数学的灵魂——数学真理性。

Hurricane: HoTT-I Type System

Proving Ground: Tools for Automated Mathematics

Diagnostic extension for redtt prover

SHRDLU II — a 2026 era modern symbolic substrate for AI agents. From blocks world to modern world models.

HoTT Telemetry Protocol

Formalizing Homotopy-Bridge and Hodge Cycles alignment via Cubical Agda & HoTT in Observation Log David 8.

A Minimal Toy-Mouse Runtime: Iteration Trees and Elementary Embeddings as a Self-Referential Safety Protocol in Two-Level Type Theory (2LTT).