3
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.