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 β©