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.Embeddings open import UF.Equiv open import UF.Equiv-FunExt open import UF.EquivalenceExamples open import UF.ClassicalLogic open import UF.FunExt open import UF.Hedberg open import UF.KrausLemma open import UF.ExitPropTrunc 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.SubtypeClassifier open import UF.SubtypeClassifier-Properties open import UF.Subsingletons open import UF.Subsingletons-FunExt 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). Question. 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. \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} π-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}