Skip to content
@HoTT

Homotopy Type Theory

Popular repositories Loading

  1. book book Public

    A textbook on informal homotopy type theory

    TeX 2.1k 369

  2. Coq-HoTT Coq-HoTT Public

    A Coq library for Homotopy Type Theory

    Rocq Prover 1.3k 199

  3. HoTT-Agda HoTT-Agda Public

    Development of homotopy type theory in Agda

    Agda 430 58

  4. EPIT-2020 EPIT-2020 Public

    EPIT 2020 - Spring School on Homotopy Type Theory

    TeX 108 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
  • Coq-HoTT Public

    A Coq library for Homotopy Type Theory

    HoTT/Coq-HoTT’s past year of commit activity
    Rocq Prover 1,326 199 109 (6 issues need help) 26 Updated Jul 14, 2025
  • book Public

    A textbook on informal homotopy type theory

    HoTT/book’s past year of commit activity
    TeX 2,084 369 76 5 Updated Jul 3, 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 708 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 108 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 430 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
    12 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…