The canonical Homotopy Type Theory informal textbook, initiated at the Institute for Advanced Study (2012–13) under the Univalent Foundations project. It presents the theory pedagogically without requiring technical proof assistant use.

Features

  • Comprehensive introduction to homotopy type theory and univalence
  • Emphasis on intuition and mathematical reasoning without proof assistants
  • Part of a broader univalent foundations initiative
  • Distributed under CC‑BY‑SA 3.0 license
  • Contributions accepted via PRs and GitHub issues
  • Nightly builds and compiled versions available online

Project Samples

book Screenshot 1

Project Activity

See All Activity >

Categories

Mathematics

Follow book

book Web Site

Other Useful Business Software
Paessler - Monitor Your Whole Network in Minutes Icon
Paessler - Monitor Your Whole Network in Minutes

Auto-discovery finds your devices and deploys pre-configured sensors instantly. No project plan required, just visibility from day one.

Waiting weeks for a monitoring rollout isn't an option when infrastructure doesn't stop running. PRTG's auto-discovery scans your network and suggests from over 200 pre-configured sensor types, so you're watching servers, applications and devices within minutes, not after a multi-week deployment. Enterprise-strength monitoring, without the enterprise complexity. Start your free trial today.
Start Free 30-Day Trial
Rate This Project
Login To Rate This Project

User Reviews

Be the first to post a review of book!

Additional Project Details

Programming Language

Python

Related Categories

Python Mathematics Software

Registered

2025-08-06
Report inappropriate content