Proof that two isomorphic types are different

Question

Given these two types,

Inductive unit : Set := tt.
Inductive otherUnit : Set := ttt.

Can Coq prove they are different, ie unit <> otherUnit ?

Both are singleton types in sort Set so it is not easy to find a Set -> Prop that differentiates them. For example, this does not even type check

Definition singletonTT (A : Set) : Prop := forall x : A, x = tt.

because tt has type unit instead of A.

Answer 1

It's actually admissible in Coq that these two types are equal; that is, you can neither prove they are equal or different, and it's consistent to assume either.

You can't express singletonTT in terms of tt because as you point out, it only type checks for the unit type. Instead you need to treat A opaquely; for example, you can express the property of being a singleton as A /\ forall (x y:A), x = y. Of course, both types are singletons so this doesn't distinguish them.

If you do assume Axiom unit_otherUnit : unit = otherUnit, then you can express something like singletonTT by casting tt to otherUnit: eq_rec _ (fun S => S) tt otherUnit ax = ttt.

When types have different cardinalities (which means they aren't isomorphic) you can use their cardinality to distinguish them and prove the types are distinct. Easy examples include False <> True and unit <> bool, and a more complicated example is nat <> (nat -> nat).