# Type theoretic equivalent of isomorphism class

How one defines the notion of isomorphism class in type theory? For concreteness I will describe what I mean with an example in Coq.

Suppose I have a record ToyRec:

Record ToyRec {Labels : Set} := {
X:Set;
r:X->Labels
}.


And a definition of isomorphisms between two objects of type ToyRec, stating that two objects T1 and T2 are isomorphic if there exists a bijection f:T1.(X)->T2.(X) which preserves the label of mapped elements.

Definition Isomorphic{Labels:Set} (T1 T2 : @ToyRec Labels) : Prop :=
exists f:T1.(X)->T2.(X), (forall x1 x2:T1.(X), f x1 <> f x2) /\
(forall x2:T2.(X), exists x1:T1.(X), f x1 = f x2) /\
(forall x1:T1.(X) T1.(r) x1 = T2.(r) (f x1)).


Now I would like to define a function that takes an object T1 and returns a set containing all objects that are isomorphic to T1.

g(T1) = {T2 | Isomorphic T1 T2}


So I have some closely related questions:

1) How one does such a thing in type theory, or more specifically, in coq? I know that I might be reasoning too set theoretically here, but what would be the right type theoretic notion of isomorphism class?

2) More basically, how one would define a set (or type) of all elements satisfying a given property P?

3) Does Voevodsky's univalence axiom helps formalizing this notion?

obs: I posted a similar question in stackoverflow, but I believe that cstheory is more appropriate, since this question is more about type theory than coq syntax.

• What's wrong with g(T1) = {T2 | Isomorphic T1 T2} (still in Coq notation)? – cody Jan 8 '15 at 23:05
• Yeah, what's wrong with @cody's suggestion? – Andrej Bauer Jan 10 '15 at 23:02