basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
Geometric mathematics is mathematics done in geometric logic or geometric type theory or inside of a Grothendieck topos. One has finite limits and all colimits, but one does not in general have function sets or power sets. The requirement that one works inside of a Grothendieck topos instead of a geometric category (cf. Vickers 22) is because geometric categories are in general not balanced categories and so the principle of unique choice is not satisfied inside of the category.
Steve Vickers, Generalized point-free spaces, pointwise, (arXiv:2206.01113)
Steve Vickers, Is geometric logic constructive? (slides)
Last revised on December 13, 2023 at 15:37:56. See the history of this page for a list of all contributions to it.