Is it possible to write a function that returns the domain of a map which is defined as follows:
Variable A B : Type.
Hypothesis A_eqB_dec : forall x y : A, {x = y} + {x <> y}.
Definition map := A -> option B.
It depends on what you call the domain. If it is a proposition of elements of A, then that function is easy to define:
Definition domain_prop (A B : Type) (map : A -> option B) : A -> Prop :=
exists (b : B), map a = Some b
You can even make this better, by replacing the proposition by a boolean, since "not being None" is decidable:
Definition domain_bool (A B : Type) (map : A -> option B) : A -> bool :=
fun a => match (map a) with | None => false | Some _ => true end
Note that defining these does not require any properties on A or B. However, if you want to enumerate elements of the domain in some form, then I do not think you can do that without assuming that A is enumerable in some way. If A is enumerable, you should be able to enumerate elements in the domain as well, by going through A and selecting only elements which are in the domain (in the sense of domain_bool above). The exact way to do this will depend on your definition of "enumerable".