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

<p>Suppose I have a record ToyRec:</p>

<pre><code>Record ToyRec {Labels : Set} := {
X:Set;
r:X-&gt;Labels
}.
</code></pre>

<p>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. </p>

<pre><code>Definition Isomorphic{Labels:Set} (T1 T2 : @ToyRec Labels) : Prop :=
exists f:T1.(X)-&gt;T2.(X), (forall x1 x2:T1.(X), f x1 &lt;&gt; 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)).
</code></pre>

<p>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. </p>

<pre><code>g(T1) = {T2 | Isomorphic T1 T2}
</code></pre>

<p>So I have some closely related questions: </p>

<p>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? </p>

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

<p>3) Does Voevodsky's univalence axiom helps formalizing this notion?</p>

<p>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.</p>

CC BY-SA 3.0
2015-01-08T23:05:09.217Z
What's wrong with ``g(T1) = {T2 | Isomorphic T1 T2}`` (still in Coq notation)?
cody
CC BY-SA 3.0
2015-01-10T23:02:37.100Z
Yeah, what's wrong with @cody's suggestion?
Andrej Bauer
<type-theory><coq>
Type theoretic equivalent of isomorphism class
verifying
# Type theoretic equivalent of isomorphism class

(Asked by: username_0 on 2015-01-08)

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.

**Tags:** type-theory, coq

> **Comments:**
> **username_1**: What's wrong with ``g(T1) = {T2 | Isomorphic T1 T2}`` (still in Coq notation)?  
> **username_2**: Yeah, what's wrong with @username_1's suggestion?  

---

## 0 answers

