constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
basic constructions:
strong axioms
further
Constructive set theory is set theory in the spirit of constructive mathematics.
Algebraic set theory is a categorical presentation of such set theories.
Some more information can be found at ZFC. Perhaps this should be moved here.
There are a number of axiom systems:
All of these set theories can be interpreted in a set-level type theory with a type of all propositions.
All of these set theories can be interpreted in set-level type theory with no type of all propositions, but with function types and dependent function types
All of these set theories can be interpreted in set-level type theory with only dependent function types for families of subsingletons.
See also
Last revised on November 27, 2022 at 23:39:32. See the history of this page for a list of all contributions to it.