Ian Ray, 4th Febuary 2024.

Modifications made by Ian Ray on 14 October 2024.

Modifications made by Ian Ray on 7 January 2025.

Modification made by Ian Ray on 17 August 2025.

We develop some results that relate size, truncation and connectedness from
the following paper:
[1] Christensen, J.D. (2024), Non-accessible localizations.
    Journal of Topology, 17: e12336.
    https://doi.org/10.1112/topo.12336

\begin{code}

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

open import UF.FunExt
open import UF.Truncations
open import MLTT.Spartan hiding (_+_)

module UF.Size-TruncatedConnected
        (fe : Fun-Ext)
        (te : general-truncations-exist fe)
        (π“₯ : Universe)
       where

open import Notation.CanonicalMap
open import Notation.Decimal
open import UF.ConnectedTypes fe
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.PropTrunc
open import UF.SmallnessProperties
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.TruncatedTypes fe
open import UF.TruncationLevels
open import UF.Univalence

private
 pt : propositional-truncations-exist
 pt = general-truncations-give-propositional-truncations fe te

open import UF.ImageAndSurjection pt
open import UF.Replacement pt

\end{code}

We begin by giving some definitions from [1] and proving important properties
about them. We have fixed the universe parameter π“₯ and use it as our point of
reference for 'smallness'. Univalence is not required for every result, so we
will explicitly assume it only when it is used.

\begin{code}

_is_locally-small : (X : 𝓀 Μ‡ ) β†’ (n : β„•) β†’ 𝓀 βŠ” (π“₯ ⁺) Μ‡
X is zero locally-small = X is π“₯ small
X is (succ n) locally-small = (x x' : X) β†’ (x ＝ x') is n locally-small

being-locally-small-is-prop : {X : 𝓀 Μ‡ } {n : β„•}
                            β†’ Univalence
                            β†’ is-prop (X is n locally-small)
being-locally-small-is-prop {_} {X} {zero} ua = being-small-is-prop ua X π“₯
being-locally-small-is-prop {_} {X} {succ n} ua
 = Ξ β‚‚-is-prop fe (Ξ» x y β†’ being-locally-small-is-prop ua)

being-locally-small-is-upper-closed : {X : 𝓀 Μ‡ } {n : β„•}
                                    β†’ X is n locally-small
                                    β†’ X is (succ n) locally-small
being-locally-small-is-upper-closed {_} {X} {zero}
 = small-implies-locally-small X π“₯
being-locally-small-is-upper-closed {_} {X} {succ n} X-loc-small x x'
 = being-locally-small-is-upper-closed (X-loc-small x x')

locally-small-types-are-small : {X : 𝓀 Μ‡ } {n : β„•}
                              β†’ X is π“₯ small
                              β†’ X is n locally-small
locally-small-types-are-small {_} {_} {zero} X-small = X-small
locally-small-types-are-small {_} {X} {succ n} X-small x x'
 = locally-small-types-are-small (small-implies-locally-small X π“₯ X-small x x')

\end{code}

Local smallness is closed under equivalence, sigma types and truncation for
each n : β„•.

\begin{code}

local-smallness-is-closed-under-≃ : {X : 𝓀 Μ‡ } {Y : 𝓦 Μ‡ } {n : β„•}
                                  β†’ X ≃ Y
                                  β†’ X is n locally-small
                                  β†’ Y is n locally-small
local-smallness-is-closed-under-≃ {_} {_} {_} {_} {zero} e X-small
 = smallness-closed-under-≃ X-small e
local-smallness-is-closed-under-≃ {_} {_} {_} {_} {succ n} e X-loc-small y y' =
 local-smallness-is-closed-under-≃ path-equiv
  (X-loc-small (⌜ e ⌝⁻¹ y) (⌜ e ⌝⁻¹ y'))
 where
  path-equiv : (⌜ e ⌝⁻¹ y ＝ ⌜ e ⌝⁻¹ y') ≃ (y ＝ y')
  path-equiv = ≃-sym (ap ⌜ e ⌝⁻¹ , ap-is-equiv ⌜ e ⌝⁻¹ (⌜⌝⁻¹-is-equiv e))

local-smallness-is-closed-under-Ξ£ : {X : 𝓀 Μ‡ } {Y : X β†’ 𝓦 Μ‡ } {n : β„•}
                                  β†’ X is n locally-small
                                  β†’ ((x : X) β†’ (Y x) is n locally-small)
                                  β†’ (Ξ£ x κž‰ X , Y x) is n locally-small
local-smallness-is-closed-under-Ξ£ {_} {_} {_} {_} {zero} X-small Y-small
 = Ξ£-is-small X-small Y-small
local-smallness-is-closed-under-Ξ£ {_} {_} {_} {Y} {succ n}
 X-loc-small Y-loc-small (x , y) (x' , y')
 = local-smallness-is-closed-under-≃ (≃-sym Ξ£-＝-≃)
    (local-smallness-is-closed-under-Ξ£ (X-loc-small x x')
     (Ξ» - β†’ Y-loc-small x' (transport Y - y) y'))

open general-truncations-exist te

local-smallness-is-closed-under-truncation
 : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚}
 β†’ Univalence
 β†’ X is ΞΉ (n + 2) locally-small
 β†’ βˆ₯ X βˆ₯[ n ] is ΞΉ (n + 2) locally-small
local-smallness-is-closed-under-truncation {_} {X} {βˆ’2} ua
 = truncations-of-small-types-are-small
local-smallness-is-closed-under-truncation {_} {X} {succ n} ua X-loc-small
 = βˆ₯βˆ₯β‚™-indβ‚‚ (Ξ» u v β†’ (u ＝ v) is ΞΉ (n + 2) locally-small)
            (Ξ» u v β†’ truncation-levels-are-upper-closed' ⋆
             (is-prop-implies-is-prop' (being-locally-small-is-prop ua)))
            (Ξ» x y β†’ local-smallness-is-closed-under-≃
             (eliminated-trunc-identity-char (ua _))
             (local-smallness-is-closed-under-truncation ua (X-loc-small x y)))

\end{code}

Many of the results in [1] follow from a fact that some call the type theoretic
axiom of replacement. It states that given a small type A, a locally small type
X and a function f : A β†’ X the image of f is small.

We note that while the name for this result is due to its 'apparent' similarity
to the axiom of replacement from set theory, but replacement in type theory is
quite a modest assumption in comparison. Indeed, type replacement follows from
the existence of pushouts (see UF/Replacement for further discussion on the
modest strength of replacement) as demonstrated by "The Join Construction" by
Egbert Rijke (https://arxiv.org/abs/1701.07538).

In the interest of keeping the present work self-contained and requiring only
the weakest assumptions possible, we simply assume the relevant form of
replacement as it is needed.

\begin{code}

open connectedness-results te

Replacement'' : {𝓀 𝓦 : Universe} β†’ (π“₯ ⁺) βŠ” (𝓀 ⁺) βŠ” (𝓦 ⁺) Μ‡
Replacement'' {𝓀} {𝓦} = {A : 𝓀 Μ‡ } {X : 𝓦 Μ‡ } {f : A β†’ X}
                      β†’ A is π“₯ small
                      β†’ X is 1 locally-small
                      β†’ f is βˆ’1 connected-map
                      β†’ X is π“₯ small

Replacement'-to-Replacement'' : {𝓀 𝓦 : Universe}
                              β†’ Replacement' {π“₯} {𝓀} {𝓦} β†’ Replacement'' {𝓀} {𝓦}
Replacement'-to-Replacement'' rep' {_} {_} {f} A-sm X-ls f-con
 = rep' f A-sm X-ls (βˆ’1-connected-maps-are-surjections f-con)

Replacement''-to-Replacement' : {𝓀 𝓦 : Universe}
                              β†’ Replacement'' {𝓀} {𝓦} β†’ Replacement' {π“₯} {𝓀} {𝓦}
Replacement''-to-Replacement' rep'' {_} {_} f A-sm X-ls f-surj
 = rep'' A-sm X-ls (surjections-are-βˆ’1-connected f-surj)

\end{code}

We will now begin proving some of the results from [1]. We avoid any unnecessary
use of propositional resizing. Theorem numbers will be provided for easy
reference.

Prop 2.2 of [1]

\begin{code}

open PropositionalTruncation pt

module _ (ua : Univalence)
         (rep : {𝓀 𝓦 : Universe} β†’ Replacement'' {𝓀} {𝓦})
       where

 Prop-2-2[locally-small-type-with-connected-map-from-small-type-is-small]
  : {𝓀 𝓦 : Universe} {A : 𝓀 Μ‡ } {X : 𝓦 Μ‡ } {f : A β†’ X} {n : β„•β‚‹β‚‚}
  β†’ f is n connected-map
  β†’ A is π“₯ small
  β†’ X is ΞΉ (n + 2) locally-small
  β†’ X is π“₯ small
 Prop-2-2[locally-small-type-with-connected-map-from-small-type-is-small]
  {_} {_} {_} {_} {_} {βˆ’2} f-con A-small X-small = X-small
 Prop-2-2[locally-small-type-with-connected-map-from-small-type-is-small]
  {𝓀} {𝓦} {A} {X} {f} {succ n} f-con A-small X-is-loc-small
  = rep A-small (III (βˆ’1-connected-maps-are-surjections I)) I
  where
   I : f is βˆ’1 connected-map
   I = map-connectedness-is-lower-closed ⋆ f-con
   II : (x x' : X)
      β†’ Ξ£ a κž‰ A , f a ＝ x
      β†’ Ξ£ a κž‰ A , f a ＝ x'
      β†’ (x ＝ x') is π“₯ small
   II .(f a) .(f a') (a , refl) (a' , refl)
    = Prop-2-2[locally-small-type-with-connected-map-from-small-type-is-small]
       (ap-is-less-connected (ua (𝓀 βŠ” 𝓦)) f f-con)
        (small-implies-locally-small A π“₯ A-small a a')
         (X-is-loc-small (f a) (f a'))
   III : is-surjection f
       β†’ (x x' : X)
       β†’ (x ＝ x') is π“₯ small
   III f-is-surj x x' = βˆ₯βˆ₯-recβ‚‚ (being-small-is-prop ua (x ＝ x') π“₯)
                         (II x x') (f-is-surj x) (f-is-surj x')

 locally-small-type-with-connected-map-from-small-type-is-small =
  Prop-2-2[locally-small-type-with-connected-map-from-small-type-is-small]

\end{code}

Lemma 2.3 of [1]

\begin{code}

Lemma-2-3[truncated-types-are-locally-small] : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚}
                                             β†’ Propositional-Resizing
                                             β†’ X is (n + 1) truncated
                                             β†’ X is ΞΉ (n + 2) locally-small
Lemma-2-3[truncated-types-are-locally-small] {_} {X} {βˆ’2} pr X-prop
 = pr X (is-prop'-implies-is-prop X-prop)
Lemma-2-3[truncated-types-are-locally-small] {_} {_} {succ n} pr X-trunc x x'
 = Lemma-2-3[truncated-types-are-locally-small] pr (X-trunc x x')

truncated-types-are-locally-small = Lemma-2-3[truncated-types-are-locally-small]

\end{code}

We note that Lemma 2.3 provides one side of a bimplication involving
propositional resizing. We will now record the other direction.

\begin{code}

truncated-types-are-locally-small-gives-propositional-resizing
 : ({X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚} β†’ X is (n + 1) truncated β†’ X is ΞΉ (n + 2) locally-small)
 β†’ propositional-resizing 𝓀 π“₯
truncated-types-are-locally-small-gives-propositional-resizing
 trunc-gives-loc-small P P-prop
 = trunc-gives-loc-small {P} {βˆ’2} (is-prop-implies-is-prop' P-prop)

\end{code}

Lemma 2.4 of [1]

\begin{code}

Lemma-2-4[type-with-truncated-map-to-locally-small-type-is-locally-small]
 : {X : 𝓀 Μ‡ } {Y : 𝓦 Μ‡ } {f : X β†’ Y} {n : β„•β‚‹β‚‚}
 β†’ Propositional-Resizing
 β†’ f is (n + 1) truncated-map
 β†’ Y is ΞΉ (n + 2) locally-small
 β†’ X is ΞΉ (n + 2) locally-small
Lemma-2-4[type-with-truncated-map-to-locally-small-type-is-locally-small]
 {_} {_} {_} {_} {f} {_} pr f-trunc Y-loc-small
 = local-smallness-is-closed-under-≃ (total-fiber-is-domain f)
    (local-smallness-is-closed-under-Ξ£ Y-loc-small
     (Ξ» y β†’ Lemma-2-3[truncated-types-are-locally-small] pr (f-trunc y)))

type-with-truncated-map-to-locally-small-type-is-locally-small
 = Lemma-2-4[type-with-truncated-map-to-locally-small-type-is-locally-small]

\end{code}

Lemma 2.5 of [1]

\begin{code}

module _ (ua : Univalence)
         (rep : {𝓀 𝓦 : Universe} β†’ Replacement'' {𝓀} {𝓦})
       where

 Lemma-2-5[connected-type-with-truncated-map-to-locally-small-type-is-small]
  : {X : 𝓀 Μ‡ } {Y : 𝓦 Μ‡ } {f : X β†’ Y} {n : β„•β‚‹β‚‚}
  β†’ Propositional-Resizing
  β†’ f is (n + 1) truncated-map
  β†’ Y is ΞΉ (n + 2) locally-small
  β†’ X is (n + 1) connected
  β†’ X is π“₯ small
 Lemma-2-5[connected-type-with-truncated-map-to-locally-small-type-is-small]
  {𝓀} {_} {X} {_} {_} {n} pr f-trunc Y-loc-small X-conn
  = βˆ₯βˆ₯-rec (being-small-is-prop ua X π“₯) VI (center II)
  where
   I : X is ΞΉ (n + 2) locally-small
   I = Lemma-2-4[type-with-truncated-map-to-locally-small-type-is-locally-small]
        pr f-trunc Y-loc-small
   II : X is βˆ’1 connected
   II = connectedness-is-lower-closed' ⋆ X-conn
   III : X β†’ πŸ™ {𝓀} β†’ X
   III x ⋆ = x
   IV : (x : X) β†’ (III x) is n connected-map
   IV x = basepoint-map-is-less-connected (ua _) (III x) X-conn
   V : πŸ™ {𝓀} is π“₯ small
   V = pr πŸ™ πŸ™-is-prop
   VI : X β†’ X is π“₯ small
   VI x
    = Prop-2-2[locally-small-type-with-connected-map-from-small-type-is-small]
       ua rep (IV x) V I

 connected-type-with-truncated-map-to-locally-small-type-is-small
  = Lemma-2-5[connected-type-with-truncated-map-to-locally-small-type-is-small]

\end{code}

In [1] Christensen proves Theorem 2.6 with propositional resizing and without.
In the presence of resizing Theorem 2.6 follows from previous results, but as
we are interested in avoiding unnecessary use of propositional resizing, we
choose to record the latter proof. It is a bit more involved, so we will first
need to prove a few lemmas.

\begin{code}

 small-path-space-from-locally-small-type-and-small-truncation
  : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚}
  β†’ X is ΞΉ (n + 2) locally-small
   Γ— βˆ₯ X βˆ₯[ n + 1 ] is π“₯ small
  β†’ (Ξ£ y κž‰ βˆ₯ X βˆ₯[ n + 1 ] , Ξ£ x κž‰ X , ∣ x ∣[ n + 1 ] ＝ y) is π“₯ small
 small-path-space-from-locally-small-type-and-small-truncation
  {𝓀} {X} {n} (X-loc-small , trunc-X-small) = Ξ£-is-small trunc-X-small IX
  where
   I : (x' : X) β†’ (Ξ£ x κž‰ X , ∣ x ∣[ n + 1 ] ＝ ∣ x' ∣[ n + 1 ]) is π“₯ small
   I x'
    = Prop-2-2[locally-small-type-with-connected-map-from-small-type-is-small]
       ua rep IV V VI
    where
     II : πŸ™ {𝓀} β†’ Ξ£ x κž‰ X , ∣ x ∣[ n + 1 ] ＝ ∣ x' ∣[ n + 1 ]
     II ⋆ = (x' , refl)
     III : (Ξ£ x κž‰ X , ∣ x ∣[ n + 1 ] ＝ ∣ x' ∣[ n + 1 ]) is (n + 1) connected
     III = trunc-map-is-connected ∣ x' ∣[ n + 1 ]
     IV : II is n connected-map
     IV = basepoint-map-is-less-connected (ua _) II III
     V : πŸ™ {𝓀} is π“₯ small
     V = (πŸ™ {π“₯} , one-πŸ™-only)
     VI : (Ξ£ x κž‰ X , ∣ x ∣[ n + 1 ] ＝ ∣ x' ∣[ n + 1 ])
           is ΞΉ (n + 2) locally-small
     VI = local-smallness-is-closed-under-Ξ£ X-loc-small VII
      where
       VII : (x : X)
           β†’ (∣ x ∣[ succ n ] ＝ ∣ x' ∣[ succ n ]) is ΞΉ (n + 2) locally-small
       VII x = local-smallness-is-closed-under-≃
                (eliminated-trunc-identity-char (ua _)) VIII
        where
         VIII : βˆ₯ x ＝ x' βˆ₯[ n ] is ΞΉ (n + 2) locally-small
         VIII = local-smallness-is-closed-under-truncation
                 ua (being-locally-small-is-upper-closed X-loc-small x x')
   IX : (y : βˆ₯ X βˆ₯[ n + 1 ]) β†’ (Ξ£ x κž‰ X , ∣ x ∣[ n + 1 ] ＝ y) is π“₯ small
   IX = βˆ₯βˆ₯β‚™-ind (Ξ» - β†’ props-are-truncated pt
         (being-small-is-prop ua (Ξ£ x κž‰ X , ∣ x ∣[ n + 1 ] ＝ -) π“₯)) I

 locally-small-type-with-small-truncation-is-small
  : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚}
  β†’ X is ΞΉ (n + 2) locally-small
    Γ— βˆ₯ X βˆ₯[ n + 1 ] is π“₯ small
  β†’ X is π“₯ small
 locally-small-type-with-small-truncation-is-small {_} {X} {n} small-hyp
  = smallness-closed-under-≃'
     (small-path-space-from-locally-small-type-and-small-truncation small-hyp)
      (domain-is-total-fiber ∣_∣[ succ n ])

\end{code}

Theorem 2.6 of [1]

\begin{code}

 Theorem-2-6[type-is-small-iff-type-is-locally-small-and-has-small-truncation]
  : {X : 𝓀 Μ‡ } {n : β„•β‚‹β‚‚}
  β†’ X is π“₯ small
  ↔ X is ΞΉ (n + 2) locally-small Γ— βˆ₯ X βˆ₯[ n + 1 ] is π“₯ small
 Theorem-2-6[type-is-small-iff-type-is-locally-small-and-has-small-truncation]
  {_} {X} {n}
  = (I , locally-small-type-with-small-truncation-is-small)
  where
   I : X is π“₯ small
     β†’ X is ΞΉ (n + 2) locally-small Γ— βˆ₯ X βˆ₯[ n + 1 ] is π“₯ small
   I X-small = (locally-small-types-are-small X-small ,
                truncations-of-small-types-are-small X-small)

 type-is-small-iff-type-is-locally-small-and-has-small-truncation =
  Theorem-2-6[type-is-small-iff-type-is-locally-small-and-has-small-truncation]

\end{code}

We will record the following corollary of Theorem 2.6 from [1]:
 The set truncation of a universe is large (i.e. not small).

\begin{code}

 set-truncation-of-universe-is-large : is-large βˆ₯ π“₯ Μ‡ βˆ₯[ 0 ]
 set-truncation-of-universe-is-large = contrapositive I universes-are-large
  where
   I : is-small βˆ₯ π“₯ Μ‡ βˆ₯[ 0 ] β†’ is-small (π“₯ Μ‡ )
   I small-trunc = locally-small-type-with-small-truncation-is-small
                    (universes-are-locally-small (ua π“₯) , small-trunc)

\end{code}

Corollary 2.7 of [1]

\begin{code}

 Corollary-2-7[type-with-small-truncation-truncated-map-to-locally-small-is-small]
  : {X : 𝓀 Μ‡ } {Y : 𝓦 Μ‡ } {f : X β†’ Y} {n : β„•β‚‹β‚‚}
  β†’ Propositional-Resizing
  β†’ f is (n + 1) truncated-map
  β†’ Y is ΞΉ (n + 2) locally-small
  β†’ βˆ₯ X βˆ₯[ n + 1 ] is π“₯ small
  β†’ X is π“₯ small
 Corollary-2-7[type-with-small-truncation-truncated-map-to-locally-small-is-small]
  pr f-trunc Y-loc-small trunc-X-small
  = locally-small-type-with-small-truncation-is-small
     (Lemma-2-4[type-with-truncated-map-to-locally-small-type-is-locally-small]
      pr f-trunc Y-loc-small , trunc-X-small)

 type-with-small-truncation-and-truncated-map-to-locally-small-type-is-small
  = Corollary-2-7[type-with-small-truncation-truncated-map-to-locally-small-is-small]

\end{code}

TODO. Proposition 2.8 requires the concept of Homotopy Groups.