55 citations · 97 across the 13 of their papers we have counts for
13 papers
Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem
Andrej Bauer
I take a constructive look at Dieter Spreen's treatment of effective topological spaces and the Kreisel-Lacombe-Shoenfield-Tseitin (KLST) continuity theorem. Transferring Spreen's…
Finitary type theories with and without contexts
Philipp G. Haselwarter, Andrej Bauer
We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin-Löf type theory, simple type theories, first-order…
Instance reducibility and Weihrauch degrees
Andrej Bauer
We identify a notion of reducibility between predicates, called instance reducibility, which commonly appears in reverse constructive mathematics. The notion can be generally used…
An extensible equality checking algorithm for dependent type theories
Andrej Bauer, Anja Petković Komel
We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying exte…
What is algebraic about algebraic effects and handlers?
Andrej Bauer
This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic ef…
Every metric space is separable in function realizability
Andrej Bauer, Andrew Swan
We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with syntheti…
Design and Implementation of the Andromeda Proof Assistant
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter +2
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromed…
The HoTT Library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine +3
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including un…
An Effect System for Algebraic Effects and Handlers
Andrej Bauer, Matija Pretnar
We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expre…
A non-commutative Priestley duality
Andrej Bauer, Karin Cvetko-Vah, Mai Gehrke +2
We prove that the category of left-handed strongly distributive skew lattices with zero and proper homomorphisms is dually equivalent to a category of sheaves over local Priestley…
On the Bourbaki-Witt Principle in Toposes
Andrej Bauer, Peter LeFanu Lumsdaine
The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. W…
Stone Duality for Skew Boolean Algebras with Intersections
Andrej Bauer, Karin Cvetko-Vah
We extend Stone duality between generalized Boolean algebras and Boolean spaces, which are the zero-dimensional locally-compact Hausdorff spaces, to a non-commutative setting. We f…
On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos
Andrej Bauer
In the effective topos there exists a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. Consequently, the Bourbaki-Witt…