tl; dr Power arguments are the only way to show unequal types. You can, of course, more efficiently automate power arguments with little reflection. If you want to go further, give your types a syntactic representation by building a universe, ensuring that your proof obligations are framed as a syntactic inequality of representations, not a semantic type inequality.
Isomorphism as equality
It is widely believed (and maybe even prove it somewhere) that Kok's logic is consistent with the axiom that isomorphic sets are propositionally equal. Indeed, this is a consequence of the axiom of uniqueness from Vladimir Voevodsky, with which people now have so much fun. I must say that it seems plausible that it is consistent (in the absence of a typecase) and that a computational interpretation can be built that somehow transfers values between equal types, inserting the one that is required in any component of the isomorphism into any given moment.
Assuming that such an axiom is consistent, we find that type inequality in logic in its current form can only be proved by refuting the existence of a type isomorphism. As a result, your private decision, at least in principle, is where it is. Enumeration is rather the key to the manifestation of non-isomorphism. I'm not sure what the status nat = (nat -> nat) can be, but from the outside the system makes it clear that every resident of nat -> nat has a normal shape and that there are a countably many normal forms: at least it is plausible that there are consecutive axioms or reflection principles that make logic more intensional and support this hypothesis.
Power Argument Automation
I see two steps you can take to improve the situation. A less radical step is to improve your overall technology to accept these power arguments by making better use of reflection. You are ideally suited to this, because in general you want to show that the final set is different from some larger set. Suppose we have some concept DList A , a list of different elements of A If you can build a comprehensive DList A and a longer DList B , then you can refute A = B
There is an excellent definition of DList by induction-recursion, but Coq does not have induction-recursion. Fortunately, this is one of those definitions that we can simulate by carefully using indexing. Excuse my unofficial syntax, but let
Parameters A : Set d : A -> A -> bool dok : forall xy, dxy = true -> x = y -> False
This is d for "different." If the collection already has solvable equality, you can easily equip it with d . A large kit can be equipped with adequate d for our purposes with little work. And in fact, this is a crucial step: following the wisdom of the SSReflect team, we use the smallness of our domain, working with bool , not Prop , and make the computer heavy.
Now let's
DListBody : (A -> bool) -> Set
where the index is the freshness test for the list
dnil : DListBody (const true) (* any element is fresh for the empty list *) dsnoc : forall f, (xs : DListBody f) -> (x : A) -> is_true (fx) -> DListBody (fun y => fy /\ dxy)
And if you like, you can define DList wrapping DListBody existentially. It’s possible that in fact we are hiding the information we want, because in order to show such a thing, it looks like this:
Exhaustive (f : A -> bool)(mylist : DListBody f) = forall x : A, is_false (fx)
So, if you can write DListBody for the final enumeration, you can prove its exhaustive just analysis of the case with trivial subgoals.
Then you only need to cast the pigeonholing argument once. If you want to refute the equality between types (provided that you already have suitable candidates for d ), you exhaustively list the smaller ones and show a longer list from the larger one and that it is.
Work in the universe
A more radical alternative is the question of why you first achieve these goals and whether that really means what you want from them. What should be the types? There are several possible answers to this question, but at least it’s open that they are, in a sense, “capacities”. If you want to think that types are more specific and syntactic, different, if they are built by different constructions, then you may need to equip types with a more specific representation, working in the universe. You define the inductive data type "names" for types, as well as the means to decode names as types, and then redefine your design in terms of names. You should find that name inequality follows ordinary constructor discrimination.
The catch is that the constructions of the Universe can be a bit complicated in Coq, again because induction recursion is not supported. It depends on what types you need to consider. Perhaps you can inductively define some U : Set , and then implement the recursive decoder T : U -> Set . This is certainly plausible for universes of simple types. If you need a universe of dependent types, things get a little dumber. You can at least do it significantly
U : Type (* note that we've gone up a size *) NAT : U PI : forall (A : Set), (A -> U) -> U T : U -> Set T NAT = nat T (PI AB) = forall (a : A), T (B a)
but note that the PI region is not PI in Set , not in U Inductively recursive Agdans can overcome this by simultaneously defining U and T
U : Set (* nice and small *) NAT : U PI : forall (A : U), (TA -> U) -> U (* note the use of T *) T : U -> Set T NAT = nat T (PI AB) = forall (a : TA), T (B a)
but Coq will not. Again, a workaround is to use indexing. Here the cost is such that U inevitably large.
U : Set -> Type NAT : U nat PI : forall (A : Set)(B : A -> Set), UA -> (forall a, U (B a)) -> U (forall a, B a)
But you can still get a lot of material created in this way. For example, it is possible to equip such a universe with the help of computationally effective extensional equality .