Pierre-Marie Pédrot said:

(that said it's not true in the Set model and I wouldn't be surprised if it contradicted mildly classical axioms)

Is it really not? Maybe not on the nose in a naïve way, but surely you can build a set-theoretic model of explicit contravariant subtyping? And I believe this explicit subtyping would satisfy enough equations that you can elaborate implicit subtyping to it

Also, what

Pierre-Marie Pédrot said:

(that said it's not true in the Set model and I wouldn't be surprised if it contradicted mildly classical axioms)

Also, what classical axioms do you have in mind, and how would they fail?

changing the interpretation of functions in Set into something else makes it a non-Set model, to me. Adding explicit subtyping is more subtle, I agree that cumulativity is basically underspecified in Set but interpreting it as something else than inclusion does make it not really set-theoretic (e.g. I think it matters for weird stuff like Prop ⊆ Type).

IIRC contravariant subtyping _on types_ (not universes) was trivial at least in a _logical relations_ set-theoretic model of implicit subtyping... I wonder which of those differences breaks it, maybe the log rel part?

As for axioms, anything that looks like EM has consequences about the existence (or not) of bijections between sets constructed as impredicative fixpoints, so YMMV.

@Paolo Giarrusso you're talking about a universe-free theory, I assume? I.e. you can interpret your logical relation as a proof-irrelevant predicate on terms?

Pierre-Marie Pédrot said:

changing the interpretation of functions in Set into something else makes it a non-Set model, to me. Adding explicit subtyping is more subtle, I agree that cumulativity is basically underspecified in Set but interpreting it as something else than inclusion does make it not really set-theoretic (e.g. I think it matters for weird stuff like Prop ⊆ Type).

So for you interpreting cumulativity as the existence of a coercion/injection between the two sets is not Set-theoretic? Then maybe this is where we disagree, but I feel like non-hardcore set-theorists blur the line between the two quite a bit

Pierre-Marie Pédrot said:

As for axioms, anything that looks like EM has consequences about the existence (or not) of bijections between sets constructed as impredicative fixpoints, so YMMV.

Not sure I see the relation of this with the rest… If you mean that in a system with explicit cumulativity you'd have to be careful about what you do with inductive types, then I agree. But I'm not sure I see the relation with EM

I have no precise example obviously, but a lot of these weird "paradoxes" from EM are statements about the non-existence of retractions between e.g. X and (X → R) → R for well-chosen X and R, oftentimes involving Prop. Given the shape of these objects, I wouldn't be surprised if this were conflicting with contravariant subtyping, since it gives you more definitional retractions. But again, this is just baseless blabbering.

Paolo Giarrusso said:

IIRC contravariant subtyping _on types_ (not universes) was trivial at least in a _logical relations_ set-theoretic model of implicit subtyping... I wonder which of those differences breaks it, maybe the log rel part?

AFAICT, the big problem with contravariant subtyping in set-theory is that it is not on the nose: if $A \subseteq A'$, you do not get a literal inclusion $A' \to B \subseteq A \to B$, only an injection $i : A' \to B \subseteq A \to B$ which discards those pairs in $A' \to B$ whose first component is not in $A$. But interpreting implicit subtyping by the existence of an inclusion is a pain, because you need this inclusion to respect all term-formers from your theory for it to be "transparent enough"

Which is why I think going first through an equivalence with a theory with explicit coercion + all the equations it should satisfy, and then into set-theoretic (or other) models is saner, as it separates the concerns

yeah, with log rels _on terms_ subtyping's on the nose because the "elements" are the same terms — if $\forall v \in A', f\; v \in B$ and $A \subseteq A'$ then $\forall v \in A, f\; v \in B$

Oups, sorry I forgot to create a new thread.

Last updated: Oct 04 2023 at 23:01 UTC