Martin Escardo, 24th January 2019.
With several additions after that, including by Tom de Jong.

Voedvodsky (Types'2011) considered resizing rules for a type theory
for univalent foundations. These rules govern the syntax of the formal
system, and hence are of a meta-mathematical nature.

Here we instead formulate, in our type theory without such rules, a
mathematical resizing principle. This principle is provable in the
system with Voevodsky's rules. But we don't postulate this principle
as an axiom. Instead, we use it an assumption, when needed, or as a
conclusion, when it follows from stronger principles, such as excluded
middle.

The consistency of the resizing rules is an open problem at the time
of writing (30th January 2018), but the resizing principle is
consistent relative to ZFC with Grothendieck universes, because it
follows from excluded middle, which is known to be validated by the
simplicial-set model (assuming classical logic in its development).

We develop some consequences of propositional resizing here, such as
the fact that every universe is a retract of any higher universe,
where the section is an embedding (its fibers are all propositions),
which seems to be a new result.

\begin{code}

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

module UF.Size where

open import MLTT.Spartan
open import UF.Base
open import UF.ClassicalLogic
open import UF.Embeddings
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.ExitPropTrunc
open import UF.FunExt
open import UF.Hedberg
open import UF.KrausLemma
open import UF.PropIndexedPiSigma
open import UF.PropTrunc
open import UF.Retracts
open import UF.Section-Embedding
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import UF.UA-FunExt
open import UF.Univalence
open import UF.UniverseEmbedding

\end{code}

We say that a type X has size π“₯, or that it is π“₯ small if it is
equivalent to a type in the universe π“₯:

\begin{code}

_is_small : 𝓀 Μ‡ β†’ (π“₯ : Universe) β†’ π“₯ ⁺  βŠ” 𝓀 Μ‡
X is π“₯ small = Ξ£ Y κž‰ π“₯ Μ‡ , Y ≃ X

native-size : (X : 𝓀 Μ‡ ) β†’ X is 𝓀 small
native-size X = X , ≃-refl X

resized : (X : 𝓀 Μ‡ ) β†’ X is π“₯ small β†’ π“₯ Μ‡
resized X = pr₁

resizing-condition : {X : 𝓀 Μ‡ } (s : X is π“₯ small)
                   β†’ resized X s ≃ X
resizing-condition = prβ‚‚

\end{code}

Obsolete notation used in some publications:

\begin{code}

private
 _has-size_ : 𝓀 Μ‡ β†’ (π“₯ : Universe) β†’ π“₯ ⁺  βŠ” 𝓀 Μ‡
 X has-size π“₯ = X is π“₯ small

\end{code}

The preferred terminology is now "_is_small", but it is better to keep
the terminology "_has-size_" in the papers that have already been
published, in particular "Injective types in univalent mathematics".

\begin{code}

propositional-resizing : (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
propositional-resizing 𝓀 π“₯ = (P : 𝓀 Μ‡ ) β†’ is-prop P β†’ P is π“₯ small

Propositional-Resizing : 𝓀ω
Propositional-Resizing = {𝓀 π“₯ : Universe} β†’ propositional-resizing 𝓀 π“₯

\end{code}

Propositional resizing from a universe to a higher universe just
holds, of course:

\begin{code}

resize-up : (X : 𝓀 Μ‡ ) β†’ X is (𝓀 βŠ” π“₯) small
resize-up {𝓀} {π“₯} X = Lift π“₯ X , Lift-is-universe-embedding π“₯ X

resize-up-proposition : propositional-resizing 𝓀 (𝓀 βŠ” π“₯)
resize-up-proposition {𝓀} {π“₯} P i = resize-up {𝓀} {π“₯} P

\end{code}

We use the following to work with propositional resizing more
abstractly. We first define the type of some functions and then define
them.

\begin{code}

resize : propositional-resizing 𝓀 π“₯ β†’ (P : 𝓀 Μ‡ ) (i : is-prop P) β†’ π“₯ Μ‡

resize-is-prop : (ρ : propositional-resizing 𝓀 π“₯) (P : 𝓀 Μ‡ ) (i : is-prop P)
               β†’ is-prop (resize ρ P i)

to-resize : (ρ : propositional-resizing 𝓀 π“₯) (P : 𝓀 Μ‡ ) (i : is-prop P)
          β†’ P β†’ resize ρ P i

from-resize : (ρ : propositional-resizing 𝓀 π“₯) (P : 𝓀 Μ‡ ) (i : is-prop P)
            β†’ resize ρ P i β†’ P

to-resize-is-equiv : (ρ : propositional-resizing 𝓀 π“₯) (P : 𝓀 Μ‡ ) (i : is-prop P)
                   β†’ is-equiv (to-resize ρ P i)

from-resize-is-equiv : (ρ : propositional-resizing 𝓀 π“₯) (P : 𝓀 Μ‡ ) (i : is-prop P)
                     β†’ is-equiv (from-resize ρ P i)

\end{code}

Definitions:

\begin{code}

resize               {𝓀} {π“₯} ρ P i = resized P (ρ P i)
resize-is-prop       {𝓀} {π“₯} ρ P i = equiv-to-prop (resizing-condition (ρ P i)) i
to-resize            {𝓀} {π“₯} ρ P i = ⌜ resizing-condition (ρ P i) ⌝⁻¹
from-resize          {𝓀} {π“₯} ρ P i = ⌜ resizing-condition (ρ P i) ⌝
to-resize-is-equiv   {𝓀} {π“₯} ρ P i = ⌜⌝⁻¹-is-equiv (resizing-condition (ρ P i))
from-resize-is-equiv {𝓀} {π“₯} ρ P i = ⌜⌝-is-equiv (resizing-condition (ρ P i))

Propositional-resizing : 𝓀ω
Propositional-resizing = {𝓀 π“₯ : Universe} β†’ propositional-resizing 𝓀 π“₯

\end{code}

Propositional resizing is consistent, because it is implied by
excluded middle, which is consistent (with or without univalence):

\begin{code}

decidable-propositions-have-any-size : (P : 𝓀  Μ‡ )
                                     β†’ is-prop P
                                     β†’ is-decidable P
                                     β†’ P is π“₯ small
decidable-propositions-have-any-size {𝓀} {π“₯} P i d = Q d , e d
 where
  Q : is-decidable P β†’ π“₯ Μ‡
  Q (inl p) = πŸ™
  Q (inr n) = 𝟘

  j : (d : is-decidable P) β†’ is-prop (Q d)
  j (inl p) = πŸ™-is-prop
  j (inr n) = 𝟘-is-prop

  f : (d : is-decidable P) β†’ P β†’ Q d
  f (inl p) p' = ⋆
  f (inr n) p  = 𝟘-elim (n p)

  g : (d : is-decidable P) β†’ Q d β†’ P
  g (inl p) q = p
  g (inr n) q = 𝟘-elim q

  e : (d : is-decidable P) β†’ Q d ≃ P
  e d = logically-equivalent-props-are-equivalent
         (j d) i (g d) (f d)

EM-gives-PR : EM 𝓀 β†’ propositional-resizing 𝓀 π“₯
EM-gives-PR em P i = decidable-propositions-have-any-size P i (em P i)

\end{code}

To show that the axiom of propositional resizing is itself a
proposition, we use univalence here (and there is a proof with weaker
hypotheses below). But notice that the type "X is π“₯ small" is a
proposition for every type X if and only if univalence holds.

\begin{code}

being-small-is-prop : Univalence
                    β†’ (X : 𝓀 Μ‡ ) (π“₯ :  Universe)
                    β†’ is-prop (X is π“₯ small)
being-small-is-prop {𝓀} ua X π“₯ = c
 where
  fe : FunExt
  fe = Univalence-gives-FunExt ua

  a : (Y : π“₯ Μ‡ ) β†’ (Y ≃ X) ≃ (Lift 𝓀 Y ＝ Lift π“₯ X)
  a Y = (Y ≃ X)                β‰ƒβŸ¨ aβ‚€ ⟩
        (Lift 𝓀 Y ≃ Lift π“₯ X)  β‰ƒβŸ¨ a₁ ⟩
        (Lift 𝓀 Y ＝ Lift π“₯ X)  β– 
   where
    aβ‚€ = ≃-cong fe
           (≃-sym (Lift-is-universe-embedding 𝓀 Y))
           (≃-sym (Lift-is-universe-embedding π“₯ X))
    a₁ = ≃-sym (univalence-≃ (ua (𝓀 βŠ” π“₯)) _ _)

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

  c : is-prop (Ξ£ Y κž‰ π“₯ Μ‡ , Y ≃ X)
  c = equiv-to-prop b (Lift-is-embedding ua (Lift π“₯ X))

propositional-resizing-is-prop : Univalence
                               β†’ is-prop (propositional-resizing 𝓀 π“₯)
propositional-resizing-is-prop {𝓀} {π“₯} ua =
 Ξ -is-prop (fe (𝓀 ⁺) (π“₯ ⁺ βŠ” 𝓀))
  (Ξ» P β†’ Ξ -is-prop (fe 𝓀 (π“₯ ⁺ βŠ” 𝓀))
  (Ξ» i β†’ being-small-is-prop ua P π“₯))
 where
  fe : FunExt
  fe = Univalence-gives-FunExt ua

\end{code}

And here is a proof that the axiom of propositional resizing is itself
a proposition using propositional and functional extensionality
instead of univalence:

\begin{code}

prop-being-small-is-prop : PropExt
                         β†’ FunExt
                         β†’ (P : 𝓀 Μ‡ )
                         β†’ is-prop P
                         β†’ {π“₯ :  Universe} β†’ is-prop (P is π“₯ small)
prop-being-small-is-prop {𝓀} pe fe P i {π“₯} = c
 where
  j : is-prop (Lift π“₯ P)
  j = equiv-to-prop (Lift-is-universe-embedding π“₯ P) i

  a : (Y : π“₯ Μ‡ ) β†’ (Y ≃ P) ≃ (Lift 𝓀 Y ＝ Lift π“₯ P)
  a Y = (Y ≃ P)                β‰ƒβŸ¨ aβ‚€ ⟩
        (Lift 𝓀 Y ≃ Lift π“₯ P)  β‰ƒβŸ¨ a₁ ⟩
        (Lift 𝓀 Y ＝ Lift π“₯ P) β– 
   where
    aβ‚€ = ≃-cong fe
           (≃-sym (Lift-is-universe-embedding 𝓀 Y))
           (≃-sym (Lift-is-universe-embedding π“₯ P))

    a₁ = ≃-sym (prop-univalent-≃
           (pe (𝓀 βŠ” π“₯))(fe (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)) (Lift 𝓀 Y) (Lift π“₯ P) j)

  b : (Ξ£ Y κž‰ π“₯ Μ‡ , Y ≃ P) ≃ (Ξ£ Y κž‰ π“₯ Μ‡ , Lift 𝓀 Y ＝ Lift π“₯ P)
  b = Ξ£-cong a

  c : is-prop (Ξ£ Y κž‰ π“₯ Μ‡ , Y ≃ P)
  c = equiv-to-prop b (prop-fiber-Lift pe fe (Lift π“₯ P) j)

propositional-resizing-is-prop' : PropExt
                                β†’ FunExt
                                β†’ is-prop (propositional-resizing 𝓀 π“₯)
propositional-resizing-is-prop' pe fe =
 Ξ β‚‚-is-prop (fe _ _) (Ξ» P i β†’ prop-being-small-is-prop pe fe P i)

\end{code}

Impredicativity. We begin with this strong notion, which says that the
type Ξ© 𝓀 of truth values in the universe 𝓀 has a copy in any successor
universe (i.e. in all universes except the first).

\begin{code}

Ω⁺-resizing : (𝓀 : Universe) β†’ 𝓀ω
Ω⁺-resizing 𝓀 = (π“₯ : Universe) β†’ (Ξ© 𝓀) is (π“₯ ⁺) small

Ω⁺-resizing-from-pr-pe-fe : Propositional-resizing
                          β†’ PropExt
                          β†’ FunExt
                          β†’ Ω⁺-resizing 𝓀
Ω⁺-resizing-from-pr-pe-fe {𝓀} ρ pe fe π“₯ = Ξ³
 where
  Ο† : Ξ© π“₯ β†’ Ξ© 𝓀
  Ο† (Q , j) = resize ρ Q j , resize-is-prop ρ Q j

  ψ : Ξ© 𝓀 β†’ Ξ© π“₯
  ψ (P , i) = resize ρ P i , resize-is-prop ρ P i

  Ο†Οˆ : (p : Ξ© 𝓀) β†’ Ο† (ψ p) ＝ p
  Ο†Οˆ (P , i) = Ξ©-extensionality (pe 𝓀) (fe 𝓀 𝓀)
               (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)

  ΟˆΟ† : (q : Ξ© π“₯) β†’ ψ (Ο† q) ＝ q
  ΟˆΟ† (Q , j) = Ξ©-extensionality (pe π“₯) (fe π“₯ π“₯)
               (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)

  Ξ³ : (Ξ© 𝓀) is (π“₯ ⁺) small
  Ξ³ = Ξ© π“₯ , qinveq Ο† (ψ , ΟˆΟ† , Ο†Οˆ)
\end{code}

A more standard notion of impredicativity is that the type Ξ© 𝓀 of
truth-values in the universe 𝓀 itself lives in 𝓀.

\begin{code}

Ξ©-resizing : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Ξ©-resizing 𝓀 = (Ξ© 𝓀) is 𝓀 small

\end{code}

Propositional resizing doesn't imply that the first universe 𝓀₀ is
impredicative, but it does imply that all other, successor, universes
𝓀 ⁺ are.

\begin{code}

Ω-resizing⁺-from-pr-pe-fe : Propositional-resizing
                          β†’ PropExt
                          β†’ FunExt
                          β†’ Ξ©-resizing (𝓀 ⁺)
Ξ©-resizing⁺-from-pr-pe-fe {𝓀} ρ pe fe = Ω⁺-resizing-from-pr-pe-fe ρ pe fe 𝓀

\end{code}

But excluded middle does give the impredicativity of the first
universe, and of all other universes, of course:

\begin{code}

Ξ©-Resizing : (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯ )⁺ Μ‡
Ξ©-Resizing 𝓀 π“₯ = (Ξ© 𝓀) is π“₯ small

Ξ©-global-resizing-from-em-pe-fe : EM 𝓀
                                β†’ propext 𝓀
                                β†’ funext 𝓀 𝓀
                                β†’ (π“₯ : Universe) β†’ Ξ©-Resizing 𝓀 π“₯
Ξ©-global-resizing-from-em-pe-fe {𝓀} lem pe fe π“₯ = Ξ³
 where
  em : LEM 𝓀
  em = EM-gives-LEM lem

  Ο† : πŸ™ + πŸ™ β†’ Ξ© 𝓀
  Ο† (inl x) = βŠ₯
  Ο† (inr y) = ⊀

  ψ : (p : Ξ© 𝓀) β†’ is-decidable (p holds) β†’ πŸ™ + πŸ™
  ψ p (inl h) = inr ⋆
  ψ p (inr n) = inl ⋆

  ΟˆΟ† : (z : πŸ™ + πŸ™) (d : is-decidable ((Ο† z) holds)) β†’ ψ (Ο† z) d ＝ z
  ΟˆΟ† (inl x) (inl h) = 𝟘-elim h
  ΟˆΟ† (inl x) (inr n) = ap inl (πŸ™-is-prop ⋆ x)
  ΟˆΟ† (inr y) (inl h) = ap inr (πŸ™-is-prop ⋆ y)
  ΟˆΟ† (inr y) (inr n) = 𝟘-elim (n ⋆)

  Ο†Οˆ : (p : Ξ© 𝓀) (d : is-decidable (p holds)) β†’ Ο† (ψ p d) ＝ p
  Ο†Οˆ p (inl h) = (true-gives-equal-⊀  pe fe (p holds) (holds-is-prop p) h)⁻¹
  Ο†Οˆ p (inr n) = (false-gives-equal-βŠ₯ pe fe (p holds) (holds-is-prop p) n)⁻¹

  Ξ³ : Ξ©-Resizing 𝓀 π“₯
  Ξ³ =  (πŸ™ {π“₯} + πŸ™ {π“₯}) ,
       qinveq Ο†
         ((Ξ» p β†’ ψ p (em p)) ,
          (Ξ» z β†’ ΟˆΟ† z (em (Ο† z))) ,
          (Ξ» p β†’ Ο†Οˆ p (em p)))

\end{code}

We also have that moving Ξ© around universes moves propositions around
universes:

\begin{code}

Ξ©-resizing-gives-propositional-resizing : Ξ©-Resizing 𝓀 π“₯
                                        β†’ propext 𝓀
                                        β†’ funext 𝓀 𝓀
                                        β†’ propositional-resizing 𝓀 π“₯
Ξ©-resizing-gives-propositional-resizing {𝓀} {π“₯} (O , e) pe fe P i = Ξ³
 where
  down : Ξ© 𝓀 β†’ O
  down = ⌜ ≃-sym e ⌝

  O-is-set : is-set O
  O-is-set = equiv-to-set e (Ξ©-is-set fe pe)

  Q : π“₯ Μ‡
  Q = down ⊀ ＝ down (P , i)

  j : is-prop Q
  j = O-is-set

  Ο† : Q β†’ P
  Ο† q = idtofun πŸ™ P (ap pr₁ (equivs-are-lc down (⌜⌝-is-equiv (≃-sym e)) q)) ⋆

  ψ : P β†’ Q
  ψ p = ap down (to-Ξ£-＝ (pe πŸ™-is-prop i (Ξ» _ β†’ p) (Ξ» _ β†’ ⋆) ,
                         being-prop-is-prop fe _ _))

  Ξ΅ : Q ≃ P
  Ξ΅ = logically-equivalent-props-are-equivalent j i Ο† ψ

  Ξ³ : Ξ£ Q κž‰ π“₯ Μ‡ , Q ≃ P
  Ξ³ = Q , Ξ΅

Ξ©-resizingβ‚€ : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Ξ©-resizingβ‚€ 𝓀 = (Ξ© 𝓀) is 𝓀₀ small

Ξ©-resizingβ‚€-from-em-pe-feβ‚€ : EM 𝓀
                           β†’ propext 𝓀
                           β†’ funext 𝓀 𝓀
                           β†’ Ξ©-resizingβ‚€ 𝓀
Ξ©-resizingβ‚€-from-em-pe-feβ‚€ {𝓀} em pe fe =
 Ξ©-global-resizing-from-em-pe-fe em pe fe 𝓀₀

\end{code}

What we get with propositional resizing is that all types of
propositions of any universe 𝓀 are equivalent to Ξ© 𝓀₀, which lives in
the second universe 𝓀₁:

\begin{code}

Ξ©-resizing₁ : (𝓀 : Universe) β†’ 𝓀 ⁺ βŠ” 𝓀₂ Μ‡
Ξ©-resizing₁ 𝓀 = (Ξ© 𝓀) is 𝓀₁ small

Ξ©-resizing₁-from-pr-pe-fe : Propositional-resizing
                          β†’ PropExt
                          β†’ FunExt
                          β†’ Ξ©-resizing₁ 𝓀
Ξ©-resizing₁-from-pr-pe-fe {𝓀} ρ pe fe = Ω⁺-resizing-from-pr-pe-fe ρ pe fe 𝓀₀

Ξ©-resizing₁-≃-from-pr-pe-fe : Propositional-resizing
                            β†’ PropExt
                            β†’ FunExt
                            β†’ Ξ© 𝓀 ≃ Ξ© 𝓀₀
Ξ©-resizing₁-≃-from-pr-pe-fe {𝓀} ρ pe fe =
  ≃-sym (resizing-condition (Ξ©-resizing₁-from-pr-pe-fe {𝓀} ρ pe fe))

private
 Ξ©-𝓀₀-lives-in-𝓀₁ : 𝓀₁ Μ‡
 Ξ©-𝓀₀-lives-in-𝓀₁ = Ξ© 𝓀₀

\end{code}

With propositional resizing, we have that any universe is a retract of
any larger universe (this seems to be a new result).

\begin{code}

Lift-is-section : Univalence
                β†’ Propositional-resizing
                β†’ (𝓀 π“₯ : Universe)
                β†’ is-section (Lift {𝓀} π“₯)
Lift-is-section ua R 𝓀 π“₯ = (r , rs)
 where
  s : 𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
  s = Lift π“₯

  e : is-embedding s
  e = Lift-is-embedding ua

  F : 𝓀 βŠ” π“₯ Μ‡ β†’ 𝓀 Μ‡
  F Y = resize R (fiber s Y) (e Y)

  f : (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ F Y β†’ fiber s Y
  f Y = from-resize R (fiber s Y) (e Y)

  r : 𝓀 βŠ” π“₯ Μ‡ β†’ 𝓀 Μ‡
  r Y = (p : F Y) β†’ fiber-point (f Y p)

  rs : (X : 𝓀 Μ‡ ) β†’ r (s X) ＝ X
  rs X = Ξ³
   where
    g : (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ fiber s Y β†’ F Y
    g Y = to-resize R (fiber s Y) (e Y)

    u : F (s X)
    u = g (s X) (X , refl)

    v : fiber s (s X)
    v = f (s X) u

    i : (Y : 𝓀 βŠ” π“₯ Μ‡ ) β†’ is-prop (F Y)
    i Y = resize-is-prop R (fiber s Y) (e Y)

    X' : 𝓀 Μ‡
    X' = fiber-point v

    a : r (s X) ≃ X'
    a = prop-indexed-product (Univalence-gives-FunExt ua 𝓀 𝓀) (i (s X)) u

    b : s X' ＝ s X
    b = fiber-identification v

    c : X' ＝ X
    c = embeddings-are-lc s e b

    d : r (s X) ≃ X
    d = transport (Ξ» - β†’ r (s X) ≃ -) c a

    γ : r (s X) ＝ X
    Ξ³ = eqtoid (ua 𝓀) (r (s X)) X d

\end{code}

We remark that for types that are not sets, sections are not
automatically embeddings (Shulman 2015, Logical Methods in Computer
Science, April 27, 2017, Volume 12, Issue 3,
https://lmcs.episciences.org/2027 , Theorem 3.10).

Hence it is worth stating this explicitly:

\begin{code}

universe-retract' : Univalence
                  β†’ Propositional-resizing
                  β†’ (𝓀 π“₯ : Universe)
                  β†’ Ξ£ (r , s , Ξ·) κž‰ retract 𝓀 Μ‡ of (𝓀 βŠ” π“₯ Μ‡ ), is-embedding s
universe-retract' ua R 𝓀 π“₯ = (pr₁ a , Lift π“₯ , prβ‚‚ a) , Lift-is-embedding ua
 where
  a : Ξ£ lower κž‰ (𝓀 βŠ” π“₯ Μ‡ β†’ 𝓀 Μ‡ ) , lower ∘ Lift π“₯ ∼ id
  a = Lift-is-section ua R 𝓀 π“₯

\end{code}

A more conceptual version of the above construction is in the module
InjectiveTypes (which was discovered first - this is just an unfolding
of that construction).

TODO. If we assume that we have such a retraction, does weak
propositional resizing follow?

The following construction is due to Voevodsky, but we use the
resizing axiom rather than his rules (and we work with non-cumulative
universes).

\begin{code}

module _ {𝓀 : Universe} where

 βˆ₯_βˆ₯⁺ : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
 βˆ₯ X βˆ₯⁺ = (P :  𝓀 Μ‡ ) β†’ is-prop P β†’ (X β†’ P) β†’ P

 βˆ₯βˆ₯⁺-is-prop : FunExt β†’ {X : 𝓀 Μ‡ } β†’ is-prop (βˆ₯ X βˆ₯⁺)
 βˆ₯βˆ₯⁺-is-prop fe = Ξ -is-prop (fe _ _)
                    (Ξ» P β†’ Ξ -is-prop (fe _ _)
                            (Ξ» i β†’ Ξ -is-prop (fe _ _)
                                     (Ξ» u β†’ i)))

 ∣_∣⁺ : {X : 𝓀 Μ‡ } β†’ X β†’ βˆ₯ X βˆ₯⁺
 ∣ x ∣⁺ = Ξ» P i u β†’ u x

 βˆ₯βˆ₯⁺-rec : {X P : 𝓀 Μ‡ } β†’ is-prop P β†’ (X β†’ P) β†’ βˆ₯ X βˆ₯⁺ β†’ P
 βˆ₯βˆ₯⁺-rec {X} {P} i u s = s P i u

resizing-truncation : FunExt
                    β†’ Propositional-resizing
                    β†’ propositional-truncations-exist
resizing-truncation fe R = record {
    βˆ₯_βˆ₯          = Ξ» {𝓀} X β†’ resize R βˆ₯ X βˆ₯⁺ (βˆ₯βˆ₯⁺-is-prop fe)
  ; βˆ₯βˆ₯-is-prop   = Ξ» {𝓀} {X} β†’ resize-is-prop R βˆ₯ X βˆ₯⁺ (βˆ₯βˆ₯⁺-is-prop fe)
  ; ∣_∣          = Ξ» {𝓀} {X} x β†’ to-resize R βˆ₯ X βˆ₯⁺ (βˆ₯βˆ₯⁺-is-prop fe) ∣ x ∣⁺
  ; βˆ₯βˆ₯-rec       = Ξ» {𝓀} {π“₯} {X} {P} i u s β†’ from-resize R P i
                                              (βˆ₯βˆ₯⁺-rec (resize-is-prop R P i)
                                                       (to-resize R P i ∘ u)
                                                       (from-resize R βˆ₯ X βˆ₯⁺
                                                         (βˆ₯βˆ₯⁺-is-prop fe) s))
  }

\end{code}

Images:

\begin{code}

module Image
        {𝓀 π“₯ : Universe}
        {X : 𝓀 Μ‡ }
        {Y : π“₯ Μ‡ }
        (fe : FunExt)
        (R : Propositional-resizing)
       where

 open PropositionalTruncation (resizing-truncation fe R)

 image : (X β†’ Y) β†’ π“₯ Μ‡
 image f = Ξ£ y κž‰ Y , resize (R {𝓀 βŠ” π“₯} {π“₯}) (βˆƒ x κž‰ X , f x ＝ y) βˆ₯βˆ₯-is-prop

 restriction : (f : X β†’ Y) β†’ image f β†’ Y
 restriction f (y , _) = y

 restriction-embedding : (f : X β†’ Y) β†’ is-embedding (restriction f)
 restriction-embedding f = pr₁-is-embedding (Ξ» y β†’ resize-is-prop R _ _)

 corestriction : (f : X β†’ Y) β†’ X β†’ image f
 corestriction f x = f x , to-resize R _ _ ∣ x , refl ∣

\end{code}

TODO. Prove the properties / perform the constructions in
UF.ImageAndSurjection. Better: reorganize the code so that reproving
is not necessary.

Added 24 January 2020 (originally proved 19 November 2019) by Tom de Jong.

It turns out that a proposition Y has size π“₯ precisely if
(Y is π“₯ small) is π“₯ small.

Hence, if you can resize the propositions of the form (Y is π“₯ small)
(with Y in 𝓀), then you can resize all propositions in 𝓀 (to π“₯).

\begin{code}

being-small-is-idempotent : (ua : Univalence) (𝓀 π“₯ : Universe) (Y : 𝓀 Μ‡ )
                          β†’ is-prop Y
                          β†’ (Y is π“₯ small) is π“₯ small
                          β†’ Y is π“₯ small
being-small-is-idempotent ua 𝓀 π“₯ Y i (H , e) = X , Ξ³
 where
  X : π“₯ Μ‡
  X = Ξ£ h κž‰ H , resized Y (eqtofun e h)

  Ξ³ = X  β‰ƒβŸ¨ Ξ£-change-of-variable (resized Y) (eqtofun e) (eqtofun- e) ⟩
      X' β‰ƒβŸ¨ Ο• ⟩
      Y  β– 
   where
    X' : π“₯ ⁺ βŠ” 𝓀 Μ‡
    X' = Ξ£ h κž‰ Y is π“₯ small , resized Y h

    Ο• = logically-equivalent-props-are-equivalent j i f g
     where
      j : is-prop X'
      j = Ξ£-is-prop (being-small-is-prop ua Y π“₯)
            (Ξ» (h : Y is π“₯ small) β†’ equiv-to-prop (resizing-condition h) i)

      f : X' β†’ Y
      f (e' , x) = eqtofun (resizing-condition e') x

      g : Y β†’ X'
      g y = (πŸ™{π“₯} , singleton-≃-πŸ™' (pointed-props-are-singletons y i)) , ⋆

deJong-resizing : (𝓀 π“₯ : Universe) β†’ 𝓀 ⁺ βŠ” π“₯ ⁺ Μ‡
deJong-resizing 𝓀 π“₯ = (Y : 𝓀 Μ‡ ) β†’ (Y is π“₯ small) is π“₯ small

deJong-resizing-implies-propositional-resizing : (ua : Univalence)
                                                 (𝓀 π“₯ : Universe)
                                               β†’ deJong-resizing 𝓀 π“₯
                                               β†’ propositional-resizing 𝓀 π“₯
deJong-resizing-implies-propositional-resizing ua 𝓀 π“₯ r P i =
 being-small-is-idempotent ua 𝓀 π“₯ P i (r P)

being-small-is-idempotent-converse
 : (ua : Univalence) (𝓀 π“₯ : Universe) (Y : 𝓀 Μ‡ )
 β†’ Y is π“₯ small
 β†’ (Y is π“₯ small) is π“₯ small
being-small-is-idempotent-converse ua 𝓀 π“₯ Y r = πŸ™{π“₯} , Ξ³
 where
  Ξ³ : πŸ™{π“₯} ≃ (Y is π“₯ small)
  Ξ³ = singleton-≃-πŸ™'
       (pointed-props-are-singletons r (being-small-is-prop ua Y π“₯))

being-small-is-idempotent-≃ : (ua : Univalence) (𝓀 π“₯ : Universe) (Y : 𝓀 Μ‡ )
                            β†’ is-prop Y
                            β†’ ((Y is π“₯ small) is π“₯ small) ≃ (Y is π“₯ small)
being-small-is-idempotent-≃ ua 𝓀 π“₯ Y i =
 logically-equivalent-props-are-equivalent
  (being-small-is-prop ua (Y is π“₯ small) π“₯)
  (being-small-is-prop ua Y π“₯)
  (being-small-is-idempotent ua 𝓀 π“₯ Y i)
  (being-small-is-idempotent-converse ua 𝓀 π“₯ Y)

being-small-is-idempotent-＝ : (ua : Univalence) (𝓀 π“₯ : Universe) (Y : 𝓀 Μ‡ )
                            β†’ is-prop Y
                            β†’ ((Y is π“₯ small) is π“₯ small) ＝ (Y is π“₯ small)
being-small-is-idempotent-＝ ua 𝓀 π“₯ Y i =
 eqtoid (ua (𝓀 βŠ” π“₯ ⁺))
  ((Y is π“₯ small) is π“₯ small)
  (Y is π“₯ small)
  (being-small-is-idempotent-≃ ua 𝓀 π“₯ Y i)

\end{code}

Added 26th January 2021. The following is based on joint work of Tom
de Jong with Martin Escardo.

TODO. Maybe "is-small" should be "is-essentially-small" and "is-large"
should also be renamed, for conformance with the (category-theoretic)
literature.

\begin{code}

is-small : 𝓀 ⁺ Μ‡ β†’ 𝓀 ⁺ Μ‡
is-small {𝓀} X = X is 𝓀 small

is-large : 𝓀 ⁺ Μ‡ β†’ 𝓀 ⁺ Μ‡
is-large X = Β¬ is-small X

universes-are-large : is-large (𝓀 Μ‡ )
universes-are-large = II
 where
  open import Various.LawvereFPT

  I : Β¬ (Ξ£ X κž‰ 𝓀 Μ‡ , 𝓀 Μ‡ ≃ X)
  I = generalized-Coquand.Theorem

  II : Β¬ (Ξ£ X κž‰ 𝓀 Μ‡ , X ≃ 𝓀 Μ‡ )
  II = contrapositive (Ξ» (X , 𝕗) β†’ (X , ≃-sym 𝕗)) I

_is_small-map : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
              β†’ (X β†’ Y)
              β†’ (𝓦 : Universe)
              β†’ 𝓀 βŠ” π“₯ βŠ” (𝓦 ⁺) Μ‡
f is 𝓦 small-map = βˆ€ y β†’ fiber f y is 𝓦 small

_is-small-map : {X Y : 𝓀 ⁺ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 ⁺ Μ‡
_is-small-map {𝓀} f = f is 𝓀 small-map

native-size-of-map : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                   β†’ f is 𝓀 βŠ” π“₯ small-map
native-size-of-map f y = native-size (fiber f y)

\end{code}

Obsolete notation used in some publications:

\begin{code}

private
 _Has-size_ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ (𝓦 : Universe) β†’ 𝓀 βŠ” π“₯ βŠ” (𝓦 ⁺) Μ‡
 f Has-size 𝓦 = f is 𝓦 small-map

\end{code}

The above should not be used anymore, but should be kept here.

\begin{code}

pr₁-is-small-map : {X : 𝓀 Μ‡} {Y : X β†’ π“₯ Μ‡}
                 β†’ (Ξ» (Οƒ : Ξ£ Y) β†’ pr₁ Οƒ) is π“₯ small-map
pr₁-is-small-map {𝓀} {π“₯} {X} {Y} x = Y x , ≃-sym (pr₁-fiber-equiv x)

𝟚-to-Ξ©-is-small-map : funext 𝓀 𝓀
                    β†’ propext 𝓀
                    β†’ (𝟚-to-Ξ© {𝓀}) is 𝓀 small-map
𝟚-to-Ω-is-small-map fe pe p = (¬ (p holds) + p holds) ,
                              ≃-sym (𝟚-to-Ξ©-fiber fe pe p)

size-contravariance : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                    β†’ f is 𝓦 small-map
                    β†’ Y is 𝓦 small
                    β†’ X is 𝓦 small
size-contravariance {𝓀} {π“₯} {𝓦} {X} {Y} f f-size (Y' , π•˜) = Ξ³
 where
  F : Y β†’ 𝓦 Μ‡
  F y = resized (fiber f y) (f-size y)

  F-is-fiber : (y : Y) β†’ F y ≃ fiber f y
  F-is-fiber y = resizing-condition (f-size y)

  X' : 𝓦 Μ‡
  X' = Ξ£ y' κž‰ Y' , F (⌜ π•˜ ⌝ y')

  e = X'                    β‰ƒβŸ¨ Ξ£-change-of-variable F ⌜ π•˜ ⌝ (⌜⌝-is-equiv π•˜) ⟩
      (Ξ£ y κž‰ Y , F y)       β‰ƒβŸ¨ Ξ£-cong F-is-fiber ⟩
      (Ξ£ y κž‰ Y , fiber f y) β‰ƒβŸ¨ total-fiber-is-domain f ⟩
      X                     β– 

  Ξ³ : X is 𝓦 small
  Ξ³ = X' , e

size-covariance : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                β†’ f is 𝓦 small-map
                β†’ Β¬ (X is 𝓦 small)
                β†’ Β¬ (Y is 𝓦 small)
size-covariance f Ο• = contrapositive (size-contravariance f Ο•)

small-contravariance : {X Y : 𝓀 ⁺ Μ‡ } (f : X β†’ Y)
                     β†’ f is-small-map
                     β†’ is-small Y
                     β†’ is-small X
small-contravariance = size-contravariance

large-covariance : {X Y : 𝓀 ⁺ Μ‡ } (f : X β†’ Y)
                 β†’ f is-small-map
                 β†’ is-large X
                 β†’ is-large Y
large-covariance = size-covariance

size-of-section-embedding : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (s : X β†’ Y)
                          β†’ is-section s
                          β†’ is-embedding s
                          β†’ s is π“₯ small-map
size-of-section-embedding {𝓀} {π“₯} {X} {Y} s (r , Ξ·) e y = Ξ³
 where
  c : (x : Y) β†’ collapsible (s (r x) ＝ x)
  c = section-embedding-gives-collapsible r s Ξ· e

  ΞΊ : s (r y) ＝ y β†’ s (r y) ＝ y
  ΞΊ = pr₁ (c y)

  ΞΊ-constant : (p p' : s (r y) ＝ y) β†’ ΞΊ p ＝ ΞΊ p'
  ΞΊ-constant = prβ‚‚ (c y)

  B : π“₯ Μ‡
  B = fix ΞΊ

  B-is-prop : is-prop B
  B-is-prop = fix-is-prop ΞΊ ΞΊ-constant

  Ξ± : B β†’ fiber s y
  Ξ± = (Ξ» p β†’ r y , p) ∘ from-fix ΞΊ

  Ξ² : fiber s y β†’ B
  Ξ² = to-fix ΞΊ ΞΊ-constant ∘ Ξ» (x , p) β†’ s (r y)     ＝⟨ ap (s ∘ r) (p ⁻¹) ⟩
                                        s (r (s x)) ＝⟨ ap s (η x) ⟩
                                        s x         ＝⟨ p ⟩
                                        y           ∎

  Ξ΄ : B ≃ fiber s y
  Ξ΄ = logically-equivalent-props-are-equivalent B-is-prop (e y) Ξ± Ξ²

  Ξ³ : (fiber s y) is π“₯ small
  Ξ³ = B , Ξ΄

section-embedding-size-contravariance : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (s : X β†’ Y)
                                      β†’ is-embedding s
                                      β†’ is-section s
                                      β†’ Y is 𝓦 small
                                      β†’ X is 𝓦 small
section-embedding-size-contravariance
 {𝓀} {π“₯} {𝓦} {X} {Y} s e (g , Ξ·) (Y' , h , i) = Ξ³
 where
  h⁻¹ : Y β†’ Y'
  h⁻¹ = inverse h i

  s' : X β†’ Y'
  s' = h⁻¹ ∘ s

  Ξ·' = Ξ» x β†’ g (h (h⁻¹ (s x))) ＝⟨ ap g (inverses-are-sections h i (s x)) ⟩
             g (s x)           ＝⟨ η x ⟩
             x                 ∎

  Ξ΄ : s' is 𝓦 small-map
  δ = size-of-section-embedding s' (g ∘ h , η')
       (∘-is-embedding e (equivs-are-embeddings h⁻¹
                         (inverses-are-equivs h i)))

  Ξ³ : X is 𝓦 small
  Ξ³ = size-contravariance s' Ξ΄ (Y' , ≃-refl Y')

embedded-retract-is-small : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                            (ρ : retract X of Y)
                          β†’ is-embedding (section ρ)
                          β†’ Y is 𝓦 small
                          β†’ X is 𝓦 small
embedded-retract-is-small (r , s , rs) s-is-embedding Y-is-small =
 section-embedding-size-contravariance s s-is-embedding (r , rs) Y-is-small

≃-size-contravariance : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                      β†’ X ≃ Y
                      β†’ Y is 𝓦 small
                      β†’ X is 𝓦 small
≃-size-contravariance {𝓀} {π“₯} {𝓦} {X} {Y} e (Z , d) = Z , ≃-comp d (≃-sym e)

singletons-have-any-size : {X : 𝓀 Μ‡ }
                         β†’ is-singleton X
                         β†’ X is π“₯ small
singletons-have-any-size i = πŸ™ , singleton-≃-πŸ™' i

equivs-have-any-size : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                     β†’ is-equiv f
                     β†’ f is 𝓦 small-map
equivs-have-any-size {𝓀} {π“₯} {𝓦} {X} {Y} f e y =
 singletons-have-any-size (equivs-are-vv-equivs f e y)

equivs-have-any-size' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (𝕗 : X ≃ Y)
                     β†’ ⌜ 𝕗 ⌝ is 𝓦 small-map
equivs-have-any-size' (f , e) = equivs-have-any-size f e

\end{code}

The following notion of local smallness is due to Egbert Rijke, in his
join-construction paper https://arxiv.org/abs/1701.07538.

\begin{code}

is-locally-small : 𝓀 ⁺ Μ‡ β†’ 𝓀 ⁺ Μ‡
is-locally-small X = (x y : X) β†’ is-small (x ＝ y)

\end{code}

For example, by univalence, universes are locally small, and so is the
(large) type of ordinals in a universe.

\begin{code}

universes-are-locally-small : is-univalent 𝓀 β†’ is-locally-small (𝓀 Μ‡ )
universes-are-locally-small ua X Y = (X ≃ Y) , ≃-sym (univalence-≃ ua X Y)

\end{code}

General machinery for dealing with local smallness:

\begin{code}

_＝⟦_⟧_ : {X : 𝓀 ⁺ Μ‡ } β†’ X β†’ is-locally-small X β†’ X β†’ 𝓀 Μ‡
x ＝⟦ ls ⟧ y = resized (x ＝ y) (ls x y)

Id⟦_⟧ : {X : 𝓀 ⁺ Μ‡ } β†’ is-locally-small X β†’ X β†’ X β†’ 𝓀 Μ‡
Id⟦ ls ⟧ x y = x ＝⟦ ls ⟧ y

＝⟦_⟧-gives-＝ : {X : 𝓀 ⁺ Μ‡ } (ls : is-locally-small X) {x y : X}
               β†’ x ＝⟦ ls ⟧ y β†’ x ＝ y
＝⟦ ls ⟧-gives-＝ {x} {y} = ⌜ resizing-condition (ls x y) ⌝

＝-gives-＝⟦_⟧ : {X : 𝓀 ⁺ Μ‡ } (ls : is-locally-small X) {x y : X}
               β†’ x ＝ y β†’ x ＝⟦ ls ⟧ y
＝-gives-＝⟦ ls ⟧ {x} {y} = ⌜ resizing-condition (ls x y) ⌝⁻¹

＝⟦_⟧-refl : {X : 𝓀 ⁺ Μ‡ } (ls : is-locally-small X) {x : X} β†’ x ＝⟦ ls ⟧ x
＝⟦ ls ⟧-refl {x} = ⌜ ≃-sym (resizing-condition (ls x x)) ⌝ refl

＝⟦_⟧-sym : {X : 𝓀 ⁺ Μ‡ } (ls : is-locally-small X) {x y : X}
          β†’ x ＝⟦ ls ⟧ y
          β†’ y ＝⟦ ls ⟧ x
＝⟦ ls ⟧-sym p = ＝-gives-＝⟦ ls ⟧ (＝⟦ ls ⟧-gives-＝ p ⁻¹)

_β‰ βŸ¦_⟧_ : {X : 𝓀 ⁺ Μ‡ } β†’ X β†’ is-locally-small X β†’ X β†’ 𝓀 Μ‡
x β‰ βŸ¦ ls ⟧ y = Β¬ (x ＝⟦ ls ⟧ y)

β‰ βŸ¦_⟧-irrefl : {X : 𝓀 ⁺ Μ‡ } (ls : is-locally-small X) {x : X} β†’ Β¬ (x β‰ βŸ¦ ls ⟧ x)
β‰ βŸ¦ ls ⟧-irrefl {x} Ξ½ = Ξ½ ＝⟦ ls ⟧-refl

β‰ βŸ¦_⟧-sym : {X : 𝓀 ⁺ Μ‡ } (ls : is-locally-small X) {x y : X}
         β†’ x β‰ βŸ¦ ls ⟧ y
         β†’ y β‰ βŸ¦ ls ⟧ x
β‰ βŸ¦ ls ⟧-sym {x} {y} n = Ξ» (p : y ＝⟦ ls ⟧ x) β†’ n (＝⟦ ls ⟧-sym p)

β‰ -gives-β‰ βŸ¦_⟧ : {X : 𝓀 ⁺ Μ‡ } (ls : is-locally-small X) {x y : X}
             β†’ x β‰  y
             β†’ x β‰ βŸ¦ ls ⟧ y
β‰ -gives-β‰ βŸ¦ ls ⟧ = contrapositive ＝⟦ ls ⟧-gives-＝

β‰ βŸ¦_⟧-gives-β‰  : {X : 𝓀 ⁺ Μ‡ } (ls : is-locally-small X) {x y : X}
             β†’ x β‰ βŸ¦ ls ⟧ y β†’ x β‰  y
β‰ βŸ¦ ls ⟧-gives-β‰  = contrapositive ＝-gives-＝⟦ ls ⟧

\end{code}

Added 11 Jul 2023 by Martin Escardo.

\begin{code}

subtype-is-small : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                 β†’ ((x : X) β†’ is-prop (A x))
                 β†’ X is 𝓦 small
                 β†’ Ξ£ A is π“₯ βŠ” 𝓦 small
subtype-is-small {𝓀} {π“₯} {𝓦} {X} {A} A-is-prop-valued (X' , 𝕗) = S , π•˜
 where
  S : π“₯ βŠ” 𝓦 Μ‡
  S = Ξ£ x' κž‰ X' , A (⌜ 𝕗 ⌝ x')

  π•˜ = (Ξ£ x' κž‰ X' , A (⌜ 𝕗 ⌝ x')) β‰ƒβŸ¨ Ξ£-change-of-variable-≃ A 𝕗 ⟩
      (Ξ£ x κž‰ X , A x)            β– 

subtype-is-locally-small : {X : 𝓀 ⁺ Μ‡ } {A : X β†’ 𝓀 ⁺ Μ‡ }
                         β†’ ((x : X) β†’ is-prop (A x))
                         β†’ is-locally-small X
                         β†’ is-locally-small (Ξ£ A)
subtype-is-locally-small A-is-prop-valued X-is-ls (x , a) (y , b) = Ξ³
 where
  γ : is-small ((x , a) ＝ (y , b))
  γ = x ＝⟦ X-is-ls ⟧ y ,
     (x ＝⟦ X-is-ls ⟧ y     β‰ƒβŸ¨ resizing-condition (X-is-ls x y) ⟩
     (x ＝ y)               β‰ƒβŸ¨ I ⟩
     ((x , a) ＝ (y , b))   β– )
    where
     I = ≃-sym (ap pr₁ ,
                embedding-gives-embedding'
                 pr₁
                 (pr₁-is-embedding A-is-prop-valued)
                 (x , a)
                 (y , b))

subtype-is-locally-small⁻ : {X : 𝓀 ⁺ Μ‡ } {A : X β†’ 𝓀 Μ‡ }
                          β†’ ((x : X) β†’ is-prop (A x))
                          β†’ is-locally-small X
                          β†’ is-locally-small (Ξ£ A)
subtype-is-locally-small⁻ A-is-prop-valued X-is-ls (x , a) (y , b) = γ
 where
  γ : is-small ((x , a) ＝ (y , b))
  γ = x ＝⟦ X-is-ls ⟧ y ,
     (x ＝⟦ X-is-ls ⟧ y     β‰ƒβŸ¨ resizing-condition (X-is-ls x y) ⟩
     (x ＝ y)               β‰ƒβŸ¨ I ⟩
     ((x , a) ＝ (y , b))   β– )
    where
     I = ≃-sym (ap pr₁ ,
                embedding-gives-embedding'
                 pr₁
                 (pr₁-is-embedding A-is-prop-valued)
                 (x , a)
                 (y , b))

\end{code}

TODO. Generalize the above to resize (the values of) A as well.

TODO. Add a characterization of equality of subtypes somewhere (the
proof is "I" above. Perhaps in UF.EquivalenceExamples.)

Added 5 April 2022 by Tom de Jong, after discussion with MartΓ­n.
(Refactoring an earlier addition dated 15 March 2022.)

Set Replacement is what we call the following principle:
given X : 𝓀 and Y a locally π“₯-small *set*, the image of a map f : X β†’ Y is
(𝓀 βŠ” π“₯)-small.

In particular, if 𝓀 and π“₯ are the same, then the image is 𝓀-small.

The name "Set Replacement" is inspired by [Section 2.19, Bezem+2022], but is
different in two ways:
(1) In [Bezem+2022] replacement is not restriced to maps into sets, hence our
    name *Set* Replacement
(2) In [Bezem+2022] the universe parameters 𝓀 and π“₯ are taken to be the same.

[Rijke2017] shows that the replacement of [Bezem+2022] is provable in the
presence of a univalent universes 𝓀 closed under pushouts.

In Quotient.Type.lagda, we prove that Set Replacement is provable if we assume
that for every X : 𝓀 and π“₯-valued equivalence relation β‰ˆ, the set quotient X / β‰ˆ
exists in 𝓀 βŠ” π“₯.

In Quotient.Type.lagda we prove the converse using a specific construction of
quotients, similar to [Corollary 5.1, Rijke2017].

Thus, Set Replacement is equivalent to having set quotients in 𝓀 βŠ” π“₯ for every
type in 𝓀 with a π“₯-valued equivalence relation (which is what you would have
when adding set quotients as higher inductive types).

[Rijke2017]  Egbert Rijke. The join construction.
             https://arxiv.org/abs/1701.07538, January 2017.

[Bezem+2022] Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjβ€ŒΓΈrn Ian Dundas and
             Daniel R. Grayson
             Symmetry
             https://unimath.github.io/SymmetryBook/book.pdf
             https://github.com/UniMath/SymmetryBook
             Book version: 2722568 (2022-03-31)

\begin{code}

_is-locally_small : 𝓀 Μ‡ β†’ (π“₯ : Universe) β†’ π“₯ ⁺ βŠ” 𝓀 Μ‡
X is-locally π“₯ small = (x y : X) β†’ (x ＝ y) is π“₯ small

module _ (pt : propositional-truncations-exist) where

 open import UF.ImageAndSurjection pt

 Set-Replacement : 𝓀ω
 Set-Replacement = {𝓦 𝓣 𝓀 π“₯ : Universe} {X : 𝓣 Μ‡ } {Y : 𝓦 Μ‡ } (f : X β†’ Y)
                 β†’ X is 𝓀 small
                 β†’ Y is-locally π“₯ small
                 β†’ is-set Y
                 β†’ image f is (𝓀 βŠ” π“₯) small
\end{code}

Added by Ian Ray 11th September 2024

If X is π“₯-small then it is locally π“₯-small.

\begin{code}

small-implies-locally-small : (X : 𝓀 Μ‡) β†’ (π“₯ : Universe)
                            β†’ X is π“₯ small
                            β†’ X is-locally π“₯ small
small-implies-locally-small X π“₯ (Y , e) x x' =
 ((⌜ e ⌝⁻¹ x ＝ ⌜ e ⌝⁻¹ x') , path-resized)
 where
  path-resized : (⌜ e ⌝⁻¹ x ＝ ⌜ e ⌝⁻¹ x') ≃ (x ＝ x')
  path-resized = ≃-sym (ap ⌜ e ⌝⁻¹ , ap-is-equiv ⌜ e ⌝⁻¹ (⌜⌝⁻¹-is-equiv e))

\end{code}

Added by Martin Escardo and Tom de Jong 29th August 2024.

\begin{code}

WEM-gives-that-negated-types-are-small
 : funext 𝓀 𝓀₀
 β†’ WEM 𝓀
 β†’ (X : 𝓀 Μ‡ ) β†’ (Β¬ X) is π“₯ small
WEM-gives-that-negated-types-are-small {𝓀} {π“₯} fe wem X =
 Cases (wem (Β¬ X)) f g
 where
  f : ¬¬ X β†’ (Β¬ X) is π“₯ small
  f h = 𝟘 , ≃-sym (empty-≃-𝟘 h)

  g : ¬¬¬ X β†’ (Β¬ X) is π“₯ small
  g h = πŸ™ ,
        singleton-≃-πŸ™'
         (pointed-props-are-singletons
           (three-negations-imply-one h)
           (negations-are-props fe))

\end{code}