Order:
  1.  33
    Metric Spaces in Synthetic Topology.Andrej Bauer & Davorin Lešnik - 2012 - Annals of Pure and Applied Logic 163 (2):87-100.
  2.  25
    Two Constructive Embedding‐Extension Theorems with Applications to Continuity Principles and to Banach‐Mazur Computability.Andrej Bauer & Alex Simpson - 2004 - Mathematical Logic Quarterly 50 (4‐5):351-369.
    We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ℤ extends to a sequentially continuous function from X to ℝ. The second asserts an analogous property for Baire space relative to any inhabited locally non-compact CSM. Both results rely on having careful (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  3.  27
    Propositions as [Types].Steve Awodey & Andrej Bauer - unknown
    Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family. We give rules for bracket types in dependent type theory and provide complete semantics using (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  3
    Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability.Andrej Bauer & Alex Simpson - 2004 - Mathematical Logic Quarterly 50 (45):351-369.
    We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ℤ extends to a sequentially continuous function from X to ℝ. The second asserts an analogous property for Baire space relative to any inhabited locally non-compact CSM. Both results rely on having careful (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  5.  18
    A Relationship Between Equilogical Spaces and Type Two Effectivity.Andrej Bauer - 2002 - Mathematical Logic Quarterly 48 (S1):1-15.
    In this paper I compare two well studied approaches to topological semantics – the domain-theoretic approach, exemplified by the category of countably based equilogical spaces, Equ and Typ Two Effectivity, exemplified by the category of Baire space representations, Rep . These two categories are both locally cartesian closed extensions of countably based T0-spaces. A natural question to ask is how they are related.First, we show that Rep is equivalent to a full coreflective subcategory of Equ, consisting of the so-called 0-equilogical (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6. Sheaf Toposes for Realizability.Steven Awodey & Andrej Bauer - 2008 - Archive for Mathematical Logic 47 (5):465-478.
    Steve Awodey and Audrej Bauer. Sheaf Toposes for Realizability.
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark  
  7.  14
    A Constructive Theory of Continuous Domains Suitable for Implementation.Andrej Bauer & Iztok Kavkler - 2009 - Annals of Pure and Applied Logic 159 (3):251-267.
    We formulate a predicative, constructive theory of continuous domains whose realizability interpretation gives a practical implementation of continuous ω-chain complete posets and continuous maps between them. We apply the theory to implementation of the interval domain and exact real numbers.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  8.  7
    Preface.Andrej Bauer, Thierry Coquand, Giovanni Sambin & Peter M. Schuster - 2012 - Annals of Pure and Applied Logic 163 (2):85-86.