https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... : > Today, Zermelo–Fraenkel s

https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory 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 https://en.wikipedia.org/wiki/Foundations_of_mathematics Implementation of mathematics in set theory: https://en.wikipedia.org/wiki/Implementation_of_mathematics_in_set_theory https://en.wikipedia.org/wiki/Implementation_of_mathematics_... : > 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 https://github.com/HoTT/Coq-HoTT What is the relation between Coq-HoTT & Homotopy Type Theory and Set Theory with e.g. ZFC? Homotopy Type Theory: https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory : > "Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities" (2018) https://scholar.google.com/scholar?cites=9763697449338277760&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=9763697449338277760... and sorted by date: https://scholar.google.com/scholar?hl=en&as_sdt=5,43&sciodt=0,43&cites=9763697449338277760&scipsc=&q=&scisbd=1 https://scholar.google.com/scholar?hl=en&as_sdt=5,43&sciodt=... What does Mathlib have for SetTheory, ZFC, NFU, and HoTT? leanprover-community/mathlib4// Mathlib/SetTheory: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/SetTheory https://github.com/leanprover-community/mathlib4/tree/master...