Suppose you have A: Type and P Q: A -> Prop such that {x : A | P x} = {x : A | Q x}. Can you show P = Q, or at least forall x : A, P x -> Q x? Does anything change if sig is replaced by ordinary dependent sum (into something predicative instead of Prop for example)? A: Set is ok if it simplifies matters. Even for a finite (listable) A it would be nice. My colleagues and I have tried to make progress on this for quite a long time without success. I'd be grateful for any ideas.

I guess it must need axioms, since by default type equality just gives an isomorphism, and you can't know that this isomophism projects to identity on A. And without it, you only have forall x : A, P x -> exists y : A, Q y. But so far we haven't had any luck even with very strong axioms added. UIP seems like an obvious candidate, but it doesn't help much (or we don't know how to employ it).

If there really is no "usual" axiom from which this follows, do you have a feeling it might be consistent? To me it surely does feel like it shouldn't spoil anything, and I'd like to have it as an additional axiom if nothing else, but what do I know.

The question is about Coq, but if some other proof assistant handles it much more nicely, I welcome sales pitches. ;)

  • 2
    $\begingroup$ This is called injectivity of type constructors (in this case, $\Sigma$) and is inconsistent with univalence (in fact it holds in basically no models besides the term model). $\endgroup$ Commented May 25 at 10:05
  • 2
    $\begingroup$ @NaïmFavier: Could you provide some evidence for your claim, please? $\endgroup$ Commented May 25 at 23:01
  • 2
    $\begingroup$ @Veky: This seems to be an instance of the XY problem. Please describe what you're really doing, because I will bet you that you do not want the assumption {x : A | P x} = {x : A | Q x}. There will be a better way. $\endgroup$ Commented May 26 at 8:50
  • 1
    $\begingroup$ Consider the fact that in HoTT we can show {n : ℕ | Odd n} = ℕ = {n : ℕ | Even n} but you can hardly expect Odd n → Even n. $\endgroup$ Commented May 26 at 8:54
  • 1
    $\begingroup$ @AndrejBauer I will cop out by saying that it fails in sets, is inconsistent with univalence, excluded middle and impredicativity, so that excludes just about every model I happen to care about. This other question is also relevant. $\endgroup$ Commented May 26 at 9:31


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.