I'm stuck with proving the following

```
Goal forall a b c d, (a * b)%type = (c * d)%type -> a = c /\ b = d.
intros * H.
```

I tried `destruct H`

or `inversion H`

but neither works. So I am skeptical about whether this can be proved or not. I'd appreciate if anyone can give suggestions about which tactic can be used here or how to re-formulate it to make it provable.

What you are trying to prove corresponds to the injectivity of the `*`

type constructor, which is not derivable in CIC. Indeed there are models where this is not true, for instance in homotopy type theory.

This would contradict some strong equality principles such as univalence so it will not be provable.

I see. Thank you both.

There are usually ways to go around these unprovable things, but it depends widely upon what you want to do with it. What is your context?

In general you cannot inspect types so inverting equalities about them is not going to work.

But a typical solution might be to replace types with codes, eg. have an inductive

```
Inductive code : Type :=
| prod : code -> code -> code
…
```

and a function `decode : code -> Type`

mapping `prod co1 co1`

to `(decode co1) * (decode co2)`

, so that you can use injectivity of the `prod`

constructor.

Here, having `prod a b = prod c d`

you *can* deduce `a = c`

and `b = d`

.

But this is somehow stronger than only having `decode (prod a b) = decode (prod c d)`

which corresponds roughly to your original goal.

I'm trying to define the product on type constructors

```
Inductive tycon_prod (E F: Type -> Type): Type -> Type :=
| tycon_prod_intro s t :
E s -> F t -> tycon_prod E F (s * t)%type.
```

So sometimes I got type level equalities like in my original question. Let me try to replace (s * t) with what you suggested. Thank you so much!

Fwiw if you just need a product it's enough to do `Definition hprod (E F : Type -> Type) (T : Type) : Type := E T * F T.`

, but codes make sense for metaprogramming tasks

Last updated: Jan 29 2023 at 01:02 UTC