Martin Escardo, 23rd August 2023.

Some counterexamples to injectivity.

We already know that if excluded middle holds then all pointed types
are algebraically injective, and that the converse also holds.

So we can't really give an example of any type which is not
algebraically injective, other than the empty type. The best we can
hope for is to derive a constructive taboo, rather than a
contradiction, from the assumption that a type of interest would be
injective.

Most types one encounters in practice are "not" injective in the above
sense. We can also say "not all types are injective in general", as
there are some ∞-toposes which do satisfy excluded middle, as well as
some ∞-toposes which don't, and we intend TypeTopology to apply to all
∞-toposes, except when special assumptions are made.

NB. We work with the assumption of algebraic injectivity, rather than
its truncated version (injectivity), but this doesn't matter because
most of our conclusions are propositions, and when they are not we can
consider their truncations, which are also constructive taboos.

More counter-examples are in the module InjectiveTypes.Resizing and in
the module InjectiveTypes.InhabitedTypesTaboo.

\begin{code}

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

open import UF.Univalence
open import UF.PropTrunc

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

open PropositionalTruncation pt

open import MLTT.Spartan
open import UF.Embeddings
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.Retracts
open import UF.Size
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
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 Taboos.Decomposability fe
open import InjectiveTypes.Blackboard fe
open import TypeTopology.SimpleTypes fe pt

\end{code}

The two-point type 𝟚 is not injective in general. It is algebraically
injective if and only if weak excluded middle holds.

\begin{code}

𝟚-ainjective-gives-WEM : ainjective-type 𝟚 𝓀 π“₯ β†’ typal-WEM 𝓀
𝟚-ainjective-gives-WEM {𝓀} 𝟚-ainj = I
 where
  d : decomposition 𝟚
  d = id , (β‚€ , refl) , (₁ , refl)

  I : typal-WEM 𝓀
  I = decomposition-of-ainjective-type-gives-WEM pe' 𝟚 𝟚-ainj d

WEM-gives-𝟚-retract-of-Ξ© : typal-WEM 𝓀 β†’ retract 𝟚 of Ξ© 𝓀
WEM-gives-𝟚-retract-of-Ξ© {𝓀} wem = II
 where
  h : (p : Ξ© 𝓀) β†’ is-decidable (Β¬ (p holds)) β†’ 𝟚
  h p (inl _) = β‚€
  h p (inr _) = ₁

  Ξ©-to-𝟚 : Ξ© 𝓀 β†’ 𝟚
  Ω-to-𝟚 p = h p (wem (p holds))

  I : (n : 𝟚) (d : is-decidable (Β¬ (𝟚-to-Ξ© n holds))) β†’ h (𝟚-to-Ξ© n) d ＝ n
  I β‚€ (inl Ο•) = refl
  I ₁ (inl Ο•) = 𝟘-elim (Ο• ⋆)
  I β‚€ (inr ψ) = 𝟘-elim (ψ unique-from-𝟘)
  I ₁ (inr ψ) = refl

  d : (p : Ξ© 𝓀) β†’ is-decidable (Β¬ (p holds))
  d p = wem (p holds)

  II : retract 𝟚 of (Ξ© 𝓀)
  II = (Ξ» p β†’ h p (d p)) ,
       𝟚-to-Ω ,
       (Ξ» n β†’ I n (d (𝟚-to-Ξ© n)))

WEM-gives-𝟚-ainjective : typal-WEM 𝓀 β†’ ainjective-type 𝟚 𝓀 𝓀
WEM-gives-𝟚-ainjective {𝓀} wem =
 retract-of-ainjective 𝟚 (Ξ© 𝓀) (Ξ©-ainjective pe') (WEM-gives-𝟚-retract-of-Ξ© wem)

WEM-gives-𝟚-aflabby : typal-WEM 𝓀 β†’ aflabby 𝟚 𝓀
WEM-gives-𝟚-aflabby wem = ainjective-types-are-aflabby 𝟚 (WEM-gives-𝟚-ainjective wem)

\end{code}

The simple types are not injective in general. These are the types
formed by starting with β„• and closing under function types. We can
also add the type 𝟚 to the base case of the definition to get the same
conclusion.

\begin{code}

simple-typeβ‚‚-injective-gives-WEM : (X : 𝓀₀ Μ‡)
                                 β†’ simple-typeβ‚‚ X
                                 β†’ ainjective-type X 𝓀 𝓀
                                 β†’ typal-WEM 𝓀
simple-typeβ‚‚-injective-gives-WEM X s X-ainj =
 𝟚-ainjective-gives-WEM
  (retract-of-ainjective 𝟚 X X-ainj
  (simple-typesβ‚‚-disconnected s))

simple-typeβ‚‚-injective-gives-WEM-examples
 : (ainjective-type β„•                   𝓀 𝓀 β†’ typal-WEM 𝓀)
 Γ— (ainjective-type (β„• β†’ β„•)             𝓀 𝓀 β†’ typal-WEM 𝓀)
 Γ— (ainjective-type (β„• β†’ 𝟚)             𝓀 𝓀 β†’ typal-WEM 𝓀)
 Γ— (ainjective-type ((β„• β†’ β„•) β†’ β„•)       𝓀 𝓀 β†’ typal-WEM 𝓀)
 Γ— (ainjective-type ((β„• β†’ 𝟚) β†’ β„•)       𝓀 𝓀 β†’ typal-WEM 𝓀)
 Γ— (ainjective-type (((β„• β†’ β„•) β†’ β„•) β†’ β„•) 𝓀 𝓀 β†’ typal-WEM 𝓀)
simple-typeβ‚‚-injective-gives-WEM-examples =
 simple-typeβ‚‚-injective-gives-WEM _ base ,
 simple-typeβ‚‚-injective-gives-WEM _ (step base base) ,
 simple-typeβ‚‚-injective-gives-WEM _ (step base baseβ‚‚) ,
 simple-typeβ‚‚-injective-gives-WEM _ (step (step base base) base) ,
 simple-typeβ‚‚-injective-gives-WEM _ (step (step base baseβ‚‚) base) ,
 simple-typeβ‚‚-injective-gives-WEM _ (step (step (step base base) base) base)

\end{code}

TODO. More generally, if a non-trivial totally separated type is
injective, then WEM holds.

TODO. We can also close under _Γ—_ and _+_ to get the same result. We
can also close under Ξ , but maybe not under Ξ£.

If the type ℝ of Dedekind reals is injective then there are
discontinuous functions ℝ β†’ ℝ, e.g. the Heaviside function, which is
also a constructive taboo. Notice that the type ℝ lives in the
universe 𝓀₁.

\begin{code}

open import DedekindReals.Type fe' pe' pt
open import DedekindReals.Order fe' pe' pt renaming (_β™―_ to _♯ℝ_)
open import Notation.Order

ℝ-ainjective-gives-Heaviside-function : ainjective-type ℝ 𝓀₁ 𝓀₁
                                      β†’ Ξ£ H κž‰ (ℝ β†’ ℝ) ,
                                            ((x : ℝ) β†’ (x < 0ℝ β†’ H x ＝ 0ℝ)
                                                     Γ— (x β‰₯ 0ℝ β†’ H x ＝ 1ℝ))
ℝ-ainjective-gives-Heaviside-function ℝ-ainj = H , Ξ³
 where
  j : (Ξ£ x κž‰ ℝ , x < 0ℝ) + (Ξ£ x κž‰ ℝ , x β‰₯ 0ℝ) β†’ ℝ
  j = cases pr₁ pr₁

  j-is-embedding : is-embedding j
  j-is-embedding = disjoint-cases-embedding pr₁ pr₁
                    (pr₁-is-embedding (Ξ» x β†’ <-is-prop x 0ℝ))
                    (pr₁-is-embedding (Ξ» x β†’ ≀-is-prop 0ℝ x))
                    d
   where
    d : disjoint-images pr₁ pr₁
    d (x , l) (x , b) refl = <ℝ-irreflexive x (ℝ<-≀-trans x 0ℝ x l b)

  h : (Ξ£ x κž‰ ℝ , x < 0ℝ) + (Ξ£ x κž‰ ℝ , x β‰₯ 0ℝ) β†’ ℝ
  h = cases (Ξ» _ β†’ 0ℝ) (Ξ» _ β†’ 1ℝ)

  H : ℝ β†’ ℝ
  H = pr₁ (ℝ-ainj j j-is-embedding h)

  H-extends-h-along-j : βˆ€ u β†’ H (j u) ＝ h u
  H-extends-h-along-j = prβ‚‚ (ℝ-ainj j j-is-embedding h)

  Ξ³ : (x : ℝ) β†’ (x < 0ℝ β†’ H x ＝ 0ℝ)
              Γ— (x β‰₯ 0ℝ β†’ H x ＝ 1ℝ)
  Ξ³ x = I , II
   where
    I : x < 0ℝ β†’ H x ＝ 0ℝ
    I l = H-extends-h-along-j (inl (x , l))

    II : x β‰₯ 0ℝ β†’ H x ＝ 1ℝ
    II b = H-extends-h-along-j (inr (x , b))

\end{code}

But we can do better than that and derive weak excluded middle from
the injectivity of ℝ.

\begin{code}

open import Rationals.Type
open import Rationals.Order

ℝ-ainjective-gives-WEM : ainjective-type ℝ 𝓀 π“₯ β†’ typal-WEM 𝓀
ℝ-ainjective-gives-WEM {𝓀} ℝ-ainj = WEM-gives-typal-WEM fe' XI
 where
  module _ (P : 𝓀 Μ‡ ) (P-is-prop : is-prop P) where

   q : Ξ© 𝓀
   q = (P + Β¬ P) , decidability-of-prop-is-prop fe' P-is-prop

   ℝ-aflabby : aflabby ℝ 𝓀
   ℝ-aflabby = ainjective-types-are-aflabby ℝ ℝ-ainj

   f : P + Β¬ P β†’ ℝ
   f = cases (Ξ» _ β†’ 0ℝ) (Ξ» _ β†’ 1ℝ)

   r : ℝ
   r = aflabby-extension ℝ-aflabby q f

   I : P β†’ r ＝ 0ℝ
   I p = aflabby-extension-property ℝ-aflabby q f (inl p)

   II : Β¬ P β†’ r ＝ 1ℝ
   II Ξ½ = aflabby-extension-property ℝ-aflabby q f (inr Ξ½)

   I-II : r β‰  0ℝ β†’ r β‰  1ℝ β†’ 𝟘
   I-II u v = contrapositive II v (contrapositive I u)

   I-IIβ‚€ : r β‰  1ℝ β†’ r ＝ 0ℝ
   I-IIβ‚€ v = ℝ-is-¬¬-separated r 0ℝ (Ξ» u β†’ I-II u v)

   I-II₁ : r β‰  0ℝ β†’ r ＝ 1ℝ
   I-II₁ u = ℝ-is-¬¬-separated r 1ℝ (I-II u)

   III : (1/4 < r) ∨ (r < 1/2)
   III = ℝ-locatedness r 1/4 1/2 1/4<1/2

   IV : 1/4 < r β†’ r ＝ 1ℝ
   IV l = I-II₁ IVβ‚€
    where
      IVβ‚€ : r β‰  0ℝ
      IVβ‚€ e = β„š<-irrefl 1/4 IVβ‚‚
       where
        IV₁ : 1/4 < 0ℝ
        IV₁ = transport (1/4 <_) e l
        IVβ‚‚ : 1/4 < 1/4
        IVβ‚‚ = β„š<-trans 1/4 0β„š 1/4 IV₁ 0<1/4

   V : r < 1/2 β†’ r ＝ 0ℝ
   V l = I-IIβ‚€ Vβ‚€
    where
      Vβ‚€ : r β‰  1ℝ
      Vβ‚€ e = β„š<-irrefl 1/2 Vβ‚‚
       where
        V₁ : 1ℝ < 1/2
        V₁ = transport (_< 1/2) e l
        Vβ‚‚ : 1/2 < 1/2
        Vβ‚‚ = β„š<-trans 1/2 1β„š 1/2 1/2<1 V₁

   VI : r ＝ 0ℝ β†’ ¬¬ P
   VI e Ξ½ = apartness-gives-inequality 0ℝ 1ℝ
             ℝ-zero-apart-from-one
              (0ℝ ＝⟨ e ⁻¹ ⟩
               r  ＝⟨ II ν ⟩
               1ℝ ∎)

   VII : r ＝ 1ℝ β†’ Β¬ P
   VII e p = apartness-gives-inequality 0ℝ 1ℝ
              ℝ-zero-apart-from-one
              (0ℝ ＝⟨ (I p)⁻¹ ⟩
              r   ＝⟨ e ⟩
              1ℝ  ∎)

   VIII : r < 1/2 β†’ ¬¬ P
   VIII l = VI (V l)

   IX :  1/4 β„š<ℝ r β†’ Β¬ P
   IX l = VII (IV l)

   X : ¬ P ∨ ¬¬ P
   X = ∨-functor IX VIII III

   XI : ¬ P + ¬¬ P
   XI = exit-βˆ₯βˆ₯ (decidability-of-prop-is-prop fe' (negations-are-props fe')) X

\end{code}

TODO. Probably the converse holds.

The injectivity of β„•βˆž, the conatural numbers, or generic convergent
sequence, gives WLPO. Like in the previous example, we first use
injectivity to define a non-continuous function.

\begin{code}

open import CoNaturals.Type
open import Taboos.BasicDiscontinuity (fe 𝓀₀ 𝓀₀)
open import Taboos.WLPO
open import Notation.CanonicalMap

β„•βˆž-injective-gives-WLPO : ainjective-type β„•βˆž 𝓀₀ 𝓀₀ β†’ WLPO
β„•βˆž-injective-gives-WLPO β„•βˆž-ainj = basic-discontinuity-taboo' f (fβ‚€ , f₁)
 where
  g : β„• + πŸ™ β†’ β„•βˆž
  g (inl _) = ΞΉ 0
  g (inr _) = ΞΉ 1

  f : β„•βˆž β†’ β„•βˆž
  f = pr₁ (β„•βˆž-ainj ΞΉπŸ™ (ΞΉπŸ™-is-embedding fe') g)

  f-extends-g-along-ΞΉπŸ™ : βˆ€ u β†’ f (ΞΉπŸ™ u) ＝ g u
  f-extends-g-along-ΞΉπŸ™ = prβ‚‚ (β„•βˆž-ainj ΞΉπŸ™ (ΞΉπŸ™-is-embedding fe') g)

  fβ‚€ : (n : β„•) β†’ f (ΞΉ n) ＝ ΞΉ 0
  fβ‚€ n = f-extends-g-along-ΞΉπŸ™ (inl n)

  f₁ : f ∞ ＝ ΞΉ 1
  f₁ = f-extends-g-along-ΞΉπŸ™ (inr ⋆)

\end{code}

The above again illustrates that we can use injectivity to define
discontinuous functions. But we can actually get a stronger
conclusion with a weaker assumption and a simpler proof.

\begin{code}

β„•βˆž-injective-gives-WEM : ainjective-type β„•βˆž 𝓀 π“₯ β†’ typal-WEM 𝓀
β„•βˆž-injective-gives-WEM β„•βˆž-ainj =
 𝟚-ainjective-gives-WEM (retract-of-ainjective 𝟚 β„•βˆž β„•βˆž-ainj 𝟚-retract-of-β„•βˆž)

\end{code}

Added 6 June 2024 by Tom de Jong during a meeting with MartΓ­n EscardΓ³.

A type with a nontrivial apartness relation cannot be injective unless weak
excluded middle holds.

TODO. We could derive ℝ-ainjective-gives-WEM from the below. (Note the
      similarities in the two proofs.)

\begin{code}

open import Apartness.Definition
open import Apartness.Properties pt
open Apartness pt

ainjective-type-with-non-trivial-apartness-gives-WEM
 : {X : 𝓀 Μ‡ }
 β†’ ainjective-type X 𝓣 𝓦
 β†’ Nontrivial-Apartness X π“₯
 β†’ typal-WEM 𝓣
ainjective-type-with-non-trivial-apartness-gives-WEM
 {𝓀} {𝓣} {𝓦} {π“₯} {X} ainj ((_β™―_ , Ξ±) , ((xβ‚€ , x₁) , points-apart))
 = WEM-gives-typal-WEM fe' VII
  where
   module _ (P : 𝓣 Μ‡ ) (P-is-prop : is-prop P) where

    X-aflabby : aflabby X 𝓣
    X-aflabby = ainjective-types-are-aflabby _ ainj

    f : (P + Β¬ P) β†’ X
    f = cases (Ξ» _ β†’ xβ‚€) (Ξ» _ β†’ x₁)

    q : Ξ© 𝓣
    q = (P + Β¬ P) , decidability-of-prop-is-prop fe' P-is-prop

    x : X
    x = aflabby-extension X-aflabby q f

    I : P β†’ x ＝ xβ‚€
    I p = aflabby-extension-property X-aflabby q f (inl p)

    II : Β¬ P β†’ x ＝ x₁
    II Ξ½ = aflabby-extension-property X-aflabby q f (inr Ξ½)

    III : x β‰  xβ‚€ β†’ Β¬ P
    III = contrapositive I

    IV : x β‰  x₁ β†’ ¬¬ P
    IV = contrapositive II

    V : xβ‚€ β™― x ∨ x₁ β™― x
    V = apartness-is-cotransitive _β™―_ Ξ± xβ‚€ x₁ x points-apart

    VI : (x β‰  xβ‚€) ∨ (x β‰  x₁)
    VI = ∨-functor ν ν V
     where
      Ξ½ : {x y : X} β†’ x β™― y β†’ y β‰  x
      Ξ½ a refl = apartness-is-irreflexive _β™―_ Ξ± _ a

    VII : ¬ P + ¬¬ P
    VII = ∨-elim (decidability-of-prop-is-prop fe' (negations-are-props fe'))
                 (inl ∘ III) (inr ∘ IV) VI

\end{code}

In particular, we have the following.

\begin{code}

non-trivial-apartness-on-universe-gives-WEM
 : is-univalent (𝓀 βŠ” π“₯)
 β†’ Nontrivial-Apartness (𝓀 βŠ” π“₯ Μ‡ ) π“₯
 β†’ typal-WEM 𝓀
non-trivial-apartness-on-universe-gives-WEM ua =
 ainjective-type-with-non-trivial-apartness-gives-WEM
  (universes-are-ainjective ua)

non-trivial-apartness-on-universe-iff-WEM
 : is-univalent 𝓀
 β†’ Nontrivial-Apartness (𝓀 Μ‡ ) 𝓀 ↔ typal-WEM 𝓀
non-trivial-apartness-on-universe-iff-WEM {𝓀} ua = f , g
 where
  f : Nontrivial-Apartness (𝓀 Μ‡ ) 𝓀 β†’ typal-WEM 𝓀
  f = non-trivial-apartness-on-universe-gives-WEM ua

  g : typal-WEM 𝓀 β†’ Nontrivial-Apartness (𝓀 Μ‡ ) 𝓀
  g = WEM-gives-that-type-with-two-distinct-points-has-nontrivial-apartness⁺
       fe'
       (universes-are-locally-small ua)
       universe-has-two-distinct-points

\end{code}

Notice that ainjective-type-with-non-trivial-apartness-gives-WEM
subsumes all the previous examples: the type 𝟚, which is a simple
type, the simple types (because they are totally separated and hence
they have a (tight) apartness), the Dedekind reals (with their
standard apartness), β„•βˆž (again because it is totally
separated).

TODO. Maybe we can list a few more interesting examples?