Martin Escardo, July 2025.

𝟚-injecting maps and 𝟚-injective types.

The motivation for this discussion is two-fold:

(1) Injective types don't have any non-trivial decidable properties in general.

(2) In particular, totally separated types, which have plenty of
    decidable properties by definition, fail badly to be injective in general.

    Can the totally separated types always be the injective types with
    respect to *some* class of maps?

    We consider 𝟚-injecting maps as a candidate for that. But, for the
    moment, they are not necessarily the answer, although we can show
    that injective types over 𝟚-injecting maps are totally separared.

\begin{code}

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

open import UF.FunExt

module gist.2-injective-types (fe : FunExt) where

open import MLTT.Plus-Properties
open import MLTT.Spartan
open import TypeTopology.TotallySeparated
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.Embeddings
open import UF.PropTrunc
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

private
 fe' : Fun-Ext
 fe' {𝓀} {π“₯} = fe 𝓀 π“₯

\end{code}

The double-dualization monad with base 𝟚, incompletely defined.

\begin{code}

K : 𝓀 Μ‡ β†’ 𝓀 Μ‡
K X = (X β†’ 𝟚) β†’ 𝟚

K-functor : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ K X β†’ K Y
K-functor f Ο• v = Ο• (v ∘ f)

Ξ·α΄· : {X : 𝓀 Μ‡ } β†’ X β†’ K X
Ξ·α΄· x u = u x

ΞΌα΄· : {X : 𝓀 Μ‡ } β†’ K (K X) β†’ K X
ΞΌα΄· F u = F (Ξ» Ο• β†’ Ο• u)

extα΄· : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ K Y) β†’ K X β†’ K Y
extα΄· f Ο• v = Ο• (Ξ» x β†’ f x v)

strengthα΄· : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X Γ— K Y β†’ K (X Γ— Y)
strengthα΄· (x , Ξ³) w = Ξ³ (Ξ» y β†’ w (x , y))

\end{code}

(We probably defined above more than what we need for now, but we may
need it in the future to answer some of the questions below.)

\begin{code}

_is-injective-over_ : (D : 𝓣 Μ‡ ) {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓣 Μ‡
D is-injective-over j = (f : domain j β†’ D) β†’ Ξ£ f' κž‰ (codomain j β†’ D) , f' ∘ j ∼ f

\end{code}

If D is injective over j, we also say that j is D-injecting.

We name the two projections.

\begin{code}

module _
         {D : 𝓦 Μ‡ } {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
         (j : X β†’ Y)
         (i : D is-injective-over j)
         (f : X β†’ D)
       where

 extension : (Y β†’ D)
 extension = pr₁ (i f)

 extension-extends : extension ∘ j ∼ f
 extension-extends = prβ‚‚ (i f)

\end{code}

The D-injecting maps form a wild category.

\begin{code}

injective-over-id : (D : 𝓣 Μ‡ ) {X : 𝓀 Μ‡ }
                  β†’ D is-injective-over (𝑖𝑑 X)
injective-over-id D f = f , ∼-refl

injective-over-∘ : (D : 𝓣 Μ‡ ) {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
                   {j : X β†’ Y} {k : Y β†’ Z}
                 β†’ D is-injective-over j
                 β†’ D is-injective-over k
                 β†’ D is-injective-over (k ∘ j)
injective-over-∘ D {X} {Y} {Z} {j} {k} ji ki f = f'' , f''-extends-f
 where
  f' : Y β†’ D
  f' = extension j ji f

  f'-extends-f : f' ∘ j ∼ f
  f'-extends-f = extension-extends j ji f

  f'' : Z β†’ D
  f'' = extension k ki f'

  f''-extends-f' : f'' ∘ k ∼ f'
  f''-extends-f' = extension-extends k ki f'

  f''-extends-f : f'' ∘ (k ∘ j) ∼ f
  f''-extends-f x = f'' (k (j x)) ＝⟨ f''-extends-f' (j x) ⟩
                    f' (j x)      ＝⟨ f'-extends-f x ⟩
                    f x           ∎

\end{code}

The natural instinct in the following is to assume that D is pointed,
but, more generally, we can assume that D is pointed if Y is pointed,
that is, we have some given function Y β†’ D. Also, it is enough to
assume that j is left-cancellable, rather than an embedding.

\begin{code}

module _ (D : 𝓣 Μ‡ ) {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } where

 lc-map-with-decidable-fibers-is-universally-injecting
  : (j : X β†’ Y)
  β†’ left-cancellable j
  β†’ each-fiber-of j is-decidable
  β†’ (Y β†’ D)
  β†’ D is-injective-over j
 lc-map-with-decidable-fibers-is-universally-injecting j j-lc Ξ΄ g f
  = f' , f'-extends-f
  where
   h : (y : Y) β†’ is-decidable (fiber j y) β†’ D
   h y (inl (x , e)) = f x
   h y (inr Ξ½)       = g y

   f' : Y β†’ D
   f' y = h y (Ξ΄ y)

   H : (x : X) (d : is-decidable (fiber j (j x))) β†’ h (j x) d ＝ f x
   H x (inl (x' , e)) = ap f (j-lc e)
   H x (inr ν)        = 𝟘-elim (ν (x , refl))

   f'-extends-f : f' ∘ j ∼ f
   f'-extends-f x = H x (Ξ΄ (j x))

 inl-is-injective-over : (Y β†’ D) β†’ D is-injective-over (inl {𝓀} {π“₯} {X} {Y})
 inl-is-injective-over g f = cases f g , ∼-refl

 inr-is-injective-over : (X β†’ D) β†’ D is-injective-over (inr {𝓀} {π“₯} {X} {Y})
 inr-is-injective-over g f = cases g f , ∼-refl

\end{code}

In this file we are mostly interesting in the case D = 𝟚. We don't
require 𝟚-injecting maps to be embeddings (but see the discussion
below).

\begin{code}

is-𝟚-injecting : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
is-𝟚-injecting j = 𝟚 is-injective-over j

\end{code}

In topological terms, the above means that every clopen of X can be
extended to a clopen of Y along j.

We say that a type is 𝟚-injective if it is injective over 𝟚-injecting
maps.

\begin{code}

𝟚-injective : 𝓦 Μ‡ β†’ (𝓀 π“₯ : Universe) β†’ 𝓦 βŠ” (𝓀 βŠ” π“₯)⁺ Μ‡
𝟚-injective {𝓦} D 𝓀 π“₯ = {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y)
                        β†’ is-𝟚-injecting j
                        β†’ D is-injective-over j

\end{code}

By construction, the type 𝟚 is 𝟚-injective.

\begin{code}

𝟚-is-𝟚-injective : 𝟚-injective 𝟚 𝓀 π“₯
𝟚-is-𝟚-injective j = id

\end{code}

The 𝟚-injective types are closed under products and retracts.

\begin{code}

𝟚-injectives-closed-under-Ξ  : {I : 𝓣 Μ‡ } {D : I β†’ 𝓦 Μ‡ }
                            β†’ ((i : I) β†’ 𝟚-injective (D i) 𝓀 π“₯)
                            β†’ 𝟚-injective (Ξ  D) 𝓀 π“₯
𝟚-injectives-closed-under-Ξ  {𝓣} {𝓦} {I} {D} D-𝟚-inj j j-𝟚-injecting f =
 (Ξ» y i β†’ extension j (D-𝟚-inj i j j-𝟚-injecting) (Ξ» x β†’ f x i) y) ,
 (Ξ» x β†’ dfunext fe'
 (Ξ» i β†’ extension-extends j (D-𝟚-inj i j j-𝟚-injecting) (Ξ» x β†’ f x i) x))

retract-of-𝟚-injective : (D' : 𝓣' Μ‡ ) (D : 𝓣 Μ‡ )
                       β†’ 𝟚-injective D 𝓀 π“₯
                       β†’ retract D' of D
                       β†’ 𝟚-injective D' 𝓀 π“₯
retract-of-𝟚-injective D' D i (r , s , rs) {X} {Y} j e f = Ο† a
  where
   a : Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ s ∘ f
   a = i j e (s ∘ f)

   Ο† : (Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ s ∘ f) β†’ Ξ£ f'' κž‰ (Y β†’ D') , f'' ∘ j ∼ f
   Ο† (f' , h) = r ∘ f' , (Ξ» x β†’ ap r (h x) βˆ™ rs (f x))

\end{code}

TODO. Formulate the above in more generality with the same proof.

The free algebras of the 𝟚-based double dualization monad are 𝟚-injective.

\begin{code}

first-dual-is-𝟚-injective : {X : 𝓣 Μ‡ } β†’ 𝟚-injective (X β†’ 𝟚) 𝓀 π“₯
first-dual-is-𝟚-injective = 𝟚-injectives-closed-under-Ξ  (Ξ» i β†’ 𝟚-is-𝟚-injective)

K-is-𝟚-injective : {X : 𝓣 Μ‡ } β†’ 𝟚-injective (K X) 𝓀 π“₯
K-is-𝟚-injective = first-dual-is-𝟚-injective

\end{code}

So, for example, the Cantor type (β„• β†’ 𝟚) is 𝟚-injective, and hence so
is β„•βˆž, because it is a retract of the Cantor type).

The unit of the monad is 𝟚-injecting.

\begin{code}

Ξ·α΄·-is-𝟚-injecting : {X : 𝓀 Μ‡ } β†’ is-𝟚-injecting (Ξ·α΄· {𝓀} {X})
Ξ·α΄·-is-𝟚-injecting f = (Ξ» Ο• β†’ Ο• f) , ∼-refl

\end{code}

Hence every 𝟚-injective type is a retract of a free algebra.

\begin{code}

𝟚-injectives-are-K-retracts : {D : 𝓀 Μ‡ }
                            β†’ 𝟚-injective D 𝓀 𝓀
                            β†’ retract D of K D
𝟚-injectives-are-K-retracts D-𝟚-inj =
 extension ηᴷ (D-𝟚-inj ηᴷ ηᴷ-is-𝟚-injecting) id ,
 Ξ·α΄· ,
 extension-extends ηᴷ (D-𝟚-inj ηᴷ ηᴷ-is-𝟚-injecting) id

\end{code}

And therefore the 𝟚-injective types are all totally separated, because
the type 𝟚 is totally separated, and the totally separated types are
closed under products and retracts.

\begin{code}

K-is-totally-separated : {X : 𝓀 Μ‡ } β†’ is-totally-separated (K X)
K-is-totally-separated = Ξ -is-totally-separated fe' (Ξ» _ β†’ 𝟚-is-totally-separated)

𝟚-injectives-are-totally-separated : {D : 𝓀 Μ‡ }
                                   β†’ 𝟚-injective D 𝓀 𝓀
                                   β†’ is-totally-separated D
𝟚-injectives-are-totally-separated D-𝟚-inj =
 retract-of-totally-separated
  (𝟚-injectives-are-K-retracts D-𝟚-inj)
  K-is-totally-separated

\end{code}

The above shows that a 𝟚-injecting map doesn't need to be an
embedding. Indeed, we have seen that the map Ξ·α΄· : X β†’ K X is always
𝟚-injecting, but we also know that it is an embedding if and only if X
is totally separated.

\begin{code}

_ : {X : 𝓀 Μ‡ } β†’ is-embedding (Ξ·α΄· {𝓀} {X}) ↔ is-totally-separated X
_ = totally-separatedβ‚‚-gives-totally-separated fe' ,
    totally-separated-gives-totally-separatedβ‚‚ fe'

\end{code}

The extension requirement is property, even though the choice of
extension is data.

\begin{code}

module _
         {D : 𝓀 Μ‡ } {X : 𝓀 Μ‡ } {Y : 𝓀 Μ‡ }
         (i : 𝟚-injective D 𝓀 𝓀)
         (j : X β†’ Y)
         (k : is-𝟚-injecting j)
         (f : X β†’ D)
       where

 extension-extends-is-prop : is-prop (extension j (i j k) f ∘ j ∼ f)
 extension-extends-is-prop =
  Ξ -is-prop fe'
   (Ξ» x β†’ totally-separated-types-are-sets fe' D
           (𝟚-injectives-are-totally-separated i))

\end{code}

As discussed above, we didn't require 2-injecting maps to be
embeddings. We now show, in a number of steps, that we could have
required them to be embeddings without loss of generality.

\begin{code}

module _ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y) (ji : is-𝟚-injecting j) where

 𝟚-injecting-map-with-totally-separated-domain-is-lc
  : is-totally-separated X β†’ left-cancellable j
 𝟚-injecting-map-with-totally-separated-domain-is-lc  ts {x} {x'} e = ts I
  where
   I : (p : X β†’ 𝟚) β†’ p x ＝ p x'
   I p = e'
    where
     p' : Y β†’ 𝟚
     p' = pr₁ (ji p)

     p'-extends-p : p' ∘ j ∼ p
     p'-extends-p = prβ‚‚ (ji p)

     e' = p x       ＝⟨ (p'-extends-p x)⁻¹ ⟩
          p' (j x)  ＝⟨ ap p' e ⟩
          p' (j x') ＝⟨ p'-extends-p x' ⟩
          p x'      ∎

 𝟚-injecting-map-of-totally-separated-types-is-embedding
  : is-totally-separated X β†’ is-totally-separated Y β†’ is-embedding j
 𝟚-injecting-map-of-totally-separated-types-is-embedding X-ts Y-ts
  = lc-maps-into-sets-are-embeddings j
     (𝟚-injecting-map-with-totally-separated-domain-is-lc X-ts)
     (totally-separated-types-are-sets fe' Y Y-ts)

\end{code}

We now need to assume that propositional truncations exist, to be able
to construct the totally separated reflection of a type.

\begin{code}

module _ (pt : propositional-truncations-exist) where

 open PropositionalTruncation pt
 open totally-separated-reflection fe pt

\end{code}

The unit of the totally separated reflection is 𝟚-injecting.

\begin{code}

 Ξ·α΅€-is-𝟚-injecting : {X : 𝓀 Μ‡ } β†’ is-𝟚-injecting (Ξ·α΅€ {𝓀} {X})
 Ξ·α΅€-is-𝟚-injecting {𝓀} {X} f = extα΅€ 𝟚-is-totally-separated f ,
                               ext-Ξ·α΅€ 𝟚-is-totally-separated f

\end{code}

The reflection of any 𝟚-injecting map is again 𝟚-injecting, and also
always an embedding.

\begin{code}

 module _ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y) (ji : is-𝟚-injecting j) where

  𝕋-is-𝟚-injecting : is-𝟚-injecting (𝕋-functor j)
  𝕋-is-𝟚-injecting q = q' , q'-extends-q
   where
    p : X β†’ 𝟚
    p = q ∘ Ξ·α΅€

    p' : Y β†’ 𝟚
    p' = extension j ji p

    p'-extends-p : p' ∘ j ∼ p
    p'-extends-p = extension-extends j ji p

    q' : 𝕋 Y β†’ 𝟚
    q' = extα΅€ 𝟚-is-totally-separated p'

    q'-extends-q : q' ∘ 𝕋-functor j ∼ q
    q'-extends-q =
     Ξ·α΅€-induction
      (Ξ» t β†’ q' (𝕋-functor j t) ＝ q t)
      (Ξ» t β†’ 𝟚-is-set)
      (Ξ» x β†’ q' (𝕋-functor j (Ξ·α΅€ x))            ＝⟨ refl ⟩
             extα΅€ _ p' (extα΅€ _ (Ξ·α΅€ ∘ j) (Ξ·α΅€ x)) ＝⟨ I x ⟩
             extα΅€ _ p' (Ξ·α΅€ (j x))               ＝⟨ II x ⟩
             p' (j x)                           ＝⟨ p'-extends-p x ⟩
             p x                                ＝⟨ refl ⟩
             q (Ξ·α΅€ x)                           ∎)
      where
       I  = Ξ» x β†’ ap (extα΅€ _ p') (ext-Ξ·α΅€ _ (Ξ·α΅€ ∘ j) x)
       II = Ξ» x β†’ ext-Ξ·α΅€ _ p' (j x)

  𝕋-is-embedding : is-embedding (𝕋-functor j)
  𝕋-is-embedding = 𝟚-injecting-map-of-totally-separated-types-is-embedding
                    (𝕋-functor j)
                    𝕋-is-𝟚-injecting
                    𝕋-is-totally-separated
                    𝕋-is-totally-separated
\end{code}

TODO. The above proof probably doesn't need induction. The reflection
laws should suffice.

The formulation of the following doesn't use propositional
truncations, but its construction does, indirectly.

The following are equivalent for any type D.

1. D is injective over 𝟚-injecting maps.

2. D is totally separated and injective over 𝟚-injecting embeddings of
   totally separated types.

\begin{code}

 is-injective-over-𝟚-injecting-embeddings-of-ts-types
  : 𝓣 Μ‡ β†’ (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯)⁺ βŠ” 𝓣 Μ‡
 is-injective-over-𝟚-injecting-embeddings-of-ts-types D 𝓀 π“₯
  = {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y)
  β†’ is-𝟚-injecting j
  β†’ is-embedding j
  β†’ is-totally-separated X
  β†’ is-totally-separated Y
  β†’ D is-injective-over j

 characterization-of-𝟚-injectivity
  : (D : 𝓀 Μ‡ )
  β†’ 𝟚-injective D 𝓀 𝓀
  ↔ (is-totally-separated D
    Γ— is-injective-over-𝟚-injecting-embeddings-of-ts-types D 𝓀 𝓀)
 characterization-of-𝟚-injectivity {𝓀} D
  = (Ξ» D-𝟚-inj β†’ 𝟚-injectives-are-totally-separated D-𝟚-inj ,
                 (Ξ» j ji _ _ _ β†’ D-𝟚-inj j ji)) ,
    I
  where
   I : is-totally-separated D
     Γ— is-injective-over-𝟚-injecting-embeddings-of-ts-types D 𝓀 𝓀
     β†’ 𝟚-injective D 𝓀 𝓀
   I (D-ts , D-inj) {X} {Y} j ji f = f' , f'-extends-f
    where
     g : 𝕋 X β†’ D
     g = extα΅€ D-ts f

     II : D is-injective-over (𝕋-functor j)
     II = D-inj
           (𝕋-functor j)
           (𝕋-is-𝟚-injecting j ji)
           (𝕋-is-embedding j ji)
           𝕋-is-totally-separated
           𝕋-is-totally-separated

     g' : 𝕋 Y β†’ D
     g' = extension (𝕋-functor j) II g

     g'-extends-g : g' ∘ 𝕋-functor j ∼ g
     g'-extends-g = extension-extends (𝕋-functor j) II g

     f' : Y β†’ D
     f' = g' ∘ Ξ·α΅€

     f'-extends-f : f' ∘ j ∼ f
     f'-extends-f x =
      f' (j x)                ＝⟨ refl ⟩
      g' (Ξ·α΅€ (j x))           ＝⟨ ap g' ((𝕋-natural j x)⁻¹) ⟩
      g' (𝕋-functor j (Ξ·α΅€ x)) ＝⟨ g'-extends-g (Ξ·α΅€ x) ⟩
      g (Ξ·α΅€ x)                ＝⟨ refl ⟩
      extα΅€ D-ts f (Ξ·α΅€ x)      ＝⟨ ext-Ξ·α΅€ D-ts f x ⟩
      f x                     ∎

\end{code}

TODO.

  (1) Can we generalize the universes in
      `𝟚-injectives-are-totally-separated` and (hence much of) the above?

  (2) Can we show that every totally separated type is 𝟚-injective? I
      can't even show, at the time of writing, that β„•, a totally
      separated type, is 𝟚-injective.

  (3) Can we show that the totally separated types are precisely the
      algebras of the 𝟚-based double dualization monad?

  (4) Now let's go back to (algebraic) injectivity with respect to all
      embeddings. Say that a map j : X β†’ Y is injecting if all
      algebraically injective types with respect to embeddings are
      injective with respect to j. Question. Can we show that j is
      necessarily an embedding?  Perhaps an embedding is precisely the
      same thing as an Ξ©-injecting map.

We now show that if all functions 𝟚ᴺ β†’ 𝟚 are uniformly continuous,
then β„• is 𝟚-injective.

\begin{code}

open import MLTT.Two-Properties
open import Naturals.Order
open import Naturals.Properties
open import Notation.Order
open import TypeTopology.Cantor

open notions-of-continuity 𝟚 𝟚-is-discrete

β„•-is-𝟚-injective-if-all-functions-πŸšα΄Ίβ†’πŸš-are-uc
 : ((f : 𝟚ᴺ β†’ 𝟚) β†’ is-uniformly-continuous f)
 β†’ 𝟚-injective β„• 𝓀 π“₯
β„•-is-𝟚-injective-if-all-functions-πŸšα΄Ίβ†’πŸš-are-uc {𝓀} {π“₯} brouwer
 = β„•-is-𝟚-injective
 where
  I : (n : β„•) β†’ (succ n) is-a-modulus-of-uc-of (Ξ·α΄· n)
  I 0        Ξ± Ξ² (e , _ ) = e
  I (succ n) Ξ± Ξ² (_ , es) = I n (tail Ξ±) (tail Ξ²) es

  II : (n k : β„•)
    β†’ k is-a-modulus-of-uc-of (Ξ·α΄· n)
    β†’ Β¬ (k ≀ n)
  II n k is-mod l = impossible
   where
    have-is-mod : (Ξ± Ξ² : 𝟚ᴺ) β†’ Ξ± ＝⟦ k ⟧ Ξ² β†’ Ξ± n ＝ Ξ² n
    have-is-mod = is-mod

    have-l : k ≀ n
    have-l = l

    Ξ³ : β„• β†’ 𝟚ᴺ
    γ 0        = 𝟏
    Ξ³ (succ k) = cons β‚€ (Ξ³ k)

    Ξ³-propertyβ‚€ : (n k : β„•) β†’ k ≀ n β†’ 𝟎 ＝⟦ k ⟧ (Ξ³ k)
    Ξ³-propertyβ‚€ n 0        l = ⋆
    Ξ³-propertyβ‚€ n (succ k) l =
     refl , Ξ³-propertyβ‚€ n k (≀-trans k (succ k) n (≀-succ k) l)

    Ξ³-property₁ : (n k : β„•) β†’ k ≀ n β†’ β‚€ β‰  Ξ³ k n
    Ξ³-property₁ n        0        l e = zero-is-not-one e
    Ξ³-property₁ (succ n) (succ k) l e = Ξ³-property₁ n k l e

    impossible : 𝟘
    impossible = Ξ³-property₁ n k l (is-mod 𝟎 (Ξ³ k) (Ξ³-propertyβ‚€ n k l))

  III : (n k : β„•)
      β†’ k is-a-modulus-of-uc-of (Ξ·α΄· n)
      β†’ succ n ≀ k
  III n k is-mod = not-less-bigger-or-equal (succ n) k (II n k is-mod)

  UC : 𝓀₀ Μ‡
  UC = Ξ£ f κž‰ (𝟚ᴺ β†’ 𝟚) , is-uniformly-continuous f

  s : β„• β†’ UC
  s n = Ξ·α΄· n , succ n , I n , III n

  r : UC β†’ β„•
  r (_ , m , _) = pred m

  rs : r ∘ s ∼ id
  rs n = refl

  β„•-retract-of-UC : retract β„• of UC
  β„•-retract-of-UC = r , s , rs

  IV : UC ≃ (𝟚ᴺ β†’ 𝟚)
  IV = pr₁ ,
       pr₁-is-equiv
        (𝟚ᴺ β†’ 𝟚)
        is-uniformly-continuous
        (Ξ» f β†’ pointed-props-are-singletons
                (brouwer f)
                (being-uniformly-continuous-is-prop fe' f))

  β„•-retract-of-πŸšα΄Ίβ†’πŸš : retract β„• of (𝟚ᴺ β†’ 𝟚)
  β„•-retract-of-πŸšα΄Ίβ†’πŸš = retracts-compose (≃-gives-◁ IV) β„•-retract-of-UC

  β„•-is-𝟚-injective : 𝟚-injective β„• 𝓀 π“₯
  β„•-is-𝟚-injective = retract-of-𝟚-injective β„• (𝟚ᴺ β†’ 𝟚)
                      K-is-𝟚-injective
                      β„•-retract-of-πŸšα΄Ίβ†’πŸš
\end{code}

Originally I tried to prove that UC is 𝟚-injective, to avoid the
Brouwerian assumption, but I didn't succeed, and I doubt this can be done.

TODO. In the topological topos, we in fact have that β„• ≃ (𝟚ᴺ β†’ 𝟚),
and, indeed, this can be proved from our Brouwerian assumption.

Question. Can β„• be proved to be 𝟚-injective unconditionally? Or does
the 𝟚-injectivity of β„• give a cotaboo such as the above Brouwerian assumption?

Notice also that a map X β†’ β„• can be seen as a partition of X by
countably many clopens. Hence asking β„• to be 𝟚-injective amounts to
saying that from the ability to extend clopens along j : X β†’ Y, we
should be able to extend countable clopen partitions to countable
clopen partitions along j.