Equilogical spaces
type: Item
instance of: scholarly article
title: Equilogical spaces
zbMATH Open document ID: 1059.18004
author: Andrej Bauer
author: Lars Birkedal
author: Dana Scott
published in: Theoretical Computer Science
publication date: 2004-08-06T00:00:00Z
review text: The paper studies the category \({\mathcal E}qu\) of equivalence relations and equivalence-preserving continuous mappings over the standard category of topological \(T_0\)-spaces. An equivalent definition, in terms of algebraic lattices and partial equivalence relations, is used to prove cartesian closure by using well-known theorems in domain theory, related to injective properties of algebraic lattices treated as topological spaces. Later, the focus is on expressiveness of \({\mathcal E}qu\), in particular, its capability to represent type theory and logic, and develop notions of modest sets and assemblies in order to justify that a model of dependent type theory is obtained. Finally, some comparisons are made to other known models.
reviewed by: Manuel Ojeda-Aciego
Mathematics Subject Classification ID: 18C50
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 18D15
Mathematics Subject Classification ID: 03G30
zbMATH DE Number: 2081672
zbMATH Keywords: domain theory
zbMATH Keywords: topology
zbMATH Keywords: logic
zbMATH Keywords: type theory
zbMATH Keywords: realizability
MaRDI profile type: Publication
full work available at URL: j.tcs.2003.11.012
OpenAlex ID: W2913777840
Wikidata QID: Q106362624
cites work: Q4222034
cites work: Exact categories and categories of sheaves
cites work: Q2753674
cites work: Total sets and objects in domain theory
cites work: Developing theories of types and computability via realizability
cites work: Q4936141
cites work: Q4304740
cites work: Q3795831
cites work: Q4692885
cites work: Q3863873
cites work: Q3898534
cites work: Q3024837
cites work: Q3671978
cites work: Tripos theory
cites work: Q5752573
cites work: The Discrete Objects in the Effective Topos
cites work: Comprehension categories and the semantics of type dependency
cites work: Categorical logic and type theory
cites work: Q4296744
cites work: A category-theoretic account of program modules
cites work: Q4335371
cites work: Colimit completions and the effective topos
cites work: Q4023580
DOI: 10.1016/J.TCS.2003.11.012
Recommended article: Q4513596
Recommended article: On a generalization of equilogical spaces
Recommended article: On generalized equilogical spaces
Recommended article: Q4511152
Recommended article: Q4522454
Recommended article: Q4513573
Recommended article: Holonomic Spaces
Recommended article: Spaces with congruence
Recommended article: Existence of a spatial equilibrium
Recommended article: Q3593851
description: scientific article; zbMATH DE number 2081672