Injection/inclusion in Propositional Resizing 2.18.6, or rather just "map"?

[marcbezem]

We recently changed from "inclusion" to "injection" in Propositional Resizing 2.18.6. I added the definition $P\mapsto P$ and a cautioning footnote that this is not the identity map, and well-typed because of cumulativity. However, the only proof that I could find that this map is indeed an injection uses UA (which is an axiom that has some resizing effect as well). My proof goes as follows. Let U,V be universes with U:V. Define the map $i :\equiv P\mapsto P : Prop_U \to Prop_V$ and let $Q: Prop_V$. We have to show that the fiber of $i$ at $Q$ is a proposition. Let $((P,!),p),((P',!),p')$ be elements of this fiber. We need a path from $P$ to $P'$ in U, but we only have one via $Q$ in V, using $p,p'$. The latter gives us functions between $P$ and $P'$ that are each other's inverses. From this we get an equivalence from $P$ to $P'$, and then from UA we get the desired path in U. BTW the types of the !'s get a lift under $i$ as well, but that should be OK.

I hope this argument is correct, but even so I find it too complicated. I also don't like that the statement of a "Principle" depends on an axiom such as UA. So I would vote for "map", or back to "inclusion", unless I'm overlooking a simpler argument.

[pierrecagne]

The way we define identity types in the book is not universe dependent: we say that a = b exists as a type for a,b: X, and moreover if X is in U then so is a = b. So here from p: Q = P (which is a type in any universe containing V) and p': Q = P' (which is a type in any universe containing V), you find p' . inv p : P = P' (which is a type in any universe containing U). So I think you can conclude directly without the use of UA. I might have overlooked something of course (about the ! notably).

[marcbezem]

@pierrecagne That may be true, but V is the type here. We easily get P =_V P' (which lives in the universe in which V lives, V+), and we would need P =_U P' (which we get using UA).

[pierrecagne]

We actually don't label the identity type with the type in which the elements live, so with strict cumulativity, I think it identifies definitionally the labelled versions you wrote.

But even if we make the type explicit like in the labelled version, the elimination rule stated in E3 doesn't restrict the target type family to any universe (large elimination is the technical term iirc) so we can define for all P,P' propositions of U, an equivalence from P =_U P' to P =_V P' by induction on P', right? Then one is contractible exactly when the other is, and we avoid UA that way.

[pierrecagne]

For the sake of remembering what is going on, @marcbezem rightly pointed out that the construction I proposed above does not work: we can definitely construct a map i : Π (P' : Propᵁ) (P =ᵁ P') → (P =ⱽ P') by path-induction. However, constructing a pointwise inverse to i is not that easy. Indeed, P' ranges over propositions in U, not in V, and so path-induction can't be used to define the wanted map of type Π (P' : Propᵁ) (P =ⱽ P') → (P =ᵁ P').

[marcbezem]

We discussed this with @martinescardo, @dybjer and @coquand. Two important observations came out of that discussion.

1. Martin's https://www.cs.bham.ac.uk/~mhe/TypeTopology/UF.Equiv-FunExt.html#propext-funext-give-prop-ua shows that propext and funext give univalence for propositions, which is sufficent for the "injection".

2. There are currently nine occurrences of "resizing" in the book, and none of them seems essential. So where do we essentially use propositional resizing? It is of course quite possible that there is some hidden use in some of the !'s, or when we leave out proofs of propositions. After all, even writing (or thinking) P = Q requires that P and Q are in the same universe (Big Typechecker is watching you :-).

As an afterthought after the discussion:

3. Is it consistent to have all Prop_U's definitionally equal? If so, that would solve all our typing problems and perhaps be the simplest for our readers. We would no doubt sacrifice some interesting models, but as long as we can keep some good ones it would be fine. (It is not consistent to have all Set_U's definitionally equal when you have UA, w.i.p. BCDE.)

[UlrikBuchholtz]

2. There are currently nine occurrences of "resizing" in the book, and none of them seems essential. So where do we essentially use propositional resizing?

I think nothing we do should depend on propositional resizing. (So the remark that we sometimes use it is perhaps overstated.) -- Of course, if you want power sets to be independent of the universe of propositions, you need it, and also to have these be complete lattices, but no group theory should depend on it. If we do Dedekind reals, it follows that these form a set independent of the universe level, but this is of course much weaker.

3. Is it consistent to have all Prop_U's definitionally equal? If so, that would solve all our typing problems and perhaps be the simplest for our readers. We would no doubt sacrifice some interesting models, but as long as we can keep some good ones it would be fine. (It is not consistent to have all Set_U's definitionally equal when you have UA, w.i.p. BCDE.)

I think this is wide open, along with consistency of Voevodsky's judgmental resizing, which is closely related. (If P : Prop_V, then P : Prop_U, for universes U, V.) None of the usual model constructions satisfy these.

[martinescardo]

Hi, after @marcbezem's @ to me. It would be indeed nice to avoid propositional resizing, if possible.

[martinescardo]

But all the models satisfy the axioms of propositional resizing. What is open is whether the rules of propositional resizing has a model. In any case, so far we don't know any constructive model that satisfies the resizing axioms, although Andrew Swan is getting close, as reported in his HoTTEST talk last Thursday.

[martinescardo]

The above assumes a classical meta-theory. But, at present, even the fact that infty-toposes are models of HoTT/UF assume a classical meta-theory.

[marcbezem]

Please take a look at e1e1925. I did not include an exercise yet, but this can be done if deemed important. If everybody is happy, the issue can be closed.

[UlrikBuchholtz]

I'm happy. (BTW, I can't attend our meeting today, so I'll see you next week.)

[bidundas]

It turns out that I won’t have an Internet connection during the book meeting so I’ll have to skip today too

Bjorn

On 16 Feb 2023, at 14:28, Ulrik Buchholtz @.***> wrote:



I'm happy. (BTW, I can't attend our meeting today, so I'll see you next week.)

— Reply to this email directly, view it on GitHubhttps://github.com/UniMath/SymmetryBook/issues/177#issuecomment-1433089142, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AKO2SKZHXGXIP7SN76E3TFTWXYTPRANCNFSM6AAAAAAUU6JNR4. You are receiving this because you are subscribed to this thread.Message ID: @.***>

[pierrecagne]

Did you mean c2aac7e624a245d040a87172eea335ee813be382?

Seems good to me!

[marcbezem]

@pierrecagne yes (but Ulrik's commit is also good!).