Skip to content

Navigation Menu

Sign in
Appearance settings
HoTT

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Appearance settings
@HoTT

Homotopy Type Theory

Popular repositories Loading

  1. book book Public

    A textbook on informal homotopy type theory

    TeX 2.1k 373

  2. Coq-HoTT Coq-HoTT Public

    A Coq library for Homotopy Type Theory

    Rocq Prover 1.4k 199

  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 110 12

  5. M-types M-types Public

    A formalization of M-types in Agda

    Agda 36 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 26 5

Repositories

Loading
Type
Select type
Language
Select language
Sort
Select order
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,363 199 111 (6 issues need help) 29 Updated Dec 21, 2025
  • book Public

    A textbook on informal homotopy type theory

    HoTT/book’s past year of commit activity
    TeX 2,126 373 76 5 Updated Nov 23, 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 26 LGPL-2.1 725 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 110 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 36 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
    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 19 23 0 0 Updated Apr 24, 2012

Top languages

Loading…

Most used topics

Loading…
Morty Proxy This is a proxified and sanitized view of the page, visit original site.