Skip to content

UF.UniverseEmbedding

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.)


{-# 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


Of course:


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 Ξ³


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


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'-≃ π“₯)

The following embedding has better definitional properties:


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 π“₯)

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.)


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 π“₯)

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


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 (_⁺)


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

Added 24th December 2020. Lifting of hSets.


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)