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, are not injective in general.

    Can the totally separated types 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  #-}

open import UF.FunExt

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

open import MLTT.Spartan
open import TypeTopology.TotallySeparated
open import UF.Embeddings
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)

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

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

K-prod : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ K X Γ— K Y β†’ K (X Γ— Y)
K-prod (Ο• , Ξ³) w = Ο• (Ξ» x β†’ Ξ³ (Ξ» y β†’ w (x , y)))

K-depprod : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ K X β†’ (X β†’ K Y) β†’ K (X Γ— Y)
K-depprod Ο• Ξ³ w = Ο• (Ξ» x β†’ Ξ³ x (Ξ» 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.)

A map j : X β†’ Y is 𝟚-injecting if the type 𝟚 is algebraically
injective with respect to it. We don't require 𝟚-injecting maps to be
embeddings (but see the discussion below).

\begin{code}

𝟚-injecting : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
𝟚-injecting j = (f : domain j β†’ 𝟚) β†’ Ξ£ f' κž‰ (codomain j β†’ 𝟚) , f' ∘ j ∼ f

\end{code}

A type is 𝟚-injective if it is injective over 𝟚-injecting maps.

\begin{code}

𝟚-injective : 𝓦 Μ‡ β†’ (𝓀 π“₯ : Universe) β†’ 𝓦 βŠ” (𝓀 βŠ” π“₯)⁺ Μ‡
𝟚-injective {𝓦} D 𝓀 π“₯ = {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                          (j : X β†’ Y)
                        β†’ 𝟚-injecting j
                        β†’ (f : X β†’ D)
                        β†’ Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ f

\end{code}

We name the two projections `extension` and `extension-property`.

\begin{code}

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

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

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

\end{code}

We'll see below that the extension property really is property, rather
than general data.

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 (D-𝟚-inj i) j j-𝟚-injecting (Ξ» x β†’ f x i) y) ,
 (Ξ» x β†’ dfunext fe'
 (Ξ» i β†’ extension-property (D-𝟚-inj i) j j-𝟚-injecting (Ξ» x β†’ f x i) x))

\end{code}

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

\begin{code}

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

\end{code}

The unit of the monad is 𝟚-injecting.

\begin{code}

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

\end{code}

For future reference, notice that the map Ξ· {𝓀} {X} is not in general
an embedding.

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 η η-𝟚-injecting id ,
 Ξ· ,
 extension-property D-𝟚-inj η η-𝟚-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}

This 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 property really is property, even though the choice of
extension is data.

\begin{code}

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

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

\end{code}

TODO.

  (1) Can we generalize the universes in
      `𝟚-injectives-are-totally-separated` and (hence) 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) Do totally separated types "think that 𝟚-injecting maps are
      embeddings"? Formulate this question precisely, and maybe answer
      it.

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

  (5) 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.