Skip to content
@HoTT

Homotopy Type Theory

Popular repositories Loading

  1. book book Public

    A textbook on informal homotopy type theory

    TeX 2.1k 370

  2. Coq-HoTT Coq-HoTT Public

    A Coq library for Homotopy Type Theory

    Rocq Prover 1.3k 198

  3. HoTT-Agda HoTT-Agda Public

    Development of homotopy type theory in Agda

    Agda 429 58

  4. EPIT-2020 EPIT-2020 Public

    EPIT 2020 - Spring School on Homotopy Type Theory

    TeX 107 12

  5. M-types M-types Public

    A formalization of M-types in Agda

    Agda 33 3

  6. coq coq Public

    Forked from rocq-prover/rocq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

    OCaml 27 5

Repositories

Showing 10 of 10 repositories
  • book Public

    A textbook on informal homotopy type theory

    HoTT/book’s past year of commit activity
    TeX 2,081 370 76 5 Updated Jun 27, 2025
  • Coq-HoTT Public

    A Coq library for Homotopy Type Theory

    HoTT/Coq-HoTT’s past year of commit activity
    Rocq Prover 1,322 198 110 (6 issues need help) 27 Updated Jun 27, 2025
  • HoTT-2023 Public Forked from HoTT/HoTT-2019

    Conference on Homotopy Type Theory 2023

    HoTT/HoTT-2023’s past year of commit activity
    SCSS 13 MIT 7 0 0 Updated Jan 24, 2024
  • coq Public Forked from rocq-prover/rocq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

    HoTT/coq’s past year of commit activity
    OCaml 27 LGPL-2.1 705 51 0 Updated Dec 27, 2023
  • EPIT-2020 Public

    EPIT 2020 - Spring School on Homotopy Type Theory

    HoTT/EPIT-2020’s past year of commit activity
    TeX 107 MIT 12 0 3 Updated Jul 29, 2021
  • M-types Public

    A formalization of M-types in Agda

    HoTT/M-types’s past year of commit activity
    Agda 33 BSD-3-Clause 3 1 0 Updated Mar 7, 2020
  • HoTT-2019 Public

    Conference on Homotopy Type Theory 2019

    HoTT/HoTT-2019’s past year of commit activity
    CSS 16 MIT 7 3 0 Updated Sep 18, 2019
  • HoTT-Agda Public

    Development of homotopy type theory in Agda

    HoTT/HoTT-Agda’s past year of commit activity
    Agda 429 MIT 58 7 1 Updated Feb 19, 2019
  • Archive Public

    Archived materials related to Homotopy Type Theory.

    HoTT/Archive’s past year of commit activity
    11 2 0 0 Updated Apr 24, 2012
  • Foundations Public Forked from UniMath/Foundations

    Development of the univalent foundations of mathematics in Coq

    HoTT/Foundations’s past year of commit activity
    Coq 18 23 0 0 Updated Apr 24, 2012

Most used topics

Loading…