Martin Escardo 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

\begin{code}

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

module MGS.Universe-Lifting where

open import MGS.Equivalence-Constructions
open import MGS.Embeddings public

record Lift {𝓀 : Universe} (π“₯ : Universe) (X : 𝓀 Μ‡ ) : 𝓀 βŠ” π“₯ Μ‡  where
 constructor
  lift
 field
  lower : X

open Lift public

type-of-Lift  :             type-of (Lift  {𝓀} π“₯)       ＝ (𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡ )
type-of-lift  : {X : 𝓀 Μ‡ } β†’ type-of (lift  {𝓀} {π“₯} {X}) ＝ (X β†’ Lift π“₯ X)
type-of-lower : {X : 𝓀 Μ‡ } β†’ type-of (lower {𝓀} {π“₯} {X}) ＝ (Lift π“₯ X β†’ X)

type-of-Lift  = refl _
type-of-lift  = refl _
type-of-lower = refl _

Lift-induction : βˆ€ {𝓀} π“₯ (X : 𝓀 Μ‡ ) (A : Lift π“₯ X β†’ 𝓦 Μ‡ )
               β†’ ((x : X) β†’ A (lift x))
               β†’ (l : Lift π“₯ X) β†’ A l

Lift-induction π“₯ X A Ο† (lift x) = Ο† x

Lift-recursion : βˆ€ {𝓀} π“₯ {X : 𝓀 Μ‡ } {B : 𝓦 Μ‡ }
               β†’ (X β†’ B) β†’ Lift π“₯ X β†’ B

Lift-recursion π“₯ {X} {B} = Lift-induction π“₯ X (Ξ» _ β†’ B)

lower-lift : {X : 𝓀 Μ‡ } (x : X) β†’ lower {𝓀} {π“₯} (lift x) ＝ x
lower-lift = refl

lift-lower : {X : 𝓀 Μ‡ } (l : Lift π“₯ X) β†’ lift (lower l) ＝ l
lift-lower = refl

Lift-≃ : (X : 𝓀 Μ‡ ) β†’ Lift π“₯ X ≃ X
Lift-≃ {𝓀} {π“₯} X = invertibility-gives-≃ lower
                     (lift , lift-lower , lower-lift {𝓀} {π“₯})

≃-Lift : (X : 𝓀 Μ‡ ) β†’ X ≃ Lift π“₯ X
≃-Lift {𝓀} {π“₯} X = invertibility-gives-≃ lift
                     (lower , lower-lift {𝓀} {π“₯} , lift-lower)

lower-dfunext : βˆ€ 𝓦 𝓣 𝓀 π“₯ β†’ dfunext (𝓀 βŠ” 𝓦) (π“₯ βŠ” 𝓣) β†’ dfunext 𝓀 π“₯
lower-dfunext 𝓦 𝓣 𝓀 π“₯ fe {X} {A} {f} {g} h = p
 where
  A' : Lift 𝓦 X β†’ π“₯ βŠ” 𝓣 Μ‡
  A' y = Lift 𝓣 (A (lower y))

  f' g' : Ξ  A'
  f' y = lift (f (lower y))
  g' y = lift (g (lower y))

  h' : f' ∼ g'
  h' y = ap lift (h (lower y))

  p' : f' ＝ g'
  p' = fe h'

  p : f ＝ g
  p = ap (Ξ» f' x β†’ lower (f' (lift x))) p'

universe-embedding-criterion : is-univalent 𝓀
                             β†’ is-univalent (𝓀 βŠ” π“₯)
                             β†’ (f : 𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡ )
                             β†’ ((X : 𝓀 Μ‡ ) β†’ f X ≃ X)
                             β†’ is-embedding f

universe-embedding-criterion {𝓀} {π“₯} ua ua' f e = embedding-criterion f Ξ³
 where
  fe : dfunext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
  fe = univalence-gives-dfunext ua'

  feβ‚€ : dfunext 𝓀 𝓀
  feβ‚€ = lower-dfunext π“₯ π“₯ 𝓀 𝓀 fe

  fe₁ : dfunext 𝓀 (𝓀 βŠ” π“₯)
  fe₁ = lower-dfunext π“₯ π“₯ 𝓀 (𝓀 βŠ” π“₯) fe

  Ξ³ : (X X' : 𝓀 Μ‡ ) β†’ (f X ＝ f X') ≃ (X ＝ X')
  Ξ³ X X' =  (f X ＝ f X')  β‰ƒβŸ¨ i ⟩
            (f X ≃ f X')  β‰ƒβŸ¨ ii ⟩
            (X ≃ X')      β‰ƒβŸ¨ iii ⟩
            (X ＝ X')      β– 
   where
    i   = univalence-≃ ua' (f X) (f X')
    ii  = Eq-Eq-cong' fe fe fe fe fe feβ‚€ fe₁ fe feβ‚€ feβ‚€ feβ‚€ feβ‚€ (e X) (e X')
    iii = ≃-sym (univalence-≃ ua X X')

Lift-is-embedding : is-univalent 𝓀 β†’ is-univalent (𝓀 βŠ” π“₯)
                  β†’ is-embedding (Lift {𝓀} π“₯)

Lift-is-embedding {𝓀} {π“₯} ua ua' = universe-embedding-criterion {𝓀} {π“₯} ua ua'
                                    (Lift π“₯) Lift-≃

module _ {𝓀 π“₯ : Universe}
         (ua : is-univalent π“₯)
         (ua' : is-univalent (𝓀 βŠ” π“₯))
 where

 private
  fe : dfunext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
  fe = univalence-gives-dfunext ua'

  feβ‚€ : dfunext π“₯ (𝓀 βŠ” π“₯)
  feβ‚€ = lower-dfunext 𝓀 𝓀 π“₯ (𝓀 βŠ” π“₯) fe

  fe₁ : dfunext 𝓀 (𝓀 βŠ” π“₯)
  fe₁ = lower-dfunext (𝓀 βŠ” π“₯) 𝓀 𝓀 (𝓀 βŠ” π“₯) fe

  feβ‚‚ : dfunext π“₯ π“₯
  feβ‚‚ = lower-dfunext 𝓀 𝓀 π“₯ π“₯ fe

  fe₃ : dfunext 𝓀 𝓀
  fe₃ = lower-dfunext π“₯ π“₯ 𝓀 𝓀 fe

 univalenceβ†’' : (X : 𝓀 Μ‡ ) β†’ is-subsingleton (Ξ£ Y κž‰ π“₯ Μ‡ , X ≃ Y)
 univalence→' X = s
  where
   e : (Y : π“₯ Μ‡ ) β†’ (X ≃ Y) ≃ (Lift 𝓀 Y ＝ Lift π“₯ X)
   e Y = (X ≃ Y)                 β‰ƒβŸ¨ i ⟩
         (Y ≃ X)                 β‰ƒβŸ¨ ii ⟩
         (Lift 𝓀 Y ≃ Lift π“₯ X)   β‰ƒβŸ¨ iii ⟩
         (Lift 𝓀 Y ＝ Lift π“₯ X)   β– 
    where
     i   = ≃-Sym feβ‚€ fe₁ fe
     ii  = Eq-Eq-cong' fe₁ fe feβ‚‚ fe₁ fe fe fe fe₃
             fe fe fe fe (≃-Lift Y) (≃-Lift X)
     iii = ≃-sym (univalence-≃ ua' (Lift 𝓀 Y) (Lift π“₯ X))

   d : (Ξ£ Y κž‰ π“₯ Μ‡ , X ≃ Y) ≃ (Ξ£ Y κž‰ π“₯ Μ‡ , Lift 𝓀 Y ＝ Lift π“₯ X)
   d = Ξ£-cong e

   j : is-subsingleton (Ξ£ Y κž‰ π“₯ Μ‡ , Lift 𝓀 Y ＝ Lift π“₯ X)
   j = Lift-is-embedding ua ua' (Lift π“₯ X)

   abstract
    s : is-subsingleton (Ξ£ Y κž‰ π“₯ Μ‡ , X ≃ Y)
    s = equiv-to-subsingleton d j

 univalenceβ†’'-dual : (Y : 𝓀 Μ‡ ) β†’ is-subsingleton (Ξ£ X κž‰ π“₯ Μ‡ , X ≃ Y)
 univalence→'-dual Y = equiv-to-subsingleton e i
  where
   e : (Ξ£ X κž‰ π“₯ Μ‡ , X ≃ Y) ≃ (Ξ£ X κž‰ π“₯ Μ‡ , Y ≃ X)
   e = Ξ£-cong (Ξ» X β†’ ≃-Sym fe₁ feβ‚€ fe)

   i : is-subsingleton (Ξ£ X κž‰ π“₯ Μ‡ , Y ≃ X)
   i = univalence→' Y

univalenceβ†’'' : is-univalent (𝓀 βŠ” π“₯)
              β†’ (X : 𝓀 Μ‡ ) β†’ is-subsingleton (Ξ£ Y κž‰ 𝓀 βŠ” π“₯ Μ‡ , X ≃ Y)

univalence→'' ua = univalence→' ua ua

univalenceβ†’''-dual : is-univalent (𝓀 βŠ” π“₯)
                   β†’ (Y : 𝓀 Μ‡ ) β†’ is-subsingleton (Ξ£ X κž‰ 𝓀 βŠ” π“₯ Μ‡ , X ≃ Y)

univalence→''-dual ua = univalence→'-dual ua ua

G↑-≃ : is-univalent (𝓀 βŠ” π“₯)
     β†’ (X : 𝓀 Μ‡ ) (A : (Ξ£ Y κž‰ 𝓀 βŠ” π“₯ Μ‡ , X ≃ Y) β†’ 𝓦 Μ‡ )
     β†’ A (Lift π“₯ X , ≃-Lift X) β†’ (Y : 𝓀 βŠ” π“₯ Μ‡ ) (e : X ≃ Y) β†’ A (Y , e)

G↑-≃ {𝓀} {π“₯} ua X A a Y e = transport A p a
 where
  t : Ξ£ Y κž‰ 𝓀 βŠ” π“₯ Μ‡ , X ≃ Y
  t = (Lift π“₯ X , ≃-Lift X)

  p : t ＝ (Y , e)
  p = univalenceβ†’'' {𝓀} {π“₯} ua X t (Y , e)

H↑-≃ : is-univalent (𝓀 βŠ” π“₯)
     β†’ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ X ≃ Y β†’ 𝓦 Μ‡ )
     β†’ A (Lift π“₯ X) (≃-Lift X) β†’ (Y : 𝓀 βŠ” π“₯ Μ‡ ) (e : X ≃ Y) β†’ A Y e

H↑-≃ ua X A = G↑-≃ ua X (Ξ£-induction A)

J↑-≃ : is-univalent (𝓀 βŠ” π“₯)
     β†’ (A : (X : 𝓀 Μ‡ ) (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ X ≃ Y β†’ 𝓦 Μ‡ )
     β†’ ((X : 𝓀 Μ‡ ) β†’ A X (Lift π“₯ X) (≃-Lift X))
     β†’ (X : 𝓀 Μ‡ ) (Y : 𝓀 βŠ” π“₯ Μ‡ ) (e : X ≃ Y) β†’ A X Y e

J↑-≃ ua A Ο† X = H↑-≃ ua X (A X) (Ο† X)

H↑-equiv : is-univalent (𝓀 βŠ” π“₯)
         β†’ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ (X β†’ Y) β†’ 𝓦 Μ‡ )
         β†’ A (Lift π“₯ X) lift β†’ (Y : 𝓀 βŠ” π“₯ Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ A Y f

H↑-equiv {𝓀} {π“₯} {𝓦} ua X A a Y f i = Ξ³ (f , i)
 where
  B : (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ X ≃ Y β†’ 𝓦 Μ‡
  B Y (f , i) = A Y f

  b : B (Lift π“₯ X) (≃-Lift X)
  b = a

  Ξ³ : (e : X ≃ Y) β†’ B Y e
  Ξ³ = H↑-≃ ua X B b Y

J↑-equiv : is-univalent (𝓀 βŠ” π“₯)
         β†’ (A : (X : 𝓀 Μ‡ ) (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ (X β†’ Y) β†’ 𝓦 Μ‡ )
         β†’ ((X : 𝓀 Μ‡ ) β†’ A X (Lift π“₯ X) lift)
         β†’ (X : 𝓀 Μ‡ ) (Y : 𝓀 βŠ” π“₯ Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ A X Y f

J↑-equiv ua A Ο† X = H↑-equiv ua X (A X) (Ο† X)

J↑-invertible : is-univalent (𝓀 βŠ” π“₯)
              β†’ (A : (X : 𝓀 Μ‡ ) (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ (X β†’ Y) β†’ 𝓦 Μ‡ )
              β†’ ((X : 𝓀 Μ‡ ) β†’ A X (Lift π“₯ X) lift)
              β†’ (X : 𝓀 Μ‡ ) (Y : 𝓀 βŠ” π“₯ Μ‡ ) (f : X β†’ Y) β†’ invertible f β†’ A X Y f

J↑-invertible ua A Ο† X Y f i = J↑-equiv ua A Ο† X Y f (invertibles-are-equivs f i)

lift-is-hae : (X : 𝓀 Μ‡ ) β†’ is-hae {𝓀} {𝓀 βŠ” π“₯} {X} {Lift π“₯ X} (lift {𝓀} {π“₯})
lift-is-hae {𝓀} {π“₯} X = lower ,
                        lower-lift {𝓀} {π“₯} ,
                        lift-lower ,
                        Ξ» x β†’ refl (refl (lift x))

equivs-are-haes↑ : is-univalent (𝓀 βŠ” π“₯)
                 β†’ {X : 𝓀 Μ‡ } {Y : 𝓀 βŠ” π“₯ Μ‡ } (f : X β†’ Y)
                 β†’ is-equiv f β†’ is-hae f

equivs-are-haes↑ {𝓀} {π“₯} ua {X} {Y} = J↑-equiv {𝓀} {π“₯} ua (Ξ» X Y f β†’ is-hae f)
                                       lift-is-hae X Y

G↓-≃ : is-univalent (𝓀 βŠ” π“₯)
     β†’ (Y : 𝓀 Μ‡ ) (A : (Ξ£ X κž‰ 𝓀 βŠ” π“₯ Μ‡ , X ≃ Y) β†’ 𝓦 Μ‡ )
     β†’ A (Lift π“₯ Y , Lift-≃ Y) β†’ (X : 𝓀 βŠ” π“₯ Μ‡ ) (e : X ≃ Y) β†’ A (X , e)

G↓-≃ {𝓀} {π“₯} ua Y A a X e = transport A p a
 where
  t : Ξ£ X κž‰ 𝓀 βŠ” π“₯ Μ‡ , X ≃ Y
  t = (Lift π“₯ Y , Lift-≃ Y)

  p : t ＝ (X , e)
  p = univalenceβ†’'-dual {𝓀} {𝓀 βŠ” π“₯} ua ua Y t (X , e)

H↓-≃ : is-univalent (𝓀 βŠ” π“₯)
     β†’ (Y : 𝓀 Μ‡ ) (A : (X : 𝓀 βŠ” π“₯ Μ‡ ) β†’ X ≃ Y β†’ 𝓦 Μ‡ )
     β†’ A (Lift π“₯ Y) (Lift-≃ Y) β†’ (X : 𝓀 βŠ” π“₯ Μ‡ ) (e : X ≃ Y) β†’ A X e

H↓-≃ ua Y A = G↓-≃ ua Y (Ξ£-induction A)

J↓-≃ : is-univalent (𝓀 βŠ” π“₯)
     β†’ (A : (X : 𝓀 βŠ” π“₯ Μ‡ ) (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ 𝓦 Μ‡ )
     β†’ ((Y : 𝓀 Μ‡ ) β†’ A (Lift π“₯ Y) Y (Lift-≃ Y))
     β†’ (X : 𝓀 βŠ” π“₯ Μ‡ ) (Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A X Y e

J↓-≃ ua A Ο† X Y = H↓-≃ ua Y (Ξ» X β†’ A X Y) (Ο† Y) X

H↓-equiv : is-univalent (𝓀 βŠ” π“₯)
         β†’ (Y : 𝓀 Μ‡ ) (A : (X : 𝓀 βŠ” π“₯ Μ‡ ) β†’ (X β†’ Y) β†’ 𝓦 Μ‡ )
         β†’ A (Lift π“₯ Y) lower β†’ (X : 𝓀 βŠ” π“₯ Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ A X f

H↓-equiv {𝓀} {π“₯} {𝓦} ua Y A a X f i = Ξ³ (f , i)
 where
  B : (X : 𝓀 βŠ” π“₯ Μ‡ ) β†’ X ≃ Y β†’ 𝓦 Μ‡
  B X (f , i) = A X f

  b : B (Lift π“₯ Y) (Lift-≃ Y)
  b = a

  Ξ³ : (e : X ≃ Y) β†’ B X e
  Ξ³ = H↓-≃ ua Y B b X

J↓-equiv : is-univalent (𝓀 βŠ” π“₯)
         β†’ (A : (X : 𝓀 βŠ” π“₯ Μ‡ ) (Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ 𝓦 Μ‡ )
         β†’ ((Y : 𝓀 Μ‡ ) β†’ A (Lift π“₯ Y) Y lower)
         β†’ (X : 𝓀 βŠ” π“₯ Μ‡ ) (Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ A X Y f

J↓-equiv ua A Ο† X Y = H↓-equiv ua Y (Ξ» X β†’ A X Y) (Ο† Y) X

J↓-invertible : is-univalent (𝓀 βŠ” π“₯)
              β†’ (A : (X : 𝓀 βŠ” π“₯ Μ‡ ) (Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ 𝓦 Μ‡ )
              β†’ ((Y : 𝓀 Μ‡ ) β†’ A (Lift π“₯ Y) Y lower)
              β†’ (X : 𝓀 βŠ” π“₯ Μ‡ ) (Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ invertible f β†’ A X Y f

J↓-invertible ua A Ο† X Y f i = J↓-equiv ua A Ο† X Y f (invertibles-are-equivs f i)

lower-is-hae : (X : 𝓀 Μ‡ ) β†’ is-hae (lower {𝓀} {π“₯} {X})
lower-is-hae {𝓀} {π“₯} X = lift ,
                         lift-lower ,
                         lower-lift {𝓀} {π“₯} ,
                         (Ξ» x β†’ refl (refl (lower x)))

equivs-are-haes↓ : is-univalent (𝓀 βŠ” π“₯)
                 β†’ {X : 𝓀 βŠ” π“₯ Μ‡ } {Y : 𝓀 Μ‡ } (f : X β†’ Y)
                 β†’ is-equiv f β†’ is-hae f

equivs-are-haes↓ {𝓀} {π“₯} ua {X} {Y} = J↓-equiv {𝓀} {π“₯} ua (Ξ» X Y f β†’ is-hae f)
                                       lower-is-hae X Y

Idβ†’Eq-is-hae' : is-univalent 𝓀 β†’ is-univalent (𝓀 ⁺)
              β†’ {X Y : 𝓀 Μ‡ } β†’ is-hae (Idβ†’Eq X Y)

Idβ†’Eq-is-hae' ua ua⁺ {X} {Y} = equivs-are-haes↓ ua⁺ (Idβ†’Eq X Y) (ua X Y)

Idβ†’Eq-is-hae : is-univalent 𝓀
             β†’ {X Y : 𝓀 Μ‡ } β†’ is-hae (Idβ†’Eq X Y)

Id→Eq-is-hae ua {X} {Y} = invertibles-are-haes (Id→Eq X Y)
                           (equivs-are-invertible (Id→Eq X Y) (ua X Y))

global-property-of-types : 𝓀ω
global-property-of-types = {𝓀 : Universe} β†’ 𝓀 Μ‡ β†’ 𝓀 Μ‡

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' : 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) β‰ƒβŸ¨ Idβ†’Eq (A (Lift π“₯ X)) (A (Lift 𝓀 Y)) q ⟩
  A (Lift 𝓀 Y) β‰ƒβŸ¨ ≃-sym (Ο† Y) ⟩
  A Y          β– 
 where
  d : Lift π“₯ X ≃ Lift 𝓀 Y
  d = Lift π“₯ X β‰ƒβŸ¨ Lift-≃ X ⟩
      X        β‰ƒβŸ¨ e ⟩
      Y        β‰ƒβŸ¨ ≃-sym (Lift-≃ Y) ⟩
      Lift 𝓀 Y β– 

  p : Lift π“₯ X ＝ Lift 𝓀 Y
  p = Eqβ†’Id (ua (𝓀 βŠ” π“₯)) (Lift π“₯ X) (Lift 𝓀 Y) d

  q : A (Lift π“₯ X) ＝ A (Lift 𝓀 Y)
  q = ap A p

global-≃-ap ua = global-≃-ap' ua id

\end{code}