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
The arithmetical hierarchy or arithmetic hierarchy or Kleene–Mostowski hierarchy is a hierarchy used in c…
As a strengthening of the uncomputability of the Halting Problem, there is a total computable function $f$ which shows where a Turing machine $M$ fails to compute the Halting problem, in that for each ...
basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In constructive mathematics, a set is exhaustible or omniscient if it satisfies a version of the limited principle of omniscience for the set rather than the natural numbers : the existential quantification of any decidable propo…
