Hott3 Alternatives

Similar projects and alternatives to hott3

Coq-HoTT

4 1,213 9.8 Coq hott3 VS Coq-HoTT

A Coq library for Homotopy Type Theory
mathlib

36 1,625 8.8 Lean hott3 VS mathlib

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

www.influxdata.com sponsored

Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
template-agda

1 8 0.0 Agda hott3 VS template-agda

An Agda template, configured for Gitpod (www.gitpod.io) to give you pre-built, ephemeral development environments in the cloud.
cubical

3 420 8.6 Agda hott3 VS cubical

An experimental library for Cubical Agda
trepplein

2 26 0.0 Scala hott3 VS trepplein

Lean type-checker written in Scala.
Leantime

49 4,037 9.9 PHP hott3 VS Leantime

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

52 3,714 9.9 Lean hott3 VS lean4

Lean 4 programming language and theorem prover
WorkOS

workos.com sponsored

The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better hott3 alternative or higher similarity.

Suggest an alternative to hott3

hott3 reviews and mentions

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.