9
$\begingroup$

A type that is a member of a universe can be coerced into a higher universe. Is that coercion injective? That is, if two elements of U1 are equal after being coerced to U2, does that imply they are equal before being coerced?

More specifically, is the following provable in Coq?

Universe U1 U2.
Constraint U1 < U2.

Theorem type_coericion_inj:
  forall (A B: Type@{U1}),
  @eq Type@{U2} A B ->
  @eq Type@{U1} A B.

If that isn't provable in Coq, is it at least consistent to add that as an axiom? Is there a better name for this property?

Improve this question
$\endgroup$
3
  • $\begingroup$ If it is not provable and not disprovable, then it is automatically consistent. $\endgroup$
    – Trebor ♦
    Commented Jul 24, 2022 at 4:45
  • $\begingroup$ Are you asking because you need injectivity for a specific purpose, or just as a matter of general interest? $\endgroup$
    – Andrej Bauer
    Commented Jul 24, 2022 at 7:50
  • $\begingroup$ I'm trying to do a shallow embedding of graded type theory in Coq. I'm basing it off of dl.acm.org/doi/pdf/10.1145/3434331. This problem came up while I was trying to prove regularity. $\endgroup$
    – Kyle Stemen
    Commented Jul 24, 2022 at 15:39

2 Answers 2

Reset to default
7
$\begingroup$

You did not specify whether you want Tarski or Russell universes, so let me do Tarski-style, as it is more reasonable anyhow.

Suppose we have two universes $U$ and $V$ with $U : V$, and given $t : U$ let $\mathrm{El}_U(t)$ be the type represented by $t$. Define a new universe $U' = U + U$ with \begin{align*} \mathrm{El}_{U'}(\mathrm{inl}(t)) &= \mathrm{El}_U(t) \\ \mathrm{El}_{U'}(\mathrm{inr}(t)) &= \mathrm{El}_U(t). \end{align*} The universe $U'$ is going to be closed under whatever constructs $U$ is closed (just inject the constructions into the left component, for instance). Obviously, $\mathrm{El}_{U'}$ is not injective as soon as $U$ is inhabited.

You asked specifically about Coq. As far as I know, it does not assume injectivity of coercions, nor does it reject it. In the set-theoretic model of Coq the coercions are injective, so it is consistent to assume that they are indeed injective.

Improve this answer
$\endgroup$
0
$\begingroup$

I'm away from my computer right now so I'm not sure if this works but I believe the "correct" notion ought to be a full and faithful functor between universes.

This sort of style can be an awful pain to work in though.

Universe U1 U2.
Constraint U1 < U2.

Definition map {A B: Type@{U1}}
  (f: A -> B)
  (x: (A : Type@{U2})): (B : Type@{U2}) := f x.

Lemma map_id {A} (x: A): map (fun y => y) x = x.
Lemma map_map {A B C} (f: B -> C) (g: A -> B) x: map f (map g x) = map (fun y => f (g y)) x.

Lemma map_inj {A B} (f g: A -> B) x:
  (forall y, map f x = map g y) ->
  f x = g x.
Lemma map_sur {A B: Type@{U1}} (f: (A : Type@{U2}) -> (B: Type@{U2})):
  { g : A -> B | forall x, map g x = f x }.

I'm pretty sure I probably made some mistake. Certainly not very elegant looking.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ It seems that you are indirectly showing that A: Type@{U1} and (A: Type@{U1}) : Type@{U2} contain the same terms. So one can prove Lemma same_contents: forall {A: Type@{U1}} (x y: A), @eq (A: Type@{U2}) x y -> @eq A x y. However, that isn't as strong as saying that type coercion is injective. A: Type@{U1} and B: Type@{U1} could contain the same terms, but have extra superfluous information that makes the types unequal, but the type coercion can drop that superfluous information such that A: Type@{U2} = B: Type@{U2}. $\endgroup$
    – Kyle Stemen
    Commented Jul 26, 2022 at 9:09
  • $\begingroup$ @KyleStemen Yes that might be one way to think about it. This is a bit awkward to talk about so call the functor from one universe up to the other S. I would think of same_contents as injectivity of the map Id => S. Anyhow the point of working up to isomorphism as opposed to strict equality is indeed to have weaker assumptions. It can definitely be awkward sometimes though. $\endgroup$
    – Ms. Molly Stewart-Gallus
    Commented Jul 27, 2022 at 17:48

Not the answer you're looking for? Browse other questions tagged or ask your own question.