Equilogical spaces (Q1826625)

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.