Repositories list

• book

  Public
  A textbook on informal homotopy type theory

  TeX

  •370•2.1k•76•9•Updated Jun 27, 2025Jun 27, 2025

• Coq-HoTT

  Public
  A Coq library for Homotopy Type Theory

  type-theoryhomotopy-type-theoryunivalent-foundations

  Rocq Prover

  •

  Other

  •198•1.3k•110•27•Updated Jun 27, 2025Jun 27, 2025

• HoTT-2023

  Public
  Conference on Homotopy Type Theory 2023

  SCSS

  •

  MIT License

  •7•13•0•0•Updated Jan 24, 2024Jan 24, 2024

• coq

  Public
  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.

  OCaml

  •

  GNU Lesser General Public License v2.1

  •688•27•51•0•Updated Dec 27, 2023Dec 27, 2023

• EPIT-2020

  Public
  EPIT 2020 - Spring School on Homotopy Type Theory

  TeX

  •

  MIT License

  •12•107•0•3•Updated Jul 29, 2021Jul 29, 2021

• M-types

  Public
  A formalization of M-types in Agda

  Agda

  •

  BSD 3-Clause "New" or "Revised" License

  •3•33•1•0•Updated Mar 7, 2020Mar 7, 2020

• HoTT-2019

  Public
  Conference on Homotopy Type Theory 2019

  CSS

  •

  MIT License

  •7•16•3•0•Updated Sep 18, 2019Sep 18, 2019

• HoTT-Agda

  Public
  Development of homotopy type theory in Agda

  hottunivalenceagda+ 1homotopy

  Agda

  •

  MIT License

  •58•429•7•1•Updated Feb 19, 2019Feb 19, 2019

• Archive

  Public
  Archived materials related to Homotopy Type Theory.

  2•11•0•0•Updated Apr 24, 2012Apr 24, 2012

• Foundations

  Public
  Development of the univalent foundations of mathematics in Coq

  Coq

  •22•18•0•0•Updated Apr 24, 2012Apr 24, 2012