>>> The HoTT library is a development of homotopy-theoretic ideas in the Coq proof assistant. It draws many ideas from Vladimir Voevodsky's Foundations library (which has since been incorporated into the UniMath library) and also cross-pollinates with the HoTT-Agda library. See also: HoTT in Lean2, Spectral Sequences in Lean2, and Cubical Agda.
/? From a set like {0,1} to a wave function of reals in Hilbert space [to Constructor Theory and Quantum Counterfactuals] https://www.google.com/search?q=From+a+set+like+%7B0%2C1%7D+... , https://www.google.com/search?q=From+a+set+like+%7B0%2C1%7D+...
From "What do we mean by "the foundations of mathematics"?" (2023) https://news.ycombinator.com/item?id=38102096#38103520 :
> HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/Coq-HoTT
>>> The HoTT library is a development of homotopy-theoretic ideas in the Coq proof assistant. It draws many ideas from Vladimir Voevodsky's Foundations library (which has since been incorporated into the UniMath library) and also cross-pollinates with the HoTT-Agda library. See also: HoTT in Lean2, Spectral Sequences in Lean2, and Cubical Agda.
leanprover/lean2 /hott: https://github.com/leanprover/lean2/tree/master/hott
Lean4:
"Theorem Proving in Lean 4" https://lean-lang.org/theorem_proving_in_lean4/
Learnxinimutes > Lean 4: https://learnxinyminutes.com/lean4/
/? Hott in lean4 https://www.google.com/search?q=hott+in+lean4
> What is the relation between Coq-HoTT & Homotopy Type Theory and Set Theory with e.g. ZFC?