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. Learn more →
Top 4 univalent-foundation Open-Source Projects
-
InfluxDB
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.
-
TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
Project mention: What do we mean by "the foundations of mathematics"? | news.ycombinator.com | 2023-11-01https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... :
> * Today, Zermelo–Fraenkel set theory [ZFC], with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common* foundation of mathematics.
Foundation of mathematics: https://en.wikipedia.org/wiki/Foundations_of_mathematics
Implementation of mathematics in set theory:
> The implementation of a number of basic mathematical concepts is carried out in parallel in ZFC (the dominant set theory) and in NFU, the version of Quine's New Foundations shown to be consistent by R. B. Jensen in 1969 (here understood to include at least axioms of Infinity and Choice).
> What is said here applies also to two families of set theories: on the one hand, a range of theories including Zermelo set theory near the lower end of the scale and going up to ZFC extended with large cardinal hypotheses such as "there is a measurable cardinal"; and on the other hand a hierarchy of extensions of NFU which is surveyed in the New Foundations article. These correspond to different general views of what the set-theoretical universe is like
IEEE-754 specifies that float64s have ±infinity and specify ZeroDivisionError. Symbolic CAS with MPFR needn't be limited to float64s.
HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/Coq-HoTT
leanprover-community/mathlib4//
I just wonder if there are any irl meetups of people involved with formalizing mathematics, I thought that it would be a cool hobby to pick up (with some background in math and programming) but the existing libraries, like MathLib, TypeTopology or UniMath look a bit intimidating...
univalent-foundations related posts
- What do we mean by "the foundations of mathematics"?
- How and where to learn the latest mathematical concepts?
- What are some examples of non-trivial proofs written in Agda that I might read?
- Homotopy Type Theory
- What is the benefit of using a text editor like MikTex, Texmaker, etc. over Overleaf?
- Plato’s Cave Found in Mathematics
-
A note from our sponsor - InfluxDB
www.influxdata.com | 24 Apr 2024
Index
What are some of the best open-source univalent-foundation projects? This list will help you:
Project | Stars | |
---|---|---|
1 | Coq-HoTT | 1,213 |
2 | cubicaltt | 556 |
3 | TypeTopology | 211 |
4 | Agda | 116 |
Sponsored