Proof-relevance in Bishop-style constructive mathematics
From MaRDI portal
Publication:5055489
DOI10.1017/S0960129522000159OpenAlexW4281733727WikidataQ113857438 ScholiaQ113857438MaRDI QIDQ5055489
Publication date: 9 December 2022
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129522000159
Related Items
Proof-relevance in Bishop-style constructive mathematics, Closed subsets in Bishop topological groups
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
- A course in constructive algebra
- Closed subsets in Bishop topological groups
- Algebras of complemented subsets
- Functions of Baire class one over a Bishop topology
- Borel and Baire sets in Bishop spaces
- Intuitionism and proof theory. Proceedings of the summer conference at Buffalo N. Y. 1968
- Constructing categories and setoids of setoids in type theory
- Proofs and Computations
- Completely Regular Bishop Spaces
- A constructive function-theoretic approach to topological compactness
- Countable Choice as a Questionable Uniformity Principle
- Direct spectra of Bishop spaces and their limits
- Proof-relevance in Bishop-style constructive mathematics
- Embeddings of Bishop spaces
- The Urysohn Extension Theorem for Bishop Spaces
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Constructive measure theory
- Reuniting the antipodes---constructive and nonstandard views of the continuum. Symposium proceedings, San Servolo, Venice, Italy, May 16--22, 1999
- Bases of Pseudocompact Bishop Spaces
