Coq-HoTT VS path_semantics

https://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//

For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:

UniMath (https://github.com/UniMath/UniMath, mentioned in the article)

Coq-HoTT (https://github.com/HoTT/Coq-HoTT)

agda-unimath (https://unimath.github.io/agda-unimath/)

cubical agda (https://github.com/agda/cubical)

All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).

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.

The major one for me is version control (git). Imaging having to write a book like HoTT without having revisions and easy way to work on your changes without interfering with anyone else's work and then easily merging everything together.

In mathematics, the roof holds up the building, not the foundation. Since humans use mathematics a lot, we design foundations to our specific needs. It is not the building we are worried about, we just want better foundations to create better tools.

Not only are we going to treat mathematics as subjective, but also having formal theories that reason about different notions of subjectivity. https://crates.io/crates/joker_calculus

> Could our conception of paradox be itself primal, and perhaps, in some plane, could it be something ranking higher, of first-class?

Yes! Paradoxes are statements of the form `false^a` in exponential propositions. https://crates.io/crates/hooo

> Also, I’ve been thinking, recently, on the role of time in structures. There can’t possibly be any structure whatsoever without time, or, more concretely, at least the memory of events, recollecting distinctive and contrasting entropic signatures. So, mathematics manifesting as, of, and for structure, wouldn’t it require, first and foremost, a treatment from physics? Regular or meta?

Path semantical quality models this relation, where you have different "moments" in time which each are spaces for normal logical reasoning. Between these moments, there are ways to propagate quality, which is a partial equivalence. https://github.com/advancedresearch/path_semantics

In topology, there is something called "point free theorem proving" style, which is almost usable in Coq or other provers like Lean, or even Cubical Type Theory. The problem is composition of normal paths. In e.g. Coq, you need a solution before you can compose. In order for normal paths to be completely painless, one use an "imaginary inverse" (paper). It is relatively easy to build your own language using an imaginary inverse to do point free theorem proving, but it also turns out that many proofs don't need types. However, adding full point free theorem proving to dependent types makes type checking undecidable.

Here is a transcript of the talk I held for the Category Theory Study Group on Applied Category Theory Server: https://github.com/advancedresearch/path_semantics/blob/master/lectures/introduction-to-path-semantics/transcript-of-introduction-to-path-semantics.pdf

Also, symbolic distinction might play a role in understanding consciousness in relation to Wolfram models. If the hypothesis and underlying assumptions are true, then this could be a major scientific breakthrough. Wolfram models correspond to theorem proving with IPL, so there might be a corresponding interpretation of physics associated with PSI. See https://github.com/advancedresearch/avatar_hypergraph_rewriting for more information. Here is the paper about the hypothesis: https://github.com/advancedresearch/path_semantics/blob/master/papers-wip2/the-symbolic-distinction-hypothesis-of-consciousness.pdf

I had a similar feeling and recently came across a project that feels like it’s closer to the core as you suggest: https://github.com/advancedresearch/path_semantics