hott3 VS template-agda

Compare hott3 vs template-agda and see what are their differences.

hott3

HoTT in Lean 3 (by gebner)
hott Lean
Source Code
Suggest alternative
Edit details

template-agda

An Agda template, configured for Gitpod (www.gitpod.io) to give you pre-built, ephemeral development environments in the cloud. (by gitpod-samples)
Agda Gitpod
Source Code
Suggest alternative
Edit details
WorkOS
Our great sponsors
  • WorkOS - The modern identity platform for B2B SaaS
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • SaaSHub - Software Alternatives and Reviews
Our great sponsors
hott3 template-agda
2 1
72 8
- -
1.8 0.0
over 3 years ago over 2 years ago
Lean Agda
Apache License 2.0 MIT License
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.

hott3

Posts with mentions or reviews of hott3. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-12-11.
  • The HoTT Game
    2 projects | news.ycombinator.com | 11 Dec 2021
    Lean 3 introduced singleton-elimination which is inconsistent with HoTT. There's a project [0] that uses an attribute to restrict uses of that rule, but it isn't really ergonomic to use.

    [0] https://github.com/gebner/hott3

  • Homotopy Type Theory
    3 projects | news.ycombinator.com | 23 Jun 2021
    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.

template-agda

Posts with mentions or reviews of template-agda. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-12-11.
  • The HoTT Game
    2 projects | news.ycombinator.com | 11 Dec 2021
    Howdy, Geoff from Gitpod here. Yes, I just created this for the Agda community. Enjoy <3 https://github.com/gitpod-io/template-agda

What are some alternatives?

When comparing hott3 and template-agda you can also consider the following projects:

mathlib - Lean 3's obsolete mathematical components library: please use mathlib4

agda-stdlib - The Agda standard library

trepplein - Lean type-checker written in Scala.

Agda - Agda formalisation of the Introduction to Homotopy Type Theory

Coq-HoTT - A Coq library for Homotopy Type Theory

agdarsec - Total Parser Combinators in Agda

Leantime - Leantime is a goals focused project management system for non-project managers. Building with ADHD, Autism, and dyslexia in mind.

TypeTopology - Logical manifestations of topological concepts, and other things, via the univalent point of view.

cubical - An experimental library for Cubical Agda

lean4 - Lean 4 programming language and theorem prover

hott3 vs mathlib template-agda vs agda-stdlib hott3 vs trepplein template-agda vs Agda hott3 vs Coq-HoTT template-agda vs agdarsec hott3 vs Leantime template-agda vs TypeTopology hott3 vs cubical hott3 vs lean4