constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
topos, homotopy topos
type theory, homotopy type theory
canonical form, univalence
Bishop set, h-set
decidable equality, decidable subset, inhabited set, subsingleton
A proof assistant or proof management system is a kind of software designed to help with proofs in formal…
basic constructions:
strong axioms
further
In the context of foundations of mathematics or mathematical logic one studies formal systems – theories – that allow us to formalize much if not all of mathematics (and hence, by extension, at least aspects of mathematical fields such as fundamental physics).
There are two different attitudes to what a desirable or interesting foundation should achieve:…
