nLab Andrej Bauer

• home page

• blog

Selected writings

On propositional truncation in dependent type theory:

• Steve Awodey, Andrej Bauer, Propositions as $[$Types$]$, Journal of Logic and Computation, 14 (2004) 447-471 [doi:10.1093/logcom/14.4.447, pdf]

On the Dedekind real numbers via abstract Stone duality:

• Andrej Bauer, Paul Taylor, The Dedekind reals in abstract Stone duality, Mathematical Structures in Computer Science 19 4 (2009) 757-838 [doi:10.1017/S0960129509007695]

• Andrej Bauer, Efficient Computation with Dedekind Reals, talk at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008 (2008) [web, slides: pdf, extended abstract: pdf]

On intuitionism/constructive mathematics/realizability and physics:

• Andrej Bauer: Intuitionistic Mathematics and Realizability in the Physical World, in A Computable Universe (2012) 143-157 [doi:10.1142/9789814374309_0008, pdf, webpage]

On the HoTT book real numbers:

• Andrej Bauer, The real numbers in homotopy type theory, talk at Computability and Complexity in Analysis, Faro (2016) [pdf, pdf]

On dependent type theory:

• Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine, A general definition of dependent type theories [arXiv:2009.05539]

On categorical logic:

• Steve Awodey, Andrej Bauer: Introduction to categorical logic, lecture notes for a course at Carnegie Mellon University (January-April 2024) [webpage, 0:pdf, 1:pdf, 2:pdf, 3:pdf, 4:pdf]

On separable metric spaces in function realizability:

• Andrej Bauer and Andrew Swan, Every metric space is separable in function realizability, 2018, (arxiv:1804.00427)

category: people