A Coq library for Homotopy Type Theory

Formal Reasoning About Programs

My personal repository of formally verified mathematics.

Lecture notes for a short course on proving/programming in Coq via SSReflect.

Modeling and Proving in Computational Type Theory

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Development of the univalent foundations of mathematics in Coq