Homotopy Type Theory

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

Our great sponsors
  • OPS - Build and Run Open Source Unikernels
  • SonarQube - Static code analysis for 29 languages.
  • Scout APM - Less time debugging, more time building
  • GitHub repo HoTT

    Homotopy type theory

    HoTT is somewhat independent of the choice of proof assistant.

    Coq: https://github.com/HoTT/HoTT

    Lean: https://github.com/gebner/hott3

    idk what you mean by "blue screened", or results being on the way. afaict most of the non-foundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT.

  • GitHub repo hott3

    HoTT in Lean 3

    HoTT is somewhat independent of the choice of proof assistant.

    Coq: https://github.com/HoTT/HoTT

    Lean: https://github.com/gebner/hott3

    idk what you mean by "blue screened", or results being on the way. afaict most of the non-foundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT.

  • OPS

    OPS - Build and Run Open Source Unikernels. Quickly and easily build and deploy open source unikernels in tens of seconds. Deploy in any language to any cloud.

  • GitHub repo cubical

    An experimental library for Cubical Agda

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts