Martin Escardo, 29th January 2019

If univalence holds, then any universe is embedded into any larger universe.

We do this without cumulativity, because it is not available in the
Martin-Löf type theory that we are working with in Agda.

Moreover, any map f : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇ with f X ≃ X for all X : 𝓤 ̇ is an
embedding, e.g. the map X ↦ X + 𝟘 {𝓥}.

(Here the notion of a map being an embedding is stronger than that of
being left-cancellable, and it means that the fibers of the map are
propositions, or subsingletons, as in HoTT/UF.)

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module UF-UniverseEmbedding where

open import SpartanMLTT
open import UF-Subsingletons
open import UF-Subsingletons-FunExt
open import UF-Embeddings
open import UF-Equiv
open import UF-EquivalenceExamples
open import UF-FunExt
open import UF-Lower-FunExt
open import UF-Equiv-FunExt
open import UF-Univalence
open import UF-UA-FunExt

is-universe-embedding : (𝓤 ̇  𝓥 ̇ )  (𝓤 )  𝓥 ̇
is-universe-embedding f =  X  f X  X

\end{code}

Of course:

\begin{code}

at-most-one-universe-embedding : Univalence
(f g : 𝓤 ̇  𝓥 ̇ )
is-universe-embedding f
is-universe-embedding g
f  g
at-most-one-universe-embedding {𝓤} {𝓥} ua f g i j = p
where
h :  X  f X  g X
h X = i X  ≃-sym (j X)

H : f  g
H X = eqtoid (ua 𝓥) (f X) (g X) (h X)

p : f  g
p = dfunext (Univalence-gives-Fun-Ext ua) H

universe-embeddings-are-embeddings : Univalence
(𝓤 𝓥 : Universe) (f : 𝓤 ̇  𝓥 ̇ )
is-universe-embedding f
is-embedding f
universe-embeddings-are-embeddings ua 𝓤 𝓥 f i = embedding-criterion' f γ
where
γ : (X X' : 𝓤 ̇ )  (f X  f X')  (X  X')
γ X X' =  (f X  f X')  ≃⟨ a
(f X  f X')  ≃⟨ b
(X  X')      ≃⟨ c
(X  X')
where
a = univalence-≃ (ua 𝓥) (f X) (f X')
b = Eq-Eq-cong (Univalence-gives-FunExt ua) (i X) (i X')
c = ≃-sym (univalence-≃ (ua 𝓤) X X')

\end{code}

For instance, the following function satisfies this condition and
hence is an embedding:

\begin{code}

Lift' : (𝓥 : Universe)  𝓤 ̇  𝓤  𝓥 ̇
Lift' 𝓥 X = X + 𝟘 {𝓥}

lift' : (𝓥 : Universe) {X : 𝓤 ̇ }  X  Lift' 𝓥 X
lift' 𝓥 = inl

lower' : {𝓥 : Universe} {X : 𝓤 ̇ }  Lift' 𝓥 X  X
lower' (inl x) = x
lower' (inr x) = 𝟘-elim x

Lift'-≃ : (𝓥 : Universe) (X : 𝓤 ̇ )  Lift' 𝓥 X  X
Lift'-≃ 𝓥 X = 𝟘-rneutral'

Lift'-is-embedding : Univalence  is-embedding (Lift' {𝓤} 𝓥)
Lift'-is-embedding {𝓤} {𝓥} ua = universe-embeddings-are-embeddings ua 𝓤 (𝓤  𝓥)
(Lift' 𝓥) (Lift'-≃ 𝓥)
\end{code}

The following embedding has better definitional properties:

\begin{code}

Lift : (𝓥 : Universe)  𝓤 ̇  𝓤  𝓥 ̇
Lift 𝓥 X = X × 𝟙 {𝓥}

lift : (𝓥 : Universe) {X : 𝓤 ̇ }  X  Lift 𝓥 X
lift 𝓥 x = (x , )

lower : {X : 𝓤 ̇ }  Lift 𝓥 X  X
lower (x , ) = x

η-Lift : (𝓥 : Universe) {X : 𝓤 ̇ } (𝔁 : Lift 𝓥 X)
lift 𝓥 (lower 𝔁)  𝔁
η-Lift  𝓥 𝔁 = refl

ε-Lift : (𝓥 : Universe) {X : 𝓤 ̇ } (x : X)
lower (lift 𝓥 x)  x
ε-Lift  𝓥 x = refl

lower-is-equiv : {X : 𝓤 ̇ }  is-equiv (lower {𝓤} {𝓥} {X})
lower-is-equiv {𝓤} {𝓥} = (lift 𝓥 , ε-Lift 𝓥) , (lift 𝓥 , η-Lift 𝓥)

lift-is-equiv : {X : 𝓤 ̇ }  is-equiv (lift 𝓥 {X})
lift-is-equiv {𝓤} {𝓥} = (lower , η-Lift 𝓥) , lower , ε-Lift 𝓥

Lift-≃ : (𝓥 : Universe) (X : 𝓤 ̇ )  Lift 𝓥 X  X
Lift-≃ 𝓥 X = lower , lower-is-equiv

≃-Lift : (𝓥 : Universe) (X : 𝓤 ̇ )  X  Lift 𝓥 X
≃-Lift 𝓥 X = lift 𝓥 , lift-is-equiv

Lift-is-universe-embedding : (𝓥 : Universe)  is-universe-embedding (Lift {𝓤} 𝓥)
Lift-is-universe-embedding = Lift-≃

Lift-is-embedding : Univalence  is-embedding (Lift {𝓤} 𝓥)
Lift-is-embedding {𝓤} {𝓥} ua = universe-embeddings-are-embeddings ua 𝓤 (𝓤  𝓥)
(Lift 𝓥) (Lift-is-universe-embedding 𝓥)
\end{code}

Added 7th Feb 2019. Assuming propositional and functional
extensionality instead of univalence, the lift-fibers of propositions
are propositions. (For use in the module UF-Resize.)

\begin{code}

prop-fiber-criterion : PropExt
FunExt
(𝓤 𝓥 : Universe)
(f : 𝓤 ̇  𝓥 ̇ )
is-universe-embedding f
(Q : 𝓥 ̇ )
is-prop Q
is-prop (fiber f Q)
prop-fiber-criterion pe fe 𝓤 𝓥 f i Q j (P , r) = d (P , r)
where
k : is-prop (f P)
k = back-transport is-prop r j

l : is-prop P
l = equiv-to-prop (≃-sym (i P)) k

a : (X : 𝓤 ̇ )  (f X  f P)  (X  P)
a X = (f X  f P)  ≃⟨ prop-univalent-≃ (pe 𝓥) (fe 𝓥 𝓥) (f X) (f P) k
(f X  f P)  ≃⟨ Eq-Eq-cong fe (i X) (i P)
(X  P)      ≃⟨ ≃-sym (prop-univalent-≃ (pe 𝓤) (fe 𝓤 𝓤) X P l)
(X  P)

b : (Σ X  𝓤 ̇ , f X  f P)  (Σ X  𝓤 ̇  , X  P)
b = Σ-cong a

c : is-prop (Σ X  𝓤 ̇ , f X  f P)
c = equiv-to-prop b (singleton-types'-are-props P)

d : is-prop (Σ X  𝓤 ̇ , f X  Q)
d = transport  -  is-prop (Σ X  𝓤 ̇ , f X  -)) r c

prop-fiber-Lift : PropExt
FunExt
(Q : 𝓤  𝓥 ̇ )
is-prop Q
is-prop (fiber (Lift 𝓥) Q)
prop-fiber-Lift {𝓤} {𝓥} pe fe = prop-fiber-criterion pe fe 𝓤 (𝓤  𝓥)
(Lift {𝓤} 𝓥) (Lift-is-universe-embedding 𝓥)
\end{code}

Taken from the MGS'2019 lecture notes (22 December 2020):

\begin{code}

global-≃-ap' : Univalence
(F : Universe  Universe)
(A : {𝓤 : Universe}  𝓤 ̇  (F 𝓤) ̇ )
({𝓤 𝓥 : Universe} (X : 𝓤 ̇ )  A X  A (Lift 𝓥 X))
(X : 𝓤 ̇ ) (Y : 𝓥 ̇ )  X  Y  A X  A Y
global-≃-ap' {𝓤} {𝓥} ua F A φ X Y e =

A X          ≃⟨ φ X
A (Lift 𝓥 X) ≃⟨ idtoeq (A (Lift 𝓥 X)) (A (Lift 𝓤 Y)) q
A (Lift 𝓤 Y) ≃⟨ ≃-sym (φ Y)
A Y
where
d : Lift 𝓥 X  Lift 𝓤 Y
d = Lift 𝓥 X ≃⟨ Lift-is-universe-embedding 𝓥 X
X        ≃⟨ e
Y        ≃⟨ ≃-sym (Lift-is-universe-embedding 𝓤 Y)
Lift 𝓤 Y

p : Lift 𝓥 X  Lift 𝓤 Y
p = eqtoid (ua (𝓤  𝓥)) (Lift 𝓥 X) (Lift 𝓤 Y) d

q : A (Lift 𝓥 X)  A (Lift 𝓤 Y)
q = ap A p

global-property-of-types : 𝓤ω
global-property-of-types = {𝓤 : Universe}  𝓤 ̇  𝓤 ̇

global-property-of-types⁺ : 𝓤ω
global-property-of-types⁺ = {𝓤 : Universe}  𝓤 ̇  𝓤  ̇

cumulative : global-property-of-types  𝓤ω
cumulative A = {𝓤 𝓥 : Universe} (X : 𝓤 ̇ )  A X  A (Lift 𝓥 X)

cumulative⁺ : global-property-of-types⁺  𝓤ω
cumulative⁺ A = {𝓤 𝓥 : Universe} (X : 𝓤 ̇ )  A X  A (Lift 𝓥 X)

global-≃-ap : Univalence
(A : global-property-of-types)
cumulative A
(X : 𝓤 ̇ ) (Y : 𝓥 ̇ )  X  Y  A X  A Y
global-≃-ap ua = global-≃-ap' ua id

global-≃-ap⁺ : Univalence
(A : global-property-of-types⁺)
cumulative⁺ A
(X : 𝓤 ̇ ) (Y : 𝓥 ̇ )  X  Y  A X  A Y
global-≃-ap⁺ ua = global-≃-ap' ua (_⁺)

\end{code}

Cumulativity in the above sense doesn't always hold. See the module
LawvereFPT for a counter-example.

Added 24th December 2020. Lifting of hSets.

\begin{code}

Lift-is-set :  {𝓤} 𝓥 (X : 𝓤 ̇ )  is-set X  is-set (Lift 𝓥 X)
Lift-is-set 𝓥 X X-is-set = equiv-to-set
(Lift-is-universe-embedding 𝓥 X)
X-is-set

Lift-hSet : (𝓥 : Universe)  hSet 𝓤  hSet (𝓤  𝓥)
Lift-hSet 𝓥 = pair-fun (Lift 𝓥) (Lift-is-set 𝓥)

Lift-is-set-is-embedding : funext (𝓤  𝓥) (𝓤  𝓥)
(X : 𝓤 ̇ )  is-embedding (Lift-is-set 𝓥 X)
Lift-is-set-is-embedding {𝓤} {𝓥} fe X = maps-of-props-are-embeddings
(Lift-is-set 𝓥 X)
(being-set-is-prop (lower-funext 𝓥 𝓥 fe))
(being-set-is-prop fe)

Lift-hSet-is-embedding : Univalence
is-embedding (Lift-hSet {𝓤} 𝓥)
Lift-hSet-is-embedding {𝓤} {𝓥} ua = pair-fun-is-embedding
(Lift 𝓥)
(Lift-is-set 𝓥)
(Lift-is-embedding ua)
(Lift-is-set-is-embedding
(Univalence-gives-FunExt ua (𝓤  𝓥) (𝓤  𝓥)))

is-hSet-embedding : (hSet 𝓤  hSet 𝓥)  (𝓤 )  𝓥 ̇
is-hSet-embedding {𝓤} {𝓥} f = (𝓧 : hSet 𝓤)  underlying-set (f 𝓧)
underlying-set 𝓧

at-most-one-hSet-embedding : Univalence
(f g : hSet 𝓤  hSet 𝓥 )
is-hSet-embedding f
is-hSet-embedding g
f  g
at-most-one-hSet-embedding {𝓤} {𝓥} ua f g i j = p
where
h :  𝓧  underlying-set (f 𝓧)  underlying-set (g 𝓧)
h 𝓧 = i 𝓧  ≃-sym (j 𝓧)

H : f  g
H 𝓧 = to-subtype-≡
𝓨  being-set-is-prop (univalence-gives-funext (ua 𝓥)))
(eqtoid (ua 𝓥) (underlying-set (f 𝓧)) (underlying-set (g 𝓧)) (h 𝓧))

p : f  g
p = dfunext (Univalence-gives-FunExt ua (𝓤 ) (𝓥 )) H

the-only-hSet-embedding-is-Lift-hSet : Univalence
(f : hSet 𝓤  hSet (𝓤  𝓥 ))
is-hSet-embedding f
f  Lift-hSet 𝓥
the-only-hSet-embedding-is-Lift-hSet {𝓤} {𝓥} ua f i =
at-most-one-hSet-embedding ua f
(Lift-hSet 𝓥) i
𝓧  Lift-is-universe-embedding 𝓥 (underlying-set 𝓧))

hSet-embeddings-are-embeddings : Univalence
(f : hSet 𝓤  hSet (𝓤  𝓥 ))
is-hSet-embedding f
is-embedding f
hSet-embeddings-are-embeddings {𝓤} {𝓥} ua f i =
transport is-embedding
((the-only-hSet-embedding-is-Lift-hSet ua f i)⁻¹)
(Lift-hSet-is-embedding {𝓤} {𝓥} ua)

\end{code}