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}