scientific article; zbMATH DE number 7561488

DOI10.4230/LIPIcs.TYPES.2018.3MaRDI QIDQ5091143

Iosif Petrakis

Publication date: 21 July 2022

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Martin-Löf's type theoryBishop's constructive mathematicsdependent sumsdependent productstype-theoretic axiom of choice

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Proof-relevance in Bishop-style constructive mathematics ⋮ Computability models over categories and presheaves ⋮ Direct spectra of Bishop spaces and their limits ⋮ Closed subsets in Bishop topological groups

Cites Work

• A minimalist two-level foundation for constructive mathematics
• A course in constructive algebra
• Set theoretic foundations for constructive analysis
• Borel and Baire sets in Bishop spaces
• Quotient topologies in constructive set theory and type theory
• Constructing categories and setoids of setoids in type theory
• Constructive set theory
• A constructive function-theoretic approach to topological compactness
• The Urysohn Extension Theorem for Bishop Spaces
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Towards Constructive Homological Algebra in Type Theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item