CODEWITHSUNDEEP
coqdependent-type
Bob
Bob

Reputation: 1743

Does injectivity of Type product make sense?

How to prove the following in Coq?

Goal forall (A B : Type), (A*A = B*B)%type -> A = B.

If it is not provable, can it be safely added as an axiom?

Upvotes: 1

Views: 255

Answers (3)

Thorsten Altenkirch
Thorsten Altenkirch

Reputation: 519

Yes my comment was on the stronger statement. Squaring should be injective but I am not sure wether you can prove this in HoTt.

Upvotes: 2

Thorsten Altenkirch
Thorsten Altenkirch

Reputation: 519

It is certainly inconsistent with univalence, e.g. 2x3 = 1 x 6 but 1 /= 2 and 3 /= 6. Strange idea to want this.

Upvotes: -1

Jannis Limperg
Jannis Limperg

Reputation: 663

Edit: The following answer assumes a stronger statement than that in the question: forall (A B C D : Type), (A*B = C*D)%type -> A = C. So the answer doesn't actually answer the question.

Your goal is not provable since it contradicts univalence, which is independent of Coq. The contradiction arises because A * False is isomorphic to False for any A. Univalence then implies A * False = False and your goal lets us conclude A = B for any A and B. In particular, True = False, which yields a proof of False by transport. So, if your goal was provable, Coq would be anti-univalent.

I don't know whether your goal without univalence also leads to a contradiction.

Upvotes: 0

Related Questions