Martin Escardo 24th January 2019

Size matters.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan

module Lifting.Size (𝓣 : Universe) where

open import Lifting.IdentityViaSIP
open import Lifting.Construction 𝓣
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Size
open import UF.SubtypeClassifier
open import UF.Subsingletons
open import UF.UA-FunExt
open import UF.Univalence

\end{code}

As one can see from the definition of 𝓛, we have that 𝓛 lives in a
universe strictly higher than that of X in general:

\begin{code}

private
 the-universe-of-𝓛 : (X : 𝓀 Μ‡ ) β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
 the-universe-of-𝓛 = 𝓛

\end{code}

However, if the argument is in 𝓣 ⁺ βŠ” 𝓀, then the size doesn't
increase:

\begin{code}

private
 𝓛-universe-preservation : (X : 𝓣 ⁺ βŠ” 𝓀 Μ‡ ) β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
 𝓛-universe-preservation = 𝓛

\end{code}

In particular, after the first application of 𝓛, further applications
don't increase the size:

\begin{code}

private
 the-universe-of-𝓛𝓛 : (X : 𝓀 Μ‡ ) β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
 the-universe-of-𝓛𝓛 X = 𝓛 (𝓛 X)

\end{code}

As a particular case of the above, if 𝓣 and 𝓀 are the same universe,
then the first application of 𝓛 has its result in the next universe 𝓣⁺.

\begin{code}

private
 the-universe-of-𝓛' : (X : 𝓣 Μ‡ ) β†’ 𝓣 ⁺ Μ‡
 the-universe-of-𝓛' = 𝓛

\end{code}

But if 𝓀 is taken to be the successor 𝓣 ⁺ of 𝓣 then it is preserved by 𝓛:

\begin{code}

private
 the-universe-of-𝓛⁺ : (X : 𝓣 ⁺ Μ‡ ) β†’ 𝓣 ⁺ Μ‡
 the-universe-of-𝓛⁺ = 𝓛

\end{code}

With weak propositional resizing (any proposition of any universe has
a logically equivalent copy in any universe), 𝓛 preserves all
universes except the first, i.e., all successor universes 𝓀 ⁺.

\begin{code}

𝓛-resize : is-univalent 𝓣
         β†’ is-univalent 𝓀
         β†’ Propositional-resizing
         β†’ (X : 𝓀 ⁺ Μ‡ ) β†’ 𝓛 X is (𝓀 ⁺) small
𝓛-resize {𝓀} ua ua' ρ X = L , e
 where
  L : 𝓀 ⁺ Μ‡
  L = Ξ£ P κž‰ 𝓀 Μ‡ , (P β†’ X) Γ— is-prop P

  e : L ≃ 𝓛 X
  e = qinveq Ο† (Ξ³ , Ξ³Ο† , φγ)
   where
    Ο† : L β†’ 𝓛 X
    Ο† (P , f , i) = resize ρ P i , f ∘ from-resize ρ P i , resize-is-prop ρ P i

    Ξ³ : 𝓛 X β†’ L
    γ (Q , g , j) = resize ρ Q j , g ∘ from-resize ρ Q j , resize-is-prop ρ Q j

    φγ : (l : 𝓛 X) β†’ Ο† (Ξ³ l) ＝ l
    φγ (Q , g , j) = ⋍-gives-＝ 𝓣 ua (a , b)
     where
      a : resize ρ (resize ρ Q j) (resize-is-prop ρ Q j) ≃ Q
      a = qinveq
           (from-resize ρ Q j ∘ from-resize ρ (resize ρ Q j) (resize-is-prop ρ Q j))
           (to-resize ρ (resize ρ Q j) (resize-is-prop ρ Q j) ∘ to-resize ρ Q j ,
           (Ξ» r β†’ resize-is-prop ρ (resize ρ Q j) (resize-is-prop ρ Q j) _ r) ,
           (Ξ» q β†’ j _ q))

      b : g ∘ from-resize ρ Q j ∘ from-resize ρ (resize ρ Q j) (resize-is-prop ρ Q j) ＝ g ∘ ⌜ a ⌝
      b = ap (g ∘_) (dfunext (univalence-gives-funext ua) (Ξ» r β†’ j _ (⌜ a ⌝ r)))

    Ξ³Ο† : (m : L) β†’ Ξ³ (Ο† m) ＝ m
    Ξ³Ο† (P , f , i) = ⋍-gives-＝ 𝓀 ua' (a , b)
     where
      a : resize ρ (resize ρ P i) (resize-is-prop ρ P i) ≃ P
      a = qinveq
           (from-resize ρ P i ∘ from-resize ρ (resize ρ P i) (resize-is-prop ρ P i))
           (to-resize ρ (resize ρ P i) (resize-is-prop ρ P i) ∘ to-resize ρ P i ,
           (Ξ» r β†’ resize-is-prop ρ (resize ρ P i) (resize-is-prop ρ P i) _ r) ,
           (Ξ» q β†’ i _ q))

      b : f ∘ from-resize ρ P i ∘ from-resize ρ (resize ρ P i) (resize-is-prop ρ P i)
        ＝ f ∘ ⌜ a ⌝
      b = ap (f ∘_) (dfunext (univalence-gives-funext ua') (Ξ» r β†’ i _ (⌜ a ⌝ r)))

\end{code}

TODO. The above proof can be simplified.

NB. With a more careful treatment everywhere (including the structure
identity principle), we can relax the assumption that 𝓣 and 𝓀 are
univalent to the assumption that 𝓣 satisfies propositional and
functional extensionality. But this is probably not worth the trouble,
as it would imply developing a copy of the SIP with this different
assumption.

Added 14t Feb 2022. Actually, function extensionality and
propositional extensionality together give univalence for
propositions, as proved in the module UF.Equiv-FunExt.

Added 8th Feb 2019.

\begin{code}

𝓛-resizingβ‚€ : Ξ©-resizingβ‚€ 𝓣
            β†’ (X : 𝓣 Μ‡ ) β†’ 𝓛 X is 𝓣 small
𝓛-resizingβ‚€ (Ξ©β‚€ , eβ‚€) X = (Ξ£ p κž‰ Ξ©β‚€ , (up p holds β†’ X)) , ≃-comp d e
 where
  up : Ξ©β‚€ β†’ Ξ© 𝓣
  up = ⌜ eβ‚€ ⌝

  up-is-equiv : is-equiv up
  up-is-equiv = ⌜⌝-is-equiv eβ‚€

  d : (Ξ£ p κž‰ Ξ©β‚€ , (up p holds β†’ X)) ≃ (Ξ£ p κž‰ Ξ© 𝓣 , (p holds β†’ X))
  d = Ξ£-change-of-variable (Ξ» p β†’ p holds β†’ X) up up-is-equiv

  e : (Ξ£ p κž‰ Ξ© 𝓣 , (p holds β†’ X)) ≃ 𝓛 X
  e = qinveq (Ξ» ((P , i) , f) β†’  P , f ,  i)
             ((Ξ» (P , f  , i) β†’ (P , i) , f) ,
             (Ξ» _ β†’ refl) ,
             (Ξ» _ β†’ refl))

\end{code}

Added 15th Feb 2019. The proof is literally the same, the assumption is
more parsimonious.

\begin{code}

𝓛-resizing : Ξ©-resizing 𝓣
           β†’ (X : 𝓣 Μ‡ ) β†’ 𝓛 X is 𝓣 small
𝓛-resizing (O , Ξ΅) X = (Ξ£ p κž‰ O , (up p holds β†’ X)) , ≃-comp d e
 where
  up : O β†’ Ξ© 𝓣
  up = ⌜ Ρ ⌝

  up-is-equiv : is-equiv up
  up-is-equiv = ⌜⌝-is-equiv Ρ

  d : (Ξ£ p κž‰ O , (up p holds β†’ X)) ≃ (Ξ£ p κž‰ Ξ© 𝓣 , (p holds β†’ X))
  d = Ξ£-change-of-variable (Ξ» p β†’ p holds β†’ X) up up-is-equiv

  e : (Ξ£ p κž‰ Ξ© 𝓣 , (p holds β†’ X)) ≃ 𝓛 X
  e = qinveq (Ξ» ((P , i) , f) β†’  P , f  , i)
             ((Ξ» (P , f ,  i) β†’ (P , i) , f) ,
             (Ξ» _ β†’ refl) ,
             (Ξ» _ β†’ refl))

\end{code}