Ian Ray, 4th Febuary 2024.

Modifications made by Ian Ray on 14 October 2024.

Modifications made by Ian Ray on 7 January 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

\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'. Also, note that in what follows we only use univalence locally
as some critical results hold in its absence.

\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. In the paper 'the join
construction' by Egbert Rijke, the axiom of replacement is shown to follow from
the join construction. Currently, the join construction and the derivation of the
axiom of replacement are not implemented in the TypeTopology library. We will
state a more convenient but equivalent form of replacement.

\begin{code}

open connectedness-results te
open PropositionalTruncation pt

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

\end{code}

Notice that under the assumption that f : A β†’ X is βˆ’1 connected (i.e. surjective)
the image of f is equivalent to X. We will explicitly assume Replacement' when
necessary.

TODO. Implement the join construction and derive Replacement (with small image as
its conclusion) and Replacement' (with -1 connected assumption and small codomain
as its conclusion). Then remove Replacement' as an explicit assumption below.

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

Prop 2.2 of [1]

\begin{code}

Prop-2-2[locally-small-type-with-connected-map-from-small-type-is-small]
 : {𝓀 𝓦 : Universe} {A : 𝓀 Μ‡ } {X : 𝓦 Μ‡ } {f : A β†’ X} {n : β„•β‚‹β‚‚}
 β†’ Univalence
 β†’ Replacement' {𝓀} {𝓦}
 β†’ 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} ua j 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} ua j f-con A-small X-is-loc-small =
 j 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]
    ua j (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}

Lemma-2-5[connected-type-with-truncated-map-to-locally-small-type-is-small]
 : {X : 𝓀 Μ‡ } {Y : 𝓦 Μ‡ } {f : X β†’ Y} {n : β„•β‚‹β‚‚}
 β†’ Univalence
 β†’ Replacement' {𝓀} {𝓀}
 β†’ 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} ua j 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 j (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 : β„•β‚‹β‚‚}
 β†’ Univalence
 β†’ Replacement' {𝓀} {𝓀}
 β†’ 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} ua j (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 j 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 : β„•β‚‹β‚‚}
 β†’ Univalence
 β†’ Replacement' {𝓀} {𝓀}
 β†’ X is ΞΉ (n + 2) locally-small
  Γ— βˆ₯ X βˆ₯[ n + 1 ] is π“₯ small
 β†’ X is π“₯ small
locally-small-type-with-small-truncation-is-small {_} {X} {n} ua j small-hyp =
 smallness-closed-under-≃'
  (small-path-space-from-locally-small-type-and-small-truncation ua j 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 : β„•β‚‹β‚‚}
 β†’ Univalence
 β†’ Replacement' {𝓀} {𝓀}
 β†’ 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} ua j =
 (I , locally-small-type-with-small-truncation-is-small ua j)
 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 : Univalence
                                    β†’ Replacement'
                                    β†’ is-large βˆ₯ π“₯ Μ‡ βˆ₯[ 0 ]
set-truncation-of-universe-is-large ua j =
 contrapositive I universes-are-large
 where
  I : is-small βˆ₯ π“₯ Μ‡ βˆ₯[ 0 ] β†’ is-small (π“₯ Μ‡ )
  I small-trunc = locally-small-type-with-small-truncation-is-small ua j
                   (universes-are-locally-small (ua π“₯) , small-trunc)

\end{code}

Corollary 2.7 of [1]

\begin{code}

Corollary-2-7[type-with-small-truncation-and-truncated-map-to-locally-small-type-is-small]
 : {X : 𝓀 Μ‡ } {Y : 𝓦 Μ‡ } {f : X β†’ Y} {n : β„•β‚‹β‚‚}
 β†’ Univalence
 β†’ Replacement' {𝓀} {𝓀}
 β†’ 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-and-truncated-map-to-locally-small-type-is-small]
 ua j pr f-trunc Y-loc-small trunc-X-small =
 locally-small-type-with-small-truncation-is-small ua j
  (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-and-truncated-map-to-locally-small-type-is-small]

\end{code}

TODO. Proposition 2.8 requires the concept of Homotopy Groups.