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-Lö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
  _ : f P ＝ Q
  _ = r

  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}