Tom de Jong and Martin Escardo, 25th August 2023.

The idea is that there should be no small injective types. However,
with Ω-resizing (a form of impredicativity for HoTT/UF), there are
small injective types, for example Ω 𝓤₀.  So we instead show that,
under some conditions, small injective types give resizing. But at the
moment we are able to derive ꪪ-resizing only (which is a weaker, but
still not provable, form of impredicativity).

It was previously known that if propositional resizing
holds then

 ainjective-type D 𝓤 𝓥 → ainjective-type D 𝓤' 𝓥'

for all universes 𝓤, 𝓥, 𝓤', 𝓥', so that (algebraic) injectivity is
universe independent.

It was also known that

 ainjective-type D (𝓤 ⊔ 𝓣) 𝓥 → ainjective-type D 𝓤 𝓣,

which resizes down the first universe parameter, and that

 * ainjective-type (𝓤 ̇ ) 𝓤 𝓤      (Universes are injective)
 * ainjective-type (Ω 𝓤) 𝓤 𝓤       (the type of propositions is injective)
 * ainjective-type (Ω¬¬ 𝓤) 𝓤 𝓤     (the type of ¬¬-stable propositions is injective)
 * ainjective-type (Ordinal 𝓤) 𝓤 𝓤 (the type of ordinals is injective)
 * ainjective-type (Magma∞ 𝓤) 𝓤 𝓤  (the type of ∞-magmas is injective)
 * ainjective-type (Monoid 𝓤) 𝓤 𝓤  (the type of monoids is injective)
 * ainjective-type (𝕄 𝓤) 𝓤 𝓤       (the type of iterative multisets is injective)
 * ainjective-type (𝕍 𝓤) 𝓤 𝓤       (the type of iterative sets is injective)

among others. We show that the above universe parameters are tight, in
the sense that we cannot increase

 ainjective D 𝓤 𝓤

to

 ainjective D (𝓤 ⁺) 𝓤

for the above choices of D unless we have ꪪ-resizing. In fact, the
third parameter is irrelevant. For any 𝓥, we have that

 ainjective D (𝓤 ⁺) 𝓥

implies ꪪ-resizing for the above choices of D.

We also show that for no type D in the first universe 𝓤₀ can we have

 ainjective D 𝓤₀ 𝓤₀

as soon as it has two distinct points, other than in models that
validate Ω¬¬ 𝓤₀ resizing (in which Ω¬¬ 𝓤₀, being a retract of Ω 𝓤₀, is
injective and serves as an example of such a D).

\begin{code}

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

open import UF.Univalence
open import UF.PropTrunc

module InjectiveTypes.Resizing
        (ua : Univalence)
        (pt : propositional-truncations-exist)
       where

open PropositionalTruncation pt

open import MLTT.Spartan
open import UF.FunExt
open import UF.NotNotStablePropositions
open import UF.Retracts
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.UA-FunExt

private
 fe : FunExt
 fe = Univalence-gives-FunExt ua

 fe' : Fun-Ext
 fe' {𝓤} {𝓥} = fe 𝓤 𝓥

 pe : PropExt
 pe = Univalence-gives-PropExt ua

 pe' : Prop-Ext
 pe' {𝓤} = pe 𝓤

open import InjectiveTypes.Article ua pt
open import InjectiveTypes.OverSmallMaps fe

\end{code}

Below we use the fact that retracts of small types are small, which in turn
relies on a construction of Mike Shulman, called
Shulman's-Splitting-Construction here, see UF.Size for more details.

\begin{code}

small-ainjective-type-with-two-distinct-points-gives-ꪪ-resizing
 : Shulman's-Splitting-Construction
 → (D : 𝓤 ̇ )
 → ainjective-type D (𝓤 ⊔ 𝓥) 𝓦
 → has-two-distinct-points D
 → Ω¬¬ 𝓤 is 𝓤 small
small-ainjective-type-with-two-distinct-points-gives-ꪪ-resizing
 {𝓤} {𝓥} {𝓦} ssc D D-ainj ((x₀ , x₁) , distinct) = II I
 where
  f : 𝟚 → D
  f ₀ = x₀
  f ₁ = x₁

  I : Σ s ꞉ (Ω¬¬ 𝓤 → D) , s ∘ 𝟚-to-Ω¬¬ ∼ f
  I = ainjectivity-over-small-maps 𝓥
       D
       D-ainj
       𝟚-to-Ω¬¬
       (𝟚-to-Ω¬¬-is-embedding fe pe)
       (𝟚-to-Ω¬¬-is-small-map fe pe)
       f

  II : type-of I → Ω¬¬ 𝓤 is 𝓤 small
  II (s , extension-property) = ꪪ-is-small
   where
    III : s ⊥Ω¬¬ ＝ x₀
    III = extension-property ₀

    IV : s ⊤Ω¬¬ ＝ x₁
    IV = extension-property ₁

    V : (𝕡 : Ω¬¬ 𝓤) → s 𝕡 ≠ x₀ → pr₁ 𝕡 holds
    V 𝕡 e = V₃
     where
      V₀ : 𝕡 ＝ ⊥Ω¬¬ → s 𝕡 ＝ x₀
      V₀ e = transport⁻¹ (λ - → s - ＝ x₀) e III
      V₁ : 𝕡 ≠ ⊥Ω¬¬
      V₁ = contrapositive V₀ e
      V₂ : ¬¬ (𝕡 holds')
      V₂ u = V₁ (to-Ω¬¬-＝ fe' (fails-gives-equal-⊥ pe' fe' (Ω¬¬-to-Ω 𝕡) u))
      V₃ : 𝕡 holds'
      V₃ = holds'-is-¬¬-stable 𝕡 V₂

    VI  : (𝕡 : Ω¬¬ 𝓤) → pr₁ 𝕡 holds → s 𝕡 ≠ x₀
    VI 𝕡 h = VI₃
     where
      VI₀ : Ω¬¬-to-Ω 𝕡 ＝ ⊤
      VI₀ = holds-gives-equal-⊤ pe' fe' (Ω¬¬-to-Ω 𝕡) h
      VI₁ : 𝕡 ＝ ⊤Ω¬¬
      VI₁ = to-Ω¬¬-＝ fe' VI₀
      VI₂ : s 𝕡 ＝ x₁
      VI₂ = transport⁻¹ (λ - → s - ＝ x₁) VI₁ IV
      VI₃ : s 𝕡 ≠ x₀
      VI₃ e = distinct
               (x₀  ＝⟨ e ⁻¹ ⟩
                s 𝕡 ＝⟨ VI₂ ⟩
                x₁  ∎)

    VII : (𝕡 : Ω¬¬ 𝓤) → (s 𝕡 ≠ x₀) ＝ (pr₁ 𝕡 holds)
    VII 𝕡 = pe' (negations-are-props fe')
                (holds'-is-prop 𝕡)
                (V 𝕡)
                (VI 𝕡)

    r : D → Ω¬¬ 𝓤
    r d = ((d ≠ x₀) , negations-are-props fe') , ¬-is-¬¬-stable

    rs : r ∘ s ∼ id
    rs 𝕡 = r (s 𝕡)              ＝⟨refl⟩
           ((s 𝕡 ≠ x₀) , _) , _ ＝⟨ to-Ω¬¬-＝' fe' (VII 𝕡) ⟩
           𝕡                     ∎

    ρ : retract (Ω¬¬ 𝓤) of D
    ρ = r , s , rs

    Ω¬¬-is-small : Ω¬¬ 𝓤 is 𝓤 small
    Ω¬¬-is-small = retracts-of-small-types-are-small fe' ssc ρ (native-size D)

\end{code}

A special case of the above is the following, which says that no type
in the first universe 𝓤₀ can be injective as soon as it has two
distinct points, other than in models that validate Ω¬¬ 𝓤₀ resizing
(in which Ω¬¬ 𝓤₀, being a retract of Ω 𝓤₀, is injective).

\begin{code}

small₀-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing
 : Shulman's-Splitting-Construction
 → (D : 𝓤₀ ̇ )
 → ainjective-type D 𝓤₀ 𝓤₀
 → has-two-distinct-points D
 → Ω¬¬ 𝓤₀ is 𝓤₀ small
small₀-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing =
 small-ainjective-type-with-two-distinct-points-gives-ꪪ-resizing

\end{code}

Of course, making the universe parameters for the injectivity of D
bigger doesn't help:

\begin{code}

small₁-ainjective-types-with-two-distinct-points-gives-Ω¬¬-resizing
 : Shulman's-Splitting-Construction
 → (D : 𝓤₀ ̇ )
 → ainjective-type D 𝓥 𝓦
 → has-two-distinct-points D
 → Ω¬¬ 𝓤₀ is 𝓤₀ small
small₁-ainjective-types-with-two-distinct-points-gives-Ω¬¬-resizing =
 small-ainjective-type-with-two-distinct-points-gives-ꪪ-resizing

\end{code}

Question. Can the homotopy circle S¹ be injective, for some choice of
universe parameter, without assuming excluded middle or resizing? If
not, can any other connected type in the first universe 𝓤₀, possibly
assuming higher-inductive types, be injective without classical or
resizing assumptions?

The above also shows that e.g. the result that

  ainjective-type (𝓤 ̇ ) 𝓤 𝓤

is tight. If we increase the first occurrence of 𝓤 to 𝓤 ⁺ then we get
ꪪ-resizing.

The second occurrence is not important, because we always have

 ainjective-type D (𝓤 ⊔ 𝓣) 𝓥 → ainjective-type D 𝓤 𝓣,

and in particular e.g.

  ainjective-type (𝓤 ̇ ) (𝓤 ⁺) 𝓥 → ainjective-type (𝓤 ̇ ) (𝓤 ⁺) (𝓤 ⁺).

\begin{code}

module ꪪ-resizing-examples
        (ssc : Shulman's-Splitting-Construction)
       where

 open import Iterative.Multisets
 open import Iterative.Multisets-Addendum ua
 open import Iterative.Sets ua
 open import Iterative.Sets-Addendum ua
 open import Ordinals.Arithmetic fe
 open import Ordinals.Injectivity
 open import Ordinals.Type

 recall-𝓤-ainjective : ainjective-type (𝓤 ̇ ) 𝓤 𝓤
 recall-𝓤-ainjective = universes-are-ainjective-Π

 recall-ainjective-resizing : (D : 𝓦 ̇ )
                            → ainjective-type D (𝓤 ⊔ 𝓣) 𝓥
                            → ainjective-type D 𝓤 𝓣
 recall-ainjective-resizing = ainjective-resizing₁

 𝓤-ainjective-resizing : ainjective-type (𝓤 ̇ ) (𝓤 ⁺) 𝓥
                       → ainjective-type (𝓤 ̇ ) (𝓤 ⁺) (𝓤 ⁺)
 𝓤-ainjective-resizing = ainjective-resizing₁ _

 𝓤-example : ainjective-type (𝓤 ̇ ) (𝓤 ⁺ ⊔ 𝓥) 𝓦
           → Ω¬¬ (𝓤 ⁺) is 𝓤 ⁺ small
 𝓤-example {𝓤} {𝓥} {𝓦} ainj =
  small-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing {𝓤 ⁺} {𝓥} {𝓦}
   ssc
   (𝓤 ̇ )
   ainj
   ((𝟘 {𝓤} , 𝟙 {𝓤}) , 𝟘-is-not-𝟙)

 𝓤-example₀ : ainjective-type (𝓤 ̇ ) (𝓤 ⁺) 𝓦
            → Ω¬¬ (𝓤 ⁺) is 𝓤 ⁺ small
 𝓤-example₀ {𝓤} {𝓦} = 𝓤-example {𝓤} {𝓢} {𝓦}
  where
   𝓢 = 𝓤
   -- 𝓢 = 𝓤₀   -- also works
   -- 𝓢 = 𝓤 ⁺  -- also works

 recall-Ω-ainjective : ainjective-type (Ω 𝓤) 𝓤 𝓤
 recall-Ω-ainjective = Ω-ainjective

 Ω-example : ainjective-type (Ω 𝓤) (𝓤 ⁺) 𝓦
           → Ω¬¬ (𝓤 ⁺) is 𝓤 ⁺ small
 Ω-example {𝓤} {𝓦} ainj =
  small-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing {𝓤 ⁺} {𝓤} {𝓦}
   ssc
   (Ω 𝓤)
   ainj
   ((⊥ , ⊤) , ⊥-is-not-⊤)

 Ω¬¬-ainjective : ainjective-type (Ω¬¬ 𝓤) 𝓤 𝓤
 Ω¬¬-ainjective {𝓤} = retract-of-ainjective (Ω¬¬ 𝓤) (Ω 𝓤)
                       Ω-ainjective
                       (Ω¬¬-is-retract-of-Ω fe' pe')

 Ω¬¬-example : ainjective-type (Ω¬¬ 𝓤) (𝓤 ⁺) 𝓦
             → Ω¬¬ (𝓤 ⁺) is 𝓤 ⁺ small
 Ω¬¬-example {𝓤} {𝓦} ainj =
  small-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing {𝓤 ⁺} {𝓤} {𝓦}
   ssc
   (Ω¬¬ 𝓤)
   ainj
   ((⊥Ω¬¬ , ⊤Ω¬¬) , ⊥Ω¬¬-is-not-⊤Ω¬¬)

 recall-Ordinal-ainjective : ainjective-type (Ordinal 𝓤) 𝓤 𝓤
 recall-Ordinal-ainjective = ordinals-injectivity.Ordinal-is-ainjective fe (ua _)

 Ordinal-example : ainjective-type (Ordinal 𝓤) (𝓤 ⁺) 𝓦
                 → Ω¬¬ (𝓤 ⁺) is 𝓤 ⁺ small
 Ordinal-example {𝓤} {𝓦} ainj =
  small-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing {𝓤 ⁺} {𝓤} {𝓦}
   ssc
   (Ordinal 𝓤)
   ainj
   ((𝟘ₒ , 𝟙ₒ) , 𝟘ₒ-is-not-𝟙ₒ)

 recall-Multisets-ainjective : ainjective-type (𝕄 𝓤) 𝓤 𝓤
 recall-Multisets-ainjective {𝓤} = 𝕄-is-ainjective 𝓤

 Multiset-example : ainjective-type (𝕄 𝓤) (𝓤 ⁺) 𝓦
                  → Ω¬¬ (𝓤 ⁺) is 𝓤 ⁺ small
 Multiset-example {𝓤} {𝓦} ainj =
  small-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing {𝓤 ⁺} {𝓤} {𝓦}
   ssc
   (𝕄 𝓤)
   ainj
   ((𝟘ᴹ 𝓤 , 𝟙ᴹ 𝓤) , 𝟘ᴹ-is-not-𝟙ᴹ 𝓤)

 recall-Iterative-sets-ainjective : Set-Replacement pt → ainjective-type (𝕍 𝓤) 𝓤 𝓤
 recall-Iterative-sets-ainjective {𝓤} = 𝕍-is-ainjective 𝓤 pt

 Iterative-set-example : ainjective-type (𝕍 𝓤) (𝓤 ⁺) 𝓦
                       → Ω¬¬ (𝓤 ⁺) is 𝓤 ⁺ small
 Iterative-set-example {𝓤} {𝓦} ainj =
  small-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing {𝓤 ⁺} {𝓤} {𝓦}
   ssc
   (𝕍 𝓤)
   ainj
   ((𝟘ⱽ 𝓤 , 𝟙ⱽ 𝓤) , 𝟘ⱽ-is-not-𝟙ⱽ 𝓤)

\end{code}

TODO. The type of monoids is injective (InjectiveTypes.MathematicalStructures).
We get the same resizing conclusion as above by considering the
monoids freely generated by the types 𝟘 and 𝟙 respectively (singleton
monoid and monoid of natural numbers).