Type inequality without cardinality arguments

Question

How can I get Coq to let me prove syntactic type inequality?

Negating univalence

I've read the answer to this question, which suggests that if you assume univalence, then the only way to prove type inequality is through cardinality arguments.

My understanding is - if Coq's logic is consistent with univalence, it should also be consistent with the negation of univalence. While I get that the negation of univalence would really be that some isomorphic types are non-equal, I believe it should be possible to express that no isomorphic types (that aren't identical) are equal.

Inequality for type constructors

In effect, I would like Coq to treat types and type constructors as inductive definitions, and do a typical inversion-style argument to say that my two very clearly different types are not equal.

Can it be done? This would need to be:

Useable for concrete types i.e. no type variables, and so
Not necessarily decidable

That strikes me as being weak enough to be consistent.

Context

I have a polymorphic judgement (effectively an inductive type with parameters forall X : Type, x -> Prop) for which the choice of X is decided by the constructors of the judgement.

I want to prove that, for all judgements for a certain choice of X (say X = nat) some property holds, but if I try to use inversion, some constructors give me hypotheses like nat = string (for example). These type equality hypotheses appear even for types with the same cardinality, so I can't (and don't want to) make cardinality arguments to produce a contradiction.

The unthinkable...

Should I produce an Inductive closed-world encoding of the types I care about, and let that be the polymorphic variable of the above judgement?

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2020-04-18T16:07:06

If you want to use type inequality, I think that the best you can do is to assume axioms for every pair of types you care about:

Axiom nat_not_string : nat <> string.
Axiom nat_not_pair : forall A B, nat <> A * B.
(* ... *)

In Coq, there is no first-class way of talking about the name of an inductively defined type, so there shouldn't be a way of stating this family of axioms with a single assumption. Naturally, you might be able to write a Coq plugin in OCaml to generate those axioms automatically every time an inductive type is defined. But the number of axioms you need grows quadratically in the number of types, so I think would quickly get out of hand.

Your "unthinkable" approach is probably the most convenient in this case, actually.

(Nit: "if Coq's logic is consistent with univalence, it should also be consistent with the negation of univalence". Yes, but only because Coq cannot prove univalence.)