I'm working on a theory that uses topology and it would be helpful to have a type of open sets. I tried the following:
context topology
begin
typedef openset = "{U. U ∈ T}"
end
where topology is a locale and the context command correctly gives the output
locale topology =
fixes T :: "'a set set"
assumes "topology T"
However, I get the following error:
Extra type variables in representing set: "'a" The error(s) above occurred in typedef "openset"
What does it mean? Here T is just a set of sets and I want to have a type consisting of the sets belonging to T, is there a way this can be done?