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 --safe --without-K #-}

module UF.UniverseEmbedding where

open import MLTT.Spartan
open import UF.Embeddings
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Lower-FunExt
open import UF.PairFun
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.UA-FunExt
open import UF.Univalence

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 = Ξ΄
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 = β-cong (Univalence-gives-FunExt ua) (i X) (i X')
c = β-sym (univalence-β (ua π€) X X')

Ξ΄ : is-embedding f
Ξ΄ = embedding-criterion' f Ξ³

\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, then 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 = 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)  ββ¨ β-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 (Ξ» π€ β π€)

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}