Can I show Coq equality of types without using a mapping between the types?

Question

Say that I have a list structure and a lemma:

my_list :  BoolSet U -> Type

Lemma union_comm (A B : BoolSet U) :
  Union A B = Union B A
Proof.
...
Qed.

Lemma my_list_eq_union (A B : BoolSet U) :
  my_list (Union A B) = my_list (Union B A).
Proof.
  rewrite union_comm; reflexivity.
Qed.

This lemma states that the two types are equal. In a function expecting a type my_list (Union A B) I would like to be able to pass a my_list (Union B A). I am able to do this by using the lemma above to create a mapping map {A B : BoolSet U} (m : my_list (Union A B)) : my_list (Union B A). from one type to the other. However, this means that my term is wrapped in this function mapping it to the correct type. This makes it hard to work with in proofs when I want to unfold it. I tried defining a coercion, but this is simply an automatic application of the mapping.

Is there a better way to use one type instead of the other when you can show their equality?

Answer 1

Without more context, I would say that you are doing things in the only possible way: the only way to use propositional equality is transport, which in your case corresponds to the function map.

If you want to avoid this problem, you will have to alter code in other places, typically find a way to have the function(s) to which you pass map m take m instead.