From 5dd3d65f51334717eeb556c0746a727b652bca15 Mon Sep 17 00:00:00 2001
From: Ayberk Tosun <ayberk.tosun@gmail.com>
Date: Tue, 21 May 2024 19:07:39 +0100
Subject: [PATCH] =?UTF-8?q?Write=20down=20the=20fact=20that=20=CE=A3-resiz?=
 =?UTF-8?q?ing=20gives=20that=20=F0=9D=93=A4=E2=82=80=20is=20=F0=9D=93=A4?=
 =?UTF-8?q?=E2=82=80-small?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 source/UF/SystemFNotionOfResizing.lagda | 26 ++++++++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/source/UF/SystemFNotionOfResizing.lagda b/source/UF/SystemFNotionOfResizing.lagda
index 9419cc850..d20c49633 100644
--- a/source/UF/SystemFNotionOfResizing.lagda
+++ b/source/UF/SystemFNotionOfResizing.lagda
@@ -23,6 +23,7 @@ module UF.SystemFNotionOfResizing
 open import InjectiveTypes.Resizing
 open import MLTT.Spartan
 open import UF.Equiv
+open import UF.EquivalenceExamples
 open import UF.Logic
 open import UF.NotNotStablePropositions
 open import UF.Retracts
@@ -296,13 +297,36 @@ It follows easily from this then `Ω¬¬ 𝓤₀` is equivalent to `Ω¬¬ 𝓤
 
 \end{code}
 
-One could also consider Σ-resizing, but we do not know if it is consistent or not.
+One might be tempted to consider Σ-resizing, but this immediately gives that 𝓤₀
+is 𝓤₀-small (thanks to Jon Sterling who pointed this out in a code review).
 
 \begin{code}
 
 Σ-Resizing : 𝓤₂  ̇
 Σ-Resizing = (A : 𝓤₁  ̇) → (B : A → 𝓤₀  ̇) → (Σ x ꞉ A , B x) is 𝓤₀ small
 
+Σ-resizing-gives-𝓤₀-is-𝓤₀-small : Σ-Resizing → (𝓤₀  ̇) is 𝓤₀ small
+Σ-resizing-gives-𝓤₀-is-𝓤₀-small ψ = resized ((𝓤₀  ̇) × 𝟙 {𝓤₀}) † , e
+ where
+  † : ((𝓤₀  ̇) × 𝟙 {𝓤₀}) is 𝓤₀ small
+  † = ψ (𝓤₀  ̇) (λ _ → 𝟙 {𝓤₀})
+
+  Ⅰ : resized ((𝓤₀  ̇) × 𝟙 {𝓤₀}) † ≃ (𝓤₀  ̇) × 𝟙 {𝓤₀}
+  Ⅰ = resizing-condition †
+
+  s : resized ((𝓤₀  ̇) × 𝟙 {𝓤₀}) † → 𝓤₀  ̇
+  s = pr₁ ∘ ⌜ Ⅰ ⌝
+
+  r : 𝓤₀  ̇ → resized ((𝓤₀  ̇) × 𝟙 {𝓤₀}) †
+  r A = ⌜ ≃-sym Ⅰ ⌝ (A , ⋆)
+
+  e : resized ((𝓤₀  ̇) × 𝟙 {𝓤₀}) † ≃ 𝓤₀  ̇
+  e = resized ((𝓤₀  ̇) × 𝟙 {𝓤₀}) †  ≃⟨ Ⅰ ⟩
+      (𝓤₀  ̇) × 𝟙 {𝓤₀}              ≃⟨ Ⅱ ⟩
+      𝓤₀  ̇                         ■
+       where
+        Ⅱ = 𝟙-rneutral {𝓤₁} {𝓤₀} {Y = (𝓤₀  ̇)}
+
 \end{code}
 
 The version of this notion of resizing with truncation, which we denote