2
$\begingroup$

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. ;)

Improve this question
$\endgroup$
5
  • 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$
    – Naïm Favier
    Commented May 25 at 10:05
  • 2
    $\begingroup$ @NaïmFavier: Could you provide some evidence for your claim, please? $\endgroup$
    – Andrej Bauer
    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$
    – Andrej Bauer
    Commented May 26 at 8:50
  • 2
    $\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$
    – Andrej Bauer
    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$
    – Naïm Favier
    Commented May 26 at 9:31

0

Reset to default