Effective versions of equilogical spaces
Dana Scott · Electronic Notes in Theoretical Computer Science · 2000
The full category of equilogical spaces can be thought of either as ER(TOP), the category of equivalence relations on T 0 -topological spaces and equivariant continuous maps (i.e., equivalence preserving), or PER(DOM/T), the category of partial equivalence relations on Scott domains with a top (i.e., algebraic lattices) and equivariant continuous maps, or PER(POWER), the category of partial equivalence relations on power-set spaces and equivariant continuous maps. (See also the the abstract of Andrej Bauer at this meeting for a discussion of another equivalent category.) If we replace general topological spaces with countably based spaces - each given with a particular choice of a countable basis - we can then ask how the resulting categories express effective (computable) notions. The most explicit equivalent version of the category obtained is PER(P(N)), the category of partial equivalence relations over the power-set-of-N domain and equivariant continuous maps. The talk will discuss how the notion of computability appears in this category and how the category can be used as a model for a type theory enriched with a ‘computability’ modal operator. (See also the abstract of Lars Birkedal at this meeting.)