Equality between Types

Using Coq
1

(The topic looks similar to Inequality between Types, but the question is quite different.)

Say that I’ve defined two isomorphic types:

Parameter A B : Type.
Parameter A2B : A  -> B.
Coercion  A2B : A >-> B.
Parameter B2A : B  -> A.
Coercion  B2A : B >-> A.

and two polymorphic types:

Variant E  : Type -> Type := aE : E  A.
Variant E' : Type -> Type := bE : E' B.

Can I show that E and E' are by some means the same? e.g.

Goal forall T, E T -> E' T.
intros _ [].

Now I need to present an instance for E' A. Is this feasible?

2

Coercion doesn’t make types isomorphic, for instance you could do this with A := nat and B := bool which are not the same

Beyond that, if your types are isomorphic you need the univalence axiom to get an equality between them. Look it up for more info, it’s a busy subject.

1 Like