On 07/05/2019 14:51, Andreas Nuyts wrote:
> Even with cumulativity, that sounds suspicious, because cumulativity of
> U in a bigger universe V does not obviously give you a map
>
> (A B : U) -> Id V A B -> Id U A B.
>
> The J-rule does not allow you to build this map.
Indeed.
In the non-cumulative system, with V bigger than U, you have a map
f : U → V with f A ≃ A. For example, if C is any contractible type in
V, you can take f A := A × C.
If both U and V are univalent, then any map f : U → V with f A ≃ A is
an embedding for all A : U, meaning that the canonical map
Id U A B → Id V (f A) (f B)
is equivalence (or equivalently that the fibers of f are propositions).
I checked this in Agda.
The reformulation of your statement above with an explicit inclusion
f : U → V, namely
(A B : U) -> Id V (f A) (f B) -> Id U A B,
which amounts to the left-cancellability of f, is a consequence of f
being an embedding, and in general strictly weaker than f being an
embedding.
But I don't see how to prove even the left-cancellability of f without
assuming univalence in the smaller universe U.
Assuming that V is univalent, Id V (f A) (f B) gives f A ≃ f B, and
then composing with the equivalences A ≃ f A and f B ≃ B we get A ≃ B.
If U were univalent we would get Id U A B and hence f would be
left-cancellable. But, as I said, the univalence of U and V gives
more, namely that f is an embedding.
And if V is univalent and f is an embedding, then U is univalent, for
A ≃ B is equivalent to f A ≃ f B and hence to Id V (f A) (f B), and
hence to Id U A B, using the embedding property in the last step.
So if V is univalent, then the smaller universe U is univalent iff
every map f : U → V with f A ≃ A for all A : U is an embedding (iff
some given such map is an embedding).
Martin
>
> On 7/05/19 14:42, Nils Anders Danielsson wrote:
>> On 02/05/2019 22.46, escardo.martin@gmail.com wrote:
>>> I can confirm from a 26k line Agda development (with comments and
>>> repeated blank lines removed in this counting of the number of lines)
>>> that not once did I need to embed a universe into a larger universe,
>>> except when I wanted to state the theorem that any universe is a
>>> retract of any larger universe if one assumes the propositional
>>> resizing axiom (any proposition in a universe U has an equivalent copy
>>> in any universe V). So I would say that such situations are *extremely
>>> rare* in practice.
>>
>> I once wrote some code where I made use of univalence at three different
>> levels. Does anyone know if one can prove that univalence at one level
>> implies univalence at lower levels, without making use of cumulativity?