Martin Escardo, 27 April 2014, with later additions, 2017, 2018, 2019.

This is a "blackboard" Agda file, which means that the ideas are
reported in the order they come to mind (with the very bad ideas
deleted, and with some intermediate useful ideas kept, even if they
are not intended to make their way to publication). See the file
InjectiveTypes-article for an organized presentation.

This introduction is incomplete and outdated / obsolete. Much more has
been done since 2014 that is not reported here.

We show that the injective types are the retracts of the exponential
powers of universes, where an exponential power of a type D is a type
of the form A β†’ D for some type A. Injectivity is defined as
(functional) data rather than property.


Injectivity of the universe (2014)
----------------------------

Here we have definitions and proofs in Agda notation, which assume a
univalent mathematics background (e.g. given by the HoTT book),
preceded by informal (rigorous) discussion.

We show that the universe is (pointwise right-Kan) injective wrt
embeddings. An embedding is a map j:X→Y whose fibers are all univalent
propositions.

In the remote past, I looked at injectivity in categories of spaces
and locales, with respect to various kinds of maps, and I wrote
several papers about that.

At present, I am looking at searchable sets in type theory
(corresponding to compact sets in topology), and I accidentally landed
in the same injectivity territory. This file is about
injectivity. Other files make use of this for searchability purposes,
which is not discussed here.

Abstractly, the general situation is

                   j
              X ------> Y
               \       /
                \     /
             f   \   / f/j
                  \ /
                   v
                   D

Given f and j, we want to find f/j making the diagram commute (that
is, f = f/j ∘ j). Of course, this "extension property" is not always
possible, and it depends on properties of f, j and D. Usually, one
requires j to be an embedding (of some sort).

Here I consider the case that D=𝓀, a universe, in which case, if one
doesn't want to assume univalence, then it makes sense to consider
commutation up to equivalence:

                   j
              X ------> Y
               \       /
                \  ≃  /
             f   \   / f/j
                  \ /
                   v
                   𝓀

But this can be the case only if j is an embedding in a suitable
sense. Otherwise, we only have a right-Kan extension

                   j
              X ------> Y
               \       /
                \  ≳  /
             f   \   / f/j
                  \ /
                   v
                   𝓀

in the sense that the type of natural transformations from "presheaves"
g : Y β†’ 𝓀 to the "presheaf" f/j, written

     g β‰Ύ f/j,

is naturally equivalent to the type g∘j β‰Ύ f of natural
transformations from g∘j to f:

     g β‰Ύ f/j ≃ g∘j β‰Ύ f

If j is an embedding (in the sense of univalent mathematics), then,
for any f, we can find f/j which is both a right-Kan extension and a
(proper) extension (up to equivalence).

All this dualizes with Ξ  replaced by Ξ£ and right replaced by left.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline  #-}

open import UF.FunExt

module InjectiveTypes.Blackboard (fe : FunExt) where

open import MLTT.Spartan
open import MLTT.Plus-Properties

open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ExcludedMiddle
open import UF.IdEmbedding
open import UF.Lower-FunExt
open import UF.PairFun
open import UF.PropIndexedPiSigma
open import UF.PropTrunc
open import UF.Retracts
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Univalence
open import UF.UniverseEmbedding

\end{code}

Here is how we define f/j given f and j.

                   j
              X ------> Y
               \       /
                \  ≳  /
             f   \   / f/j
                  \ /
                   v
                   𝓀

We have to apply the following constructions for 𝓀=π“₯=𝓦 for the above
triangles to make sense.

We rename the type of natural transformations:

\begin{code}

_β‰Ύ_ : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ (X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
_β‰Ύ_ = Nat

_β‰Ύ_-explicitly : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
               β†’ A β‰Ύ B ＝ ((x : X) β†’ A x β†’ B x)
_β‰Ύ_-explicitly A B = refl

\end{code}

We think of A and B as some sort ∞-presheaves, with the category of
sets replaced by a universe of ∞-groupoids.

Natural transformations are automatically natural: for all x,y: A and
p : x ＝ y,

                        Ο„ x
               A x --------------β†’ B x
                |                   |
                |                   |
           A[p] |                   | B[p]
                |                   |
                |                   |
                ↓                   ↓
               A y --------------β†’ B y
                        Ο„ y

\begin{code}

β‰Ύ-naturality : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ ) (Ο„ : A β‰Ύ B)
             β†’ {x y : X} (p : x ＝ y) β†’ Ο„ y ∘ transport A p ＝ transport B p ∘ Ο„ x
β‰Ύ-naturality = Nats-are-natural

\end{code}

We now work with the following assumptions:

\begin{code}

module _ {X : 𝓀 Μ‡ }
         {Y : π“₯ Μ‡ }
         (f : X β†’ 𝓦 Μ‡ )
         (j : X β†’ Y)
       where

  Ξ -extension Ξ£-extension : Y β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
  Ξ -extension y = Ξ  (x , _) κž‰ fiber j y , f x
  Ξ£-extension y = Ξ£ (x , _) κž‰ fiber j y , f x

  private
   f/j fβˆ–j : Y β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
   f/j = Ξ -extension
   fβˆ–j = Ξ£-extension

  Ξ£β†’Ξ  : is-embedding j β†’ fβˆ–j β‰Ύ f/j
  Ξ£β†’Ξ  e y ((x , p) , B) (x' , p') = transport f (embeddings-are-lc j e (p βˆ™ p' ⁻¹)) B

\end{code}

  The natural transformation Ξ£β†’Ξ  j itself should be a natural
  embedding (conjectural conjecture).

\begin{code}

  Ξ·Ξ  : f/j ∘ j β‰Ύ f
  Ξ·Ξ  x C = C (x , refl)

  Ξ·Ξ£ : f β‰Ύ fβˆ–j ∘ j
  Ξ·Ξ£ x B = (x , refl) , B

\end{code}

  For arbitrary j:X→Y, this gives Kan extensions in the following
  sense:

\begin{code}

  Ξ -extension-right-Kan : (g : Y β†’ 𝓣 Μ‡ ) β†’ (g β‰Ύ f/j) ≃  (g ∘ j β‰Ύ f)
  Ξ -extension-right-Kan {𝓣} g = qinveq (ψ g) (Ο† g , Ο†Οˆ' g , ΟˆΟ†' g)
   where
    Ο† : (g : Y β†’ 𝓣 Μ‡ ) β†’ g ∘ j β‰Ύ f β†’ g β‰Ύ f/j
    Ο† g Ξ· y C (x , p) = Ξ· x (transport⁻¹ g p C)

    ψ : (g : Y β†’ 𝓣 Μ‡ ) β†’ g β‰Ύ f/j β†’ g ∘ j β‰Ύ f
    ψ g θ x C = θ (j x) C (x , refl)

    ΟˆΟ† : (g : Y β†’ 𝓣 Μ‡ ) (Ξ· : g ∘ j β‰Ύ f) (x : X) (C : g (j x)) β†’ ψ g (Ο† g Ξ·) x C ＝ Ξ· x C
    ΟˆΟ† g Ξ· x C = refl

    ΟˆΟ†' : (g : Y β†’ 𝓣 Μ‡ ) (Ξ· : g ∘ j β‰Ύ f) β†’ ψ g (Ο† g Ξ·) ＝ Ξ·
    ΟˆΟ†' g Ξ· = dfunext (fe 𝓀 (𝓦 βŠ” 𝓣)) (Ξ» x β†’ dfunext (fe 𝓣 𝓦) (ΟˆΟ† g Ξ· x))

    Ο†Οˆ : (g : Y β†’ 𝓣 Μ‡ ) (ΞΈ : g β‰Ύ f/j) (y : Y) (C : g y) (w : fiber j y) β†’ Ο† g (ψ g ΞΈ) y C w ＝ ΞΈ y C w
    Ο†Οˆ g ΞΈ y C (x , refl) = refl

    Ο†Οˆ' : (g : Y β†’ 𝓣 Μ‡ ) (ΞΈ : g β‰Ύ f/j) β†’ Ο† g (ψ g ΞΈ) ＝ ΞΈ
    Ο†Οˆ' g ΞΈ = dfunext (fe π“₯ (𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓣)) (Ξ» y β†’ dfunext (fe 𝓣 (𝓀 βŠ” π“₯ βŠ” 𝓦)) (Ξ» C β†’ dfunext (fe (𝓀 βŠ” π“₯) 𝓦) (Ο†Οˆ g ΞΈ y C)))

  Ξ£-extension-left-Kan : (g : Y β†’ 𝓣 Μ‡ ) β†’ (fβˆ–j β‰Ύ g) ≃ (f β‰Ύ g ∘ j)
  Ξ£-extension-left-Kan {𝓣} g = e
   where
    Ο† : (g : Y β†’ 𝓣 Μ‡ ) β†’ f β‰Ύ g ∘ j β†’ fβˆ–j β‰Ύ g
    Ο† g Ξ· y ((x , p) , C) = transport g p (Ξ· x C)

    ψ : (g : Y β†’ 𝓣 Μ‡ ) β†’ fβˆ–j β‰Ύ g β†’ f β‰Ύ g ∘ j
    ψ g θ x B = θ (j x) ((x , refl) , B)

    Ο†Οˆ : (g : Y β†’ 𝓣 Μ‡ ) (ΞΈ : fβˆ–j β‰Ύ g) (y : Y) (B : fβˆ–j y) β†’ Ο† g (ψ g ΞΈ) y B ＝ ΞΈ y B
    Ο†Οˆ g ΞΈ y ((x , refl) , B) = refl

    ΟˆΟ† : (g : Y β†’ 𝓣 Μ‡ ) (Ξ· : f β‰Ύ g ∘ j) (x : X) (B : f x) β†’ ψ g (Ο† g Ξ·) x B ＝ Ξ· x B
    ΟˆΟ† g Ξ· x B = refl

    e : fβˆ–j β‰Ύ g ≃ f β‰Ύ g ∘ j
    e = ψ g , (Ο† g , Ξ» Ξ· β†’ dfunext (fe 𝓀 (𝓦 βŠ” 𝓣)) (Ξ» x β†’ dfunext (fe 𝓦 𝓣) (Ξ» B β†’ ΟˆΟ† g Ξ· x B)))
            , (Ο† g , Ξ» ΞΈ β†’ dfunext (fe π“₯ (𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓣)) (Ξ» y β†’ dfunext (fe (𝓀 βŠ” π“₯ βŠ” 𝓦) 𝓣) (Ξ» C β†’ Ο†Οˆ g ΞΈ y C)))

\end{code}

  Conjectural conjecture: the type

    Ξ£ (f' : Y β†’ 𝓀), Ξ  (g : Y β†’ 𝓀), g β‰Ύ f' ≃ g∘j β‰Ύ f

  should be contractible assuming univalence. Similarly for left Kan
  extensions as discussed below.

  The above formula actually give extensions up to pointwise
  equivalence if j:X→Y is an embedding in the sense of univalent
  mathematics.

\begin{code}

  Ξ -extension-property : is-embedding j β†’ (x : X) β†’ f/j (j x) ≃ f x
  Ξ -extension-property e x = prop-indexed-product (fe (𝓀 βŠ” π“₯) 𝓦)
                              {fiber j (j x)} {Ξ» (z : fiber j (j x)) β†’ f (fiber-point z)}
                              (e (j x))
                              (x , refl)

  Ξ -extension-equivalence : is-embedding j β†’ (x : X) β†’ is-equiv (Ξ -proj (x , refl))
  Ξ -extension-equivalence e x = prβ‚‚ (Ξ -extension-property e x)

  Ξ -extension-out-of-range : βˆ€ {𝓦} (y : Y) β†’ ((x : X) β†’ j x β‰  y) β†’ f/j (y) ≃ πŸ™ {𝓦}
  Ξ -extension-out-of-range y Ο† = prop-indexed-product-one (fe (𝓀 βŠ” π“₯) 𝓦) (uncurry Ο†)

  Ξ£-extension-property : is-embedding j β†’ (x : X) β†’ fβˆ–j (j x) ≃ f x
  Ξ£-extension-property e x = prop-indexed-sum (e (j x)) (x , refl)

  Ξ£-extension-out-of-range : (y : Y) β†’ ((x : X) β†’ j x β‰  y) β†’ fβˆ–j (y) ≃ 𝟘 {𝓦}
  Ξ£-extension-out-of-range y Ο† = prop-indexed-sum-zero (uncurry Ο†)

\end{code}

  We now rewrite the Ξ -extension formula in an equivalent way:

\begin{code}

  2nd-Ξ -extension-formula : (y : Y) β†’ f/j (y) ≃ (Ξ  x κž‰ X , (j x ＝ y β†’ f x))
  2nd-Ξ -extension-formula y = curry-uncurry fe

  2nd-Ξ -extension-formula' : (y : Y) β†’ f/j (y) ≃ (Ξ» x β†’ j x ＝ y) β‰Ύ f
  2nd-Ξ -extension-formula' = 2nd-Ξ -extension-formula

  2nd-Ξ£-extension-formula : (y : Y) β†’ fβˆ–j (y) ≃ (Ξ£ x κž‰ X , (j x ＝ y) Γ— f x)
  2nd-Ξ£-extension-formula y = Ξ£-assoc


\end{code}

  This is the Ξ -extension formula we actually used for (1) showing that
  the universe is indiscrete, and (2) defining the squashed sum and
  proving that it preserves searchability.

\begin{code}

  Ξ -observation : is-embedding j β†’ (a : X) β†’ f a ≃ (Ξ  x κž‰ X , (j x ＝ j a β†’ f x))
  Ξ -observation e a = ≃-sym ((≃-sym (2nd-Ξ -extension-formula (j a))) ●
                                      (Ξ -extension-property e a))

  Ξ£-observation : is-embedding j β†’ (a : X) β†’ f a ≃ (Ξ£ x κž‰ X , (j x ＝ j a) Γ— f x)
  Ξ£-observation e a = ≃-sym ((≃-sym (2nd-Ξ£-extension-formula (j a))) ●
                                      (Ξ£-extension-property e a))

\end{code}

Added December 2017:

The extensions f/j and fβˆ–j have the same product and sum as f
respectively:

\begin{code}

  same-Ξ  : Ξ  f ≃ Ξ  f/j
  same-Ξ  = F , (G , FG) , (G , GF)
    where
      F : Ξ  f β†’ Ξ  f/j
      F Ο† y (x , p) = Ο† x

      G : Ξ  f/j β†’ Ξ  f
      G ψ x = ψ (j x) (x , refl)

      FG' : (ψ : Ξ  f/j) (y : Y) (Οƒ : fiber j y) β†’ F (G ψ) y Οƒ ＝ ψ y Οƒ
      FG' ψ x (_ , refl) = refl

      FG : (ψ : Ξ  f/j) β†’ F (G ψ) ＝ ψ
      FG ψ = dfunext (fe π“₯ (𝓀 βŠ” π“₯ βŠ” 𝓦)) (Ξ» y β†’ dfunext (fe (𝓀 βŠ” π“₯) 𝓦) (FG' ψ y))

      GF : (Ο† : Ξ  f) β†’ G (F Ο†) ＝ Ο†
      GF Ο† = refl

  same-Ξ£ : Ξ£ f ≃ Ξ£ fβˆ–j
  same-Ξ£ = F , (G , FG) , (G , GF)
    where
      F : Ξ£ f β†’ Ξ£ fβˆ–j
      F (x , y) = (j x , (x , refl) , y)

      G : Ξ£ fβˆ–j β†’ Ξ£ f
      G (y , (x , p) , y') = (x , y')

      FG : (Οƒ : Ξ£ fβˆ–j) β†’ F (G Οƒ) ＝ Οƒ
      FG (x , (_ , refl) , y') = refl

      GF : (Οƒ : Ξ£ f) β†’ G (F Οƒ) ＝ Οƒ
      GF (x , y) = refl

\end{code}

We now introduce the notations f / j and f βˆ– j for the Ξ - and
Ξ£-extensions, outside the above anonymous module.

\begin{code}

_/_ _βˆ–_ :  {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
        β†’ (X β†’ 𝓦 Μ‡ ) β†’ (X β†’ Y) β†’ (Y β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡ )
f / j = Ξ -extension f j
f βˆ– j = Ξ£-extension f j

infix 7 _/_

\end{code}

Also added December 2017.

A different notation reflects a different view of these processes:

\begin{code}

inverse-image : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
              β†’ (X β†’ Y) β†’ (Y β†’ 𝓦 Μ‡ ) β†’ (X β†’ 𝓦 Μ‡ )
inverse-image f v = v ∘ f


Ξ -image Ξ£-image : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                β†’ (X β†’ Y)
                β†’ ((X β†’ 𝓦 Μ‡ ) β†’ (Y β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡ ))
Ξ -image j = Ξ» f β†’ Ξ -extension f j

Ξ£-image j = Ξ» f β†’ Ξ£-extension f j

\end{code}

Ξ£-images of singletons. Another way to see the following is with the
function same-Ξ£ defined above. This and univalence give

 Ξ£ (Id x) ＝ Ξ£ (Id x βˆ– j) = Ξ£-image j (Id x)

Hence

 is-singleton (Σ (Id x)) ＝ is-singleton (Σ-image j (Id x))

But the lhs holds, and hence is-singleton (Ξ£-image j (Id x)).

\begin{code}

Ξ£-image-of-singleton-lemma : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (j : X β†’ Y) (x : X) (y : Y)
                           β†’ Ξ£-image j (Id x) y ≃ Id (j x) y
Ξ£-image-of-singleton-lemma {𝓀} {π“₯} {X} {Y} j x y = (f , (g , fg) , (g , gf))
 where
  f : Ξ£-image j (Id x) y β†’ Id (j x) y
  f ((x , refl) , refl) = refl

  g : Id (j x) y β†’ Ξ£-image j (Id x) y
  g refl = (x , refl) , refl

  gf : (i : Ξ£-image j (Id x) y) β†’ g (f i) ＝ i
  gf ((x , refl) , refl) = refl

  fg : (p : Id (j x) y) β†’ f (g p) ＝ p
  fg refl = refl

Ξ£-image-of-singleton-lemma' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (j : X β†’ Y) (x : X) (y : Y)
                            β†’ (((Id x) βˆ– j) y) ≃ (j x ＝ y)
Ξ£-image-of-singleton-lemma' = Ξ£-image-of-singleton-lemma

Ξ£-image-of-singleton : {X Y : 𝓀 Μ‡ }
                     β†’ is-univalent 𝓀
                     β†’ (j : X β†’ Y) (x : X) β†’ Ξ£-image j (Id x) ＝ Id (j x)
Ξ£-image-of-singleton {𝓀} {X} {Y} ua j x = b
  where
   a : (y : Y) β†’ Ξ£-image j (Id x) y ＝ Id (j x) y
   a y = eqtoid ua (Ξ£-image j (Id x) y) (Id (j x) y) (Ξ£-image-of-singleton-lemma j x y)

   b : Σ-image j (Id x) ＝ Id (j x)
   b = dfunext (fe 𝓀 (𝓀 ⁺)) a

Ξ£-image-of-singleton' : {X Y : 𝓀 Μ‡ }
                      β†’ is-univalent 𝓀
                      β†’ (j : X β†’ Y) (x : X) β†’ (Id x) βˆ– j ＝ Id (j x)
Ξ£-image-of-singleton' = Ξ£-image-of-singleton

\end{code}

There is more to do about this.

\begin{code}

Ξ -extension-is-extension : is-univalent (𝓀 βŠ” π“₯) β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y)
                         β†’ is-embedding j
                         β†’ (f : X β†’ 𝓀 βŠ” π“₯ Μ‡ ) β†’ (f / j) ∘ j ∼ f
Ξ -extension-is-extension ua j e f x = eqtoid ua _ _ (Ξ -extension-property f j e x)

Ξ -extension-is-extension' : is-univalent (𝓀 βŠ” π“₯) β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
                          β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y)
                          β†’ is-embedding j
                          β†’ (f : X β†’ 𝓀 βŠ” π“₯ Μ‡ ) β†’ (f / j) ∘ j ＝ f
Ξ -extension-is-extension' ua fe j e f = dfunext fe (Ξ -extension-is-extension ua j e f)

Ξ -extension-is-extension'' : is-univalent (𝓀 βŠ” π“₯)
                           β†’ funext ((𝓀 βŠ” π“₯)⁺) ((𝓀 βŠ” π“₯)⁺)
                           β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y)
                           β†’ is-embedding j
                           β†’ (Ξ» f β†’ (f / j) ∘ j) ＝ id
Ξ -extension-is-extension'' {𝓀} {π“₯} ua fe j e = dfunext fe (Ξ -extension-is-extension' ua (lower-fun-ext 𝓀 fe) j e)

Ξ£-extension-is-extension : is-univalent (𝓀 βŠ” π“₯) β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y)
                         β†’ is-embedding j
                         β†’ (f : X β†’ 𝓀 βŠ” π“₯ Μ‡ ) β†’ (f βˆ– j) ∘ j ∼ f
Ξ£-extension-is-extension ua j e f x = eqtoid ua _ _ (Ξ£-extension-property f j e x)

Ξ£-extension-is-extension' : is-univalent (𝓀 βŠ” π“₯)
                          β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
                          β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y)
                          β†’ is-embedding j
                          β†’ (f : X β†’ 𝓀 βŠ” π“₯ Μ‡ ) β†’ (f βˆ– j) ∘ j ＝ f
Ξ£-extension-is-extension' ua fe j e f = dfunext fe (Ξ£-extension-is-extension ua j e f)

Ξ£-extension-is-extension'' : is-univalent (𝓀 βŠ” π“₯)
                           β†’ funext ((𝓀 βŠ” π“₯)⁺) ((𝓀 βŠ” π“₯)⁺)
                           β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y)
                           β†’ is-embedding j
                           β†’ (Ξ» f β†’ (f βˆ– j) ∘ j) ＝ id
Ξ£-extension-is-extension'' {𝓀} {π“₯} ua fe j e = dfunext fe
                                                 (Ξ£-extension-is-extension' ua
                                                   (lower-fun-ext 𝓀 fe) j e)
\end{code}

We now consider injectivity, defined with Ξ£ rather than βˆƒ (that is, as
data rather than property), called algebraic injectivity.

\begin{code}

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

embedding-retract : (D : 𝓦 Μ‡ ) (Y : π“₯ Μ‡ ) (j : D β†’ Y)
                  β†’ is-embedding j
                  β†’ ainjective-type D 𝓦 π“₯
                  β†’ retract D of Y
embedding-retract D Y j e i = pr₁ a , j , prβ‚‚ a
 where
  a : Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ id
  a = i j e id

retract-of-ainjective : (D' : 𝓦' Μ‡ ) (D : 𝓦 Μ‡ )
                      β†’ ainjective-type D 𝓀 π“₯
                      β†’ retract D' of D
                      β†’ ainjective-type D' 𝓀 π“₯
retract-of-ainjective 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))

equiv-to-ainjective : (D' : 𝓦' Μ‡ ) (D : 𝓦 Μ‡ )
                    β†’ ainjective-type D 𝓀 π“₯
                    β†’ D' ≃ D
                    β†’ ainjective-type D' 𝓀 π“₯
equiv-to-ainjective D' D i e = retract-of-ainjective D' D i (≃-gives-◁ e)

universes-are-ainjective-Ξ  : is-univalent (𝓀 βŠ” π“₯) β†’ ainjective-type (𝓀 βŠ” π“₯ Μ‡ ) 𝓀 π“₯
universes-are-ainjective-Ξ  ua j e f = f / j , Ξ -extension-is-extension ua j e f

universes-are-ainjective-Ξ ' : is-univalent 𝓀 β†’ ainjective-type (𝓀 Μ‡ ) 𝓀 𝓀
universes-are-ainjective-Ξ ' = universes-are-ainjective-Ξ 

universes-are-ainjective-Ξ£ : is-univalent (𝓀 βŠ” π“₯)
                           β†’ ainjective-type (𝓀 βŠ” π“₯ Μ‡ ) 𝓀 π“₯
universes-are-ainjective-Ξ£ ua j e f = f βˆ– j ,
                                      (Ξ» x β†’ eqtoid ua _ _ (Ξ£-extension-property f j e x))

ainjective-is-retract-of-power-of-universe : (D : 𝓀 Μ‡ ) β†’ is-univalent 𝓀
                                           β†’ ainjective-type D 𝓀  (𝓀 ⁺)
                                           β†’ retract D of (D β†’ 𝓀 Μ‡ )
ainjective-is-retract-of-power-of-universe {𝓀} D ua = embedding-retract D (D β†’ 𝓀 Μ‡ ) Id (UA-Id-embedding ua fe)

Ξ -ainjective : {A : 𝓣 Μ‡ } {D : A β†’ 𝓦 Μ‡ }
             β†’ ((a : A) β†’ ainjective-type (D a) 𝓀 π“₯)
             β†’ ainjective-type (Ξ  D) 𝓀 π“₯
Ξ -ainjective {𝓣}  {𝓦} {𝓀} {π“₯} {A} {D} i {X} {Y} j e f = f' , g
  where
    l : (a : A) β†’ Ξ£ h κž‰ (Y β†’ D a) , h ∘ j ∼ (Ξ» x β†’ f x a)
    l a = (i a) j e (Ξ» x β†’ f x a)

    f' : Y β†’ (a : A) β†’ D a
    f' y a = pr₁ (l a) y

    g : f' ∘ j ∼ f
    g x = dfunext (fe 𝓣 𝓦) (Ξ» a β†’ prβ‚‚ (l a) x)

power-of-ainjective : {A : 𝓣 Μ‡ } {D : 𝓦 Μ‡ }
                    β†’ ainjective-type D 𝓀 π“₯
                    β†’ ainjective-type (A β†’ D) 𝓀 π“₯
power-of-ainjective i = Ξ -ainjective (Ξ» a β†’ i)

\end{code}

The following is the first of a number of injectivity resizing
constructions:

\begin{code}

ainjective-resizingβ‚€ : is-univalent 𝓀
                     β†’ (D : 𝓀 Μ‡ ) β†’ ainjective-type D 𝓀 (𝓀 ⁺) β†’ ainjective-type D 𝓀 𝓀
ainjective-resizingβ‚€ {𝓀} ua D i = Ο† (ainjective-is-retract-of-power-of-universe D ua i)
 where
  Ο† : retract D of (D β†’ 𝓀 Μ‡ ) β†’ ainjective-type D 𝓀 𝓀
  Ο† = retract-of-ainjective D (D β†’ 𝓀 Μ‡ )
       (power-of-ainjective (universes-are-ainjective-Ξ  ua))

\end{code}

Propositional resizing gives a much more general injectivity resizing
(see below).

Added 18th July 2018. Notice that the function e : X β†’ Y doesn't need
to be an embedding and that the proof is completely routine.

\begin{code}

retract-extension : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : X β†’ 𝓦 Μ‡ ) (B : X β†’ 𝓣 Μ‡ ) (e : X β†’ Y)
                  β†’ ((x : X) β†’ retract (A x) of (B x))
                  β†’ ((y : Y) β†’ retract ((A / e) y) of ((B / e) y))
retract-extension {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} A B e ρ y = r , s , rs
 where
  R : (x : X) β†’ B x β†’ A x
  R x = retraction (ρ x)

  S : (x : X) β†’ A x β†’ B x
  S x = section (ρ x)

  RS : (x : X) (a : A x) β†’ R x (S x a) ＝ a
  RS x = retract-condition (ρ x)

  r : (B / e) y β†’ (A / e) y
  r v (x , p) = R x (v (x , p))

  s : (A / e) y β†’ (B / e) y
  s u (x , p) = S x (u (x , p))

  h : (u : (A / e) y) (Οƒ : fiber e y) β†’ r (s u) Οƒ ＝ u Οƒ
  h u (x , p) = RS x (u (x , p))

  rs : (u : (A / e) y) β†’ r (s u) ＝ u
  rs u = dfunext (fe (𝓀 βŠ” π“₯) 𝓦) (h u)

\end{code}

Added 25th July 2018.

\begin{code}

iterated-extension : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } {A : X β†’ 𝓣 Μ‡ }
                     (j : X β†’ Y) (k : Y β†’ Z)
                   β†’ (z : Z) β†’ ((A / j) / k) z ≃ (A / (k ∘ j)) z
iterated-extension {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} {Z} {A} j k z = Ξ³
 where
  f : ((A / j) / k) z β†’ (A / (k ∘ j)) z
  f u (x , p) = u (j x , p) (x , refl)

  g : (A / (k ∘ j)) z β†’ ((A / j) / k) z
  g v (.(j x) , q) (x , refl) = v (x , q)

  fg : (v : (A / (k ∘ j)) z) β†’ f (g v) ＝ v
  fg v = refl

  gf' : (u : ((A / j) / k) z) (w : fiber k z) (t : fiber j (fiber-point w))
      β†’ g (f u) w t ＝ u w t
  gf' u (.(j x) , q) (x , refl) = refl

  gf : (u : ((A / j) / k) z) β†’ g (f u) ＝ u
  gf u = dfunext (fe (π“₯ βŠ” 𝓦) (𝓀 βŠ” π“₯ βŠ” 𝓣))
          (Ξ» w β†’ dfunext (fe (𝓀 βŠ” π“₯) 𝓣) (gf' u w))

  Ξ³ : ((A / j) / k) z ≃ (A / (k ∘ j)) z
  Ξ³ = f , ((g , fg) , (g , gf))

\end{code}

Added 9th November 2018.

We want to show that f ↦ f/j is an embedding of (X β†’ 𝓀) into (Y β†’ 𝓀)
if j is an embedding.

                   j
              X ------> Y
               \       /
                \     /
             f   \   / f/j
                  \ /
                   v
                   𝓀

The simplest case is X = P and Y = πŸ™, where P is a proposition. Then
the map P β†’ πŸ™ is an embedding.

                   j
              P ------> πŸ™
               \       /
                \     /
              f  \   / (f / j) (x) = Ξ  (w : fiber j x) β†’ f (fiber-point w)
                  \ /              ≃ Ξ  (p : P) β†’ j p ＝ x β†’ f p
                   v               ≃ Ξ  (p : P) β†’ f p
                   𝓀

So in essence we are considering the map s : (P β†’ 𝓀) β†’ 𝓀 defined by

   s f = Ξ  (p : P) β†’ f p.

Then, for any X : 𝓀,

  fiber s X = Ξ£ f κž‰ P β†’ 𝓀 , (Ξ  (p : P) β†’ f p) ＝ X.

A few days pause. Now 15th Nov 2018 after a discussion in the HoTT list.
https://groups.google.com/d/topic/homotopytypetheory/xvx5hOEPnDs/discussion

Here is my take on the outcome of the discussion, following
independent solutions by Shulman and Capriotti.

\begin{code}

module /-extension-is-embedding-special-case
         (P : 𝓀 Μ‡ )
         (i : is-prop P)
         (fe' : funext 𝓀 (𝓀 ⁺))
         (ua : is-univalent 𝓀)
       where

 open import UF.Equiv-FunExt
 open import UF.UA-FunExt

 feuu : funext 𝓀 𝓀
 feuu = univalence-gives-funext ua

 r :  𝓀 Μ‡ β†’ (P β†’ 𝓀 Μ‡ )
 r X p = X

 s : (P β†’ 𝓀 Μ‡ ) β†’ 𝓀 Μ‡
 s = Ξ 

 rs : βˆ€ A β†’ r (s A) ＝ A
 rs A = dfunext fe' (Ξ» p β†’ eqtoid ua (s A) (A p) (prop-indexed-product feuu i p))

 sr : βˆ€ X β†’ s (r X) ＝ (P β†’ X)
 sr X = refl

 ΞΊ : (X : 𝓀 Μ‡ ) β†’ X β†’ s (r X)
 ΞΊ X x p = x

 M : 𝓀 ⁺ Μ‡
 M = Ξ£ X κž‰ 𝓀 Μ‡ , is-equiv (ΞΊ X)

 Ο† : (P β†’ 𝓀 Μ‡ ) β†’ M
 Ο† A = s A , qinvs-are-equivs (ΞΊ (s A)) (Ξ΄ , Ξ΅ , Ξ·)
  where
   Ξ΄ : (P β†’ s A) β†’ s A
   Ξ΄ v p = v p p

   Ξ· : (v : P β†’ s A) β†’ ΞΊ (s A) (Ξ΄ v) ＝ v
   Ξ· v = dfunext feuu (Ξ» p β†’ dfunext feuu (Ξ» q β†’ ap (Ξ» - β†’ v - q) (i q p)))

   Ξ΅ : (u : Ξ  A) β†’ Ξ΄ (ΞΊ (s A) u) ＝ u
   Ξ΅ u = refl

 Ξ³ : M β†’ (P β†’ 𝓀 Μ‡ )
 Ξ³ (X , i) = r X

 φγ : (m : M) β†’ Ο† (Ξ³ m) ＝ m
 φγ (X , i) = to-Ξ£-＝ (eqtoid ua (P β†’ X) X (≃-sym (ΞΊ X , i)) ,
                      being-equiv-is-prop fe (ΞΊ X) _ i)

 Ξ³Ο† : (A : P β†’ 𝓀 Μ‡ ) β†’ Ξ³ (Ο† A) ＝ A
 Ξ³Ο† = rs

 Ο†-is-equiv : is-equiv Ο†
 Ο†-is-equiv = qinvs-are-equivs Ο† (Ξ³ , Ξ³Ο† , φγ)

 Ο†-is-embedding : is-embedding Ο†
 Ο†-is-embedding = equivs-are-embeddings Ο† Ο†-is-equiv

 ψ : M β†’ 𝓀 Μ‡
 ψ = pr₁

 ψ-is-embedding : is-embedding ψ
 ψ-is-embedding = pr₁-is-embedding (Ξ» X β†’ being-equiv-is-prop fe (ΞΊ X))

 s-is-comp : s ＝ ψ ∘ Ο†
 s-is-comp = refl

 s-is-embedding : is-embedding s
 s-is-embedding = ∘-is-embedding Ο†-is-embedding ψ-is-embedding

\end{code}

Also 15th Nov 2018. We have a dual situation:

\begin{code}

module βˆ–-extension-is-embedding-special-case
         (P : 𝓀 Μ‡ )
         (i : is-prop P)
         (fe' : funext 𝓀 (𝓀 ⁺))
         (ua : is-univalent 𝓀)
       where

 open import UF.PropIndexedPiSigma
 open import UF.Equiv-FunExt

 s : (P β†’ 𝓀 Μ‡ ) β†’ 𝓀 Μ‡
 s = Ξ£

 r :  𝓀 Μ‡ β†’ (P β†’ 𝓀 Μ‡ )
 r X p = X

 rs : βˆ€ A β†’ r (s A) ＝ A
 rs A = dfunext fe' (Ξ» p β†’ eqtoid ua (Ξ£ A) (A p) (prop-indexed-sum i p))

 sr : βˆ€ X β†’ s (r X) ＝ P Γ— X
 sr X = refl

 ΞΊ : (X : 𝓀 Μ‡ ) β†’ s (r X) β†’ X
 ΞΊ X = prβ‚‚

 C : 𝓀 ⁺ Μ‡
 C = Ξ£ X κž‰ 𝓀 Μ‡ , is-equiv (ΞΊ X)

 Ο† : (P β†’ 𝓀 Μ‡ ) β†’ C
 Ο† A = s A , qinvs-are-equivs (ΞΊ (s A)) (Ξ΄ , Ξ΅ , Ξ·)
  where
   Ξ΄ : s A β†’ P Γ— s A
   Ξ΄ (p , a) = p , p , a

   Ξ· : (Οƒ : s A) β†’ ΞΊ (s A) (Ξ΄ Οƒ) ＝ Οƒ
   Ξ· Οƒ = refl

   Ξ΅ : (Ο„ : P Γ— s A) β†’ Ξ΄ (ΞΊ (s A) Ο„) ＝ Ο„
   Ξ΅ (p , q , a) = to-Γ—-＝ (i q p) refl

 Ξ³ : C β†’ (P β†’ 𝓀 Μ‡ )
 Ξ³ (X , i) = r X

 φγ : (c : C) β†’ Ο† (Ξ³ c) ＝ c
 φγ (X , i) = to-Ξ£-＝ (eqtoid ua (P Γ— X) X (ΞΊ X , i) ,
                     (being-equiv-is-prop fe (ΞΊ X) _ i))

 Ξ³Ο† : (A : P β†’ 𝓀 Μ‡ ) β†’ Ξ³ (Ο† A) ＝ A
 Ξ³Ο† = rs

 Ο†-is-equiv : is-equiv Ο†
 Ο†-is-equiv = qinvs-are-equivs Ο† (Ξ³ , Ξ³Ο† , φγ)

 Ο†-is-embedding : is-embedding Ο†
 Ο†-is-embedding = equivs-are-embeddings Ο† Ο†-is-equiv

 ψ : C β†’ 𝓀 Μ‡
 ψ = pr₁

 ψ-is-embedding : is-embedding ψ
 ψ-is-embedding = pr₁-is-embedding (Ξ» X β†’ being-equiv-is-prop fe (ΞΊ X))

 s-is-comp : s ＝ ψ ∘ Ο†
 s-is-comp = refl

 s-is-embedding : is-embedding s
 s-is-embedding = ∘-is-embedding Ο†-is-embedding ψ-is-embedding

\end{code}

Added 20th November 2018.

\begin{code}

module /-extension-is-embedding
         (X Y : 𝓀 Μ‡ )
         (j : X β†’ Y)
         (i : is-embedding j)
         (fe' : funext 𝓀 (𝓀 ⁺))
         (ua : is-univalent 𝓀)
       where

 open import UF.PropIndexedPiSigma
 open import UF.Equiv-FunExt
 open import UF.Subsingletons-FunExt
 open import UF.UA-FunExt

 feuu : funext 𝓀 𝓀
 feuu = univalence-gives-funext ua

 s : (X β†’ 𝓀 Μ‡ ) β†’ (Y β†’ 𝓀 Μ‡ )
 s f = f / j

 r : (Y β†’ 𝓀 Μ‡ ) β†’ (X β†’ 𝓀 Μ‡ )
 r g = g ∘ j

 rs : βˆ€ f β†’ r (s f) ＝ f
 rs = Ξ -extension-is-extension' ua fe' j i

 sr : βˆ€ g β†’ s (r g) ＝ (g ∘ j) / j
 sr g = refl

 ΞΊ : (g : Y β†’ 𝓀 Μ‡ ) β†’ g β‰Ύ s (r g)
 κ g y C (x , p) = transport⁻¹ g p C

 M : (𝓀 ⁺) Μ‡
 M = Ξ£ g κž‰ (Y β†’ 𝓀 Μ‡ ), ((y : Y) β†’ is-equiv (ΞΊ g y))

 Ο† : (X β†’ 𝓀 Μ‡ ) β†’ M
 Ο† f = s f , e
  where
   e : (y : Y) β†’ is-equiv (ΞΊ (s f) y)
   e y = qinvs-are-equivs (ΞΊ (s f) y) (Ξ΄ , Ξ΅ , Ξ·)
    where
     Ξ΄ : (((f / j) ∘ j) / j) y β†’ (f / j) y
     Ξ΄ C (x , p) = C (x , p) (x , refl)

     Ξ· : (C : ((f / j ∘ j) / j) y) β†’ ΞΊ (s f) y (Ξ΄ C) ＝ C
     Ξ· C = dfunext feuu g
      where
       g : (w : fiber j y) β†’ ΞΊ (s f) y (Ξ΄ C) w ＝ C w
       g (x , refl) = dfunext feuu h
        where
         h : (t : fiber j (j x)) β†’ C t (pr₁ t , refl) ＝ C (x , refl) t
         h (x' , p') = transport (Ξ» - β†’ C - (pr₁ - , refl) ＝ C (x , refl) -) q refl
          where
           q : (x , refl) ＝ (x' , p')
           q = i (j x) (x , refl) (x' , p')

     Ξ΅ : (a : (f / j) y) β†’ Ξ΄ (ΞΊ (s f) y a) ＝ a
     Ξ΅ a = dfunext feuu g
      where
       g : (w : fiber j y) β†’ Ξ΄ (ΞΊ (s f) y a) w ＝ a w
       g (x , refl) = refl

 Ξ³ : M β†’ (X β†’ 𝓀 Μ‡ )
 Ξ³ (g , e) = r g

 φγ : βˆ€ m β†’ Ο† (Ξ³ m) ＝ m
 φγ (g , e) = to-Ξ£-＝
               (dfunext fe' (Ξ» y β†’ eqtoid ua (s (r g) y) (g y) (≃-sym (ΞΊ g y , e y))) ,
                Ξ -is-prop feuu (Ξ» y β†’ being-equiv-is-prop'' feuu (ΞΊ g y)) _ e)

 Ξ³Ο† : βˆ€ f β†’ Ξ³ (Ο† f) ＝ f
 Ξ³Ο† = rs

 Ο†-is-equiv : is-equiv Ο†
 Ο†-is-equiv = qinvs-are-equivs Ο† (Ξ³ , Ξ³Ο† , φγ)

 Ο†-is-embedding : is-embedding Ο†
 Ο†-is-embedding = equivs-are-embeddings Ο† Ο†-is-equiv

 ψ : M β†’ (Y β†’ 𝓀 Μ‡ )
 ψ = pr₁

 ψ-is-embedding : is-embedding ψ
 ψ-is-embedding = pr₁-is-embedding (Ξ» g β†’ Ξ -is-prop feuu (Ξ» y β†’ being-equiv-is-prop'' feuu (ΞΊ g y)))

 s-is-comp : s ＝ ψ ∘ Ο†
 s-is-comp = refl

 s-is-embedding : is-embedding s
 s-is-embedding = ∘-is-embedding Ο†-is-embedding ψ-is-embedding

\end{code}

Added 21th November 2018.

\begin{code}

module βˆ–-extension-is-embedding
         (X Y : 𝓀 Μ‡ )
         (j : X β†’ Y)
         (i : is-embedding j)
         (fe' : funext 𝓀 (𝓀 ⁺))
         (ua : is-univalent 𝓀)
       where

 open import UF.PropIndexedPiSigma
 open import UF.Equiv-FunExt
 open import UF.Subsingletons-FunExt
 open import UF.UA-FunExt

 feuu : funext 𝓀 𝓀
 feuu = univalence-gives-funext ua

 s : (X β†’ 𝓀 Μ‡ ) β†’ (Y β†’ 𝓀 Μ‡ )
 s f = f βˆ– j

 r : (Y β†’ 𝓀 Μ‡ ) β†’ (X β†’ 𝓀 Μ‡ )
 r g = g ∘ j

 rs : βˆ€ f β†’ r (s f) ＝ f
 rs = Ξ£-extension-is-extension' ua fe' j i

 sr : βˆ€ g β†’ s (r g) ＝ (g ∘ j) βˆ– j
 sr g = refl

 ΞΊ : (g : Y β†’ 𝓀 Μ‡ ) β†’ s (r g) β‰Ύ g
 ΞΊ g y ((x , p) , C) = transport g p C

 M : (𝓀 ⁺) Μ‡
 M = Ξ£ g κž‰ (Y β†’ 𝓀 Μ‡ ), ((y : Y) β†’ is-equiv (ΞΊ g y))

 Ο† : (X β†’ 𝓀 Μ‡ ) β†’ M
 Ο† f = s f , e
  where
   e : (y : Y) β†’ is-equiv (ΞΊ (s f) y)
   e y = qinvs-are-equivs (ΞΊ (s f) y) (Ξ΄ , Ξ΅ , Ξ·)
    where
     Ξ΄ : (Ξ£ (x , _) κž‰ fiber j y , f x)
       β†’ Ξ£ t κž‰ fiber j y , Ξ£ (x , _) κž‰ fiber j (j (pr₁ t)), f x
     Ξ΄ ((x , p) , C) = (x , p) , (x , refl) , C

     Ξ· : (Οƒ : s f y) β†’ ΞΊ (s f) y (Ξ΄ Οƒ) ＝ Οƒ
     Ξ· ((x , refl) , C) = refl

     Ξ΅ : (Ο„ : Ξ£ (Ξ» w β†’ r (s f) (pr₁ w))) β†’ Ξ΄ (ΞΊ (s f) y Ο„) ＝ Ο„
     Ξ΅ ((x , refl) , (x' , p') , C) = t x x' (pa x' x p') p' C (appa x x' p')
      where
        t : (x x' : X) (u : x' ＝ x) (p : j x' ＝ j x) (C : f x') β†’ (ap j u ＝ p) β†’
            ((x' , p)    , (x' , refl) , C)
          ＝ (((x  , refl) , (x' , p)    , C) ∢ (Ξ£ (x , _) κž‰  fiber j (j x) , r (s f) x))
        t x .x refl p C refl = refl

        ej' : βˆ€ x x' β†’ qinv (ap j {x} {x'})
        ej' x x' = equivs-are-qinvs (ap j) (embedding-embedding' j i x x')

        pa : βˆ€ x x' β†’ j x ＝ j x' β†’ x ＝ x'
        pa x x' = pr₁ (ej' x x')

        appa : βˆ€ x x' p' β†’ ap j (pa x' x p') ＝ p'
        appa x x' = prβ‚‚ (prβ‚‚ (ej' x' x))

 Ξ³ : M β†’ (X β†’ 𝓀 Μ‡ )
 Ξ³ (g , e) = r g

 φγ : βˆ€ m β†’ Ο† (Ξ³ m) ＝ m
 φγ (g , e) = to-Ξ£-＝
               (dfunext fe' (Ξ» y β†’ eqtoid ua (s (r g) y) (g y) (ΞΊ g y , e y)) ,
                Ξ -is-prop feuu (Ξ» y β†’ being-equiv-is-prop'' feuu (ΞΊ g y)) _ e)

 Ξ³Ο† : βˆ€ f β†’ Ξ³ (Ο† f) ＝ f
 Ξ³Ο† = rs

 Ο†-is-equiv : is-equiv Ο†
 Ο†-is-equiv = qinvs-are-equivs Ο† (Ξ³ , Ξ³Ο† , φγ)

 Ο†-is-embedding : is-embedding Ο†
 Ο†-is-embedding = equivs-are-embeddings Ο† Ο†-is-equiv

 ψ : M β†’ (Y β†’ 𝓀 Μ‡ )
 ψ = pr₁

 ψ-is-embedding : is-embedding ψ
 ψ-is-embedding = pr₁-is-embedding
                     (Ξ» g β†’ Ξ -is-prop feuu (Ξ» y β†’ being-equiv-is-prop'' feuu (ΞΊ g y)))

 s-is-comp : s ＝ ψ ∘ Ο†
 s-is-comp = refl

 s-is-embedding : is-embedding s
 s-is-embedding = ∘-is-embedding Ο†-is-embedding ψ-is-embedding

\end{code}

Added 23rd Nov 2018, version of 21st January 2017:

The notion of flabbiness used in topos theory is defined with
truncated Ξ£, that is, βˆƒ. We refer to the notion defined with Ξ£ as
algebraic flabbiness.

\begin{code}

aflabby : 𝓦 Μ‡ β†’ (𝓀 : Universe) β†’ 𝓦 βŠ” 𝓀 ⁺ Μ‡
aflabby D 𝓀 = (P : 𝓀 Μ‡ ) β†’ is-prop P β†’ (f : P β†’ D) β†’ Ξ£ d κž‰ D , ((p : P) β†’ d ＝ f p)

aflabby-pointed : (D : 𝓦 Μ‡ ) β†’ aflabby D 𝓀 β†’ D
aflabby-pointed D Ο† = pr₁ (Ο† 𝟘 𝟘-is-prop unique-from-𝟘)


ainjective-types-are-aflabby : (D : 𝓦 Μ‡ ) β†’ ainjective-type D 𝓀 π“₯ β†’ aflabby D 𝓀
ainjective-types-are-aflabby {𝓦} {𝓀} {π“₯} D i P isp f =
  pr₁ (i (Ξ» p β†’ ⋆) (prop-embedding P isp π“₯) f) ⋆ ,
  prβ‚‚ (i (Ξ» p β†’ ⋆) (prop-embedding P isp π“₯) f)

aflabby-types-are-ainjective : (D : 𝓦 Μ‡ ) β†’ aflabby D (𝓀 βŠ” π“₯) β†’ ainjective-type D 𝓀 π“₯
aflabby-types-are-ainjective D Ο† {X} {Y} j e f = f' , p
 where
  f' : Y β†’ D
  f' y = pr₁ (Ο† (fiber j y) (e y) (f ∘ pr₁))

  p : (x : X) β†’ f' (j x) ＝ f x
  p x = q (x , refl)
   where
    q : (w : fiber j (j x)) β†’ f' (j x) ＝ f (pr₁ w)
    q = prβ‚‚ (Ο† (fiber j (j x)) (e (j x)) (f ∘ pr₁))

\end{code}

Because Ξ© is a retract of 𝓀 via propositional truncation, it is
injective. But we can prove this directly without assumming
propositional truncations, and propositional and functional
extensionality (which give to propositional univalence) are enough,
whereas the injectivity of the universe requires full univalence.

\begin{code}

Ξ©-aflabby : propext (𝓀 βŠ” π“₯) β†’ aflabby (Ξ© (𝓀 βŠ” π“₯)) 𝓀
Ξ©-aflabby {𝓀} {π“₯} pe P i f = (Q , j) , c
 where
  Q : 𝓀 βŠ” π“₯ Μ‡
  Q = (p : P) β†’ f p holds
  j : is-prop Q
  j = Ξ -is-prop (fe 𝓀 (𝓀 βŠ” π“₯)) (Ξ» p β†’ holds-is-prop (f p))
  c : (p : P) β†’ Q , j ＝ f p
  c p = to-Ξ£-＝ (t , being-prop-is-prop (fe (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)) _ _)
   where
      g : Q β†’ f p holds
      g q = q p

      h : f p holds β†’ Q
      h r p' = transport (Ξ» - β†’ f - holds) (i p p') r

      t : Q ＝ f p holds
      t = pe j (holds-is-prop (f p)) g h

Ξ©-ainjective : propext (𝓀 βŠ” π“₯) β†’ ainjective-type (Ξ© (𝓀 βŠ” π“₯)) 𝓀 π“₯
Ξ©-ainjective {𝓀} {π“₯} pe = aflabby-types-are-ainjective (Ξ© (𝓀 βŠ” π“₯)) (Ξ©-aflabby {𝓀 βŠ” π“₯} {𝓀} pe)

\end{code}

Added 6th Feb 2019.

The injectivity of all types is logically equivalent to excluded middle
(even though excluded middle is a proposition but injectivity is data):

\begin{code}

EM-gives-pointed-types-aflabby : (D : 𝓦 Μ‡ ) β†’ EM 𝓀 β†’ D β†’ aflabby D 𝓀
EM-gives-pointed-types-aflabby {𝓦} {𝓀} D em d P i f = h (em P i)
 where
  h : P + Β¬ P β†’ Ξ£ d κž‰ D , ((p : P) β†’ d ＝ f p)
  h (inl p) = f p , (Ξ» q β†’ ap f (i p q))
  h (inr n) = d , (Ξ» p β†’ 𝟘-elim (n p))

aflabby-EM-lemma : (P : 𝓦 Μ‡ ) β†’ is-prop P β†’ aflabby ((P + Β¬ P) + πŸ™) 𝓦 β†’ P + Β¬ P
aflabby-EM-lemma {𝓦} P i Ο† = Ξ³
 where
  D = (P + Β¬ P) + πŸ™ {𝓦}

  f : P + Β¬ P β†’ D
  f (inl p) = inl (inl p)
  f (inr n) = inl (inr n)

  d : D
  d = pr₁ (Ο† (P + Β¬ P) (decidability-of-prop-is-prop (fe 𝓦 𝓀₀) i) f)

  ΞΊ : (z : P + Β¬ P) β†’ d ＝ f z
  ΞΊ = prβ‚‚ (Ο† (P + Β¬ P) (decidability-of-prop-is-prop (fe 𝓦 𝓀₀) i) f)

  a : (p : P) β†’ d ＝ inl (inl p)
  a p = ΞΊ (inl p)

  b : (n : Β¬ P) β†’ d ＝ inl (inr n)
  b n = ΞΊ (inr n)

  Ξ΄ : (d' : D) β†’ d ＝ d' β†’ P + Β¬ P
  Ξ΄ (inl (inl p)) r = inl p
  Ξ΄ (inl (inr n)) r = inr n
  Ξ΄ (inr ⋆)       r = 𝟘-elim (m n)
   where
    n : Β¬ P
    n p = 𝟘-elim (+disjoint ((a p)⁻¹ βˆ™ r))

    m : ¬¬ P
    m n = 𝟘-elim (+disjoint ((b n)⁻¹ βˆ™ r))

  Ξ³ : P + Β¬ P
  Ξ³ = Ξ΄ d refl

pointed-types-aflabby-gives-EM : ((D : 𝓦 Μ‡ ) β†’ D β†’ aflabby D 𝓦) β†’ EM 𝓦
pointed-types-aflabby-gives-EM {𝓦} Ξ± P i = aflabby-EM-lemma P i (Ξ± ((P + Β¬ P) + πŸ™) (inr ⋆))

EM-gives-pointed-types-ainjective : EM (𝓀 βŠ” π“₯) β†’ (D : 𝓦 Μ‡ ) β†’ D β†’ ainjective-type D 𝓀 π“₯
EM-gives-pointed-types-ainjective em D d = aflabby-types-are-ainjective D
                                            (EM-gives-pointed-types-aflabby D em d)

pointed-types-ainjective-gives-EM : ((D : 𝓦 Μ‡ ) β†’ D β†’ ainjective-type D 𝓦 𝓀) β†’ EM 𝓦
pointed-types-ainjective-gives-EM Ξ± = pointed-types-aflabby-gives-EM
                                       (Ξ» D d β†’ ainjective-types-are-aflabby D (Ξ± D d))

\end{code}

End of 6th Feb addition. But this is not the end of the story. What
happens with anonymous injectivity (defined and studied below)?

TODO. Show that the extension induced by aflabbiness is an embedding of
function types.

Without resizing axioms, we have the following resizing construction:

\begin{code}

ainjective-resizing₁ : (D : 𝓦 Μ‡ ) β†’ ainjective-type D (𝓀 βŠ” 𝓣) π“₯ β†’ ainjective-type D 𝓀 𝓣
ainjective-resizing₁ D i j e f = aflabby-types-are-ainjective D
                                  (ainjective-types-are-aflabby D i) j e f

\end{code}

In particular:

\begin{code}

ainjective-resizingβ‚‚ : (D : 𝓦 Μ‡ ) β†’ ainjective-type D 𝓀 π“₯ β†’ ainjective-type D 𝓀 𝓀
ainjective-resizingβ‚‚ = ainjective-resizing₁

ainjective-resizing₃ : (D : 𝓦 Μ‡ ) β†’ ainjective-type D 𝓀 π“₯ β†’ ainjective-type D 𝓀₀ 𝓀
ainjective-resizing₃ = ainjective-resizing₁

\end{code}

Added 24th January 2019.

With propositional resizing, as soon as D is aflabby with respect to
some universe, it is aflabby with respect to all universes:

\begin{code}

aflabbiness-resizing : (D : 𝓦 Μ‡ ) (𝓀 π“₯ : Universe)
                     β†’ propositional-resizing 𝓀 π“₯
                     β†’ aflabby D π“₯ β†’ aflabby D 𝓀
aflabbiness-resizing D 𝓀 π“₯ R Ο† P i f = d , h
 where
  Q : π“₯ Μ‡
  Q = resize R P i

  j : is-prop Q
  j = resize-is-prop R P i

  Ξ± : P β†’ Q
  Ξ± = to-resize R P i

  Ξ² : Q β†’ P
  Ξ² = from-resize R P i

  d : D
  d = pr₁ (Ο† Q j (f ∘ Ξ²))

  k : (q : Q) β†’ d ＝ f (Ξ² q)
  k = prβ‚‚ (Ο† Q j (f ∘ Ξ²))

  h : (p : P) β†’ d ＝ f p
  h p = d           ＝⟨ k (α p) ⟩
        f (β (α p)) ＝⟨ ap f (i (β (α p)) p) ⟩
        f p         ∎

\end{code}

And from this it follows that the injectivity of a type with respect
to two given universes implies its injectivity with respect to all
universes:

\begin{code}

ainjective-resizing : βˆ€ {𝓀 π“₯ 𝓀' π“₯' 𝓦}
                    β†’ propositional-resizing (𝓀' βŠ” π“₯') 𝓀
                    β†’ (D : 𝓦 Μ‡ ) β†’ ainjective-type D 𝓀 π“₯ β†’ ainjective-type D 𝓀' π“₯'
ainjective-resizing {𝓀} {π“₯} {𝓀'} {π“₯'} {𝓦} R D i j e f =
  aflabby-types-are-ainjective D
   (aflabbiness-resizing D (𝓀' βŠ” π“₯') 𝓀 R (ainjective-types-are-aflabby D i)) j e f

\end{code}

As an application of this and of injectivity of universes, we have
that any universe is a retract of any larger universe.

We remark that for types that are not sets, sections are not
automatically embeddings (Shulman 2015, https://arxiv.org/abs/1507.03634).

\begin{code}

universe-retract : Univalence
                 β†’ Propositional-resizing
                 β†’ (𝓀 π“₯ : Universe)
                 β†’ Ξ£ ρ κž‰ retract 𝓀 Μ‡ of (𝓀 βŠ” π“₯ Μ‡ ), is-embedding (section ρ)
universe-retract ua R 𝓀 π“₯ = ρ , (Lift-is-embedding ua)
 where
  a : ainjective-type (𝓀 Μ‡ ) 𝓀 𝓀
  a = universes-are-ainjective-Ξ  {𝓀} {𝓀} (ua 𝓀)

  b : is-embedding (Lift π“₯)
    β†’ ainjective-type (𝓀 Μ‡ ) (𝓀 ⁺) ((𝓀 βŠ” π“₯ )⁺)
    β†’ retract 𝓀 Μ‡ of (𝓀 βŠ” π“₯ Μ‡ )
  b = embedding-retract (𝓀 Μ‡ ) (𝓀 βŠ” π“₯ Μ‡ ) (Lift π“₯)

  ρ : retract 𝓀 Μ‡ of (𝓀 βŠ” π“₯ Μ‡ )
  ρ = b (Lift-is-embedding ua) (ainjective-resizing R (𝓀 Μ‡ ) a)

\end{code}

And unfolding of the above construction is in the module UF.Size.

Added 25th January 2019. From this we get the following
characterization of injective types (as a logical equivalence, not a
type equivalence), which can be read as saying that the injective
types in a universe 𝓀 are precisely the retracts of exponential powers
of 𝓀.

\begin{code}

ainjective-characterization : is-univalent 𝓀
                            β†’ propositional-resizing (𝓀 ⁺) 𝓀 β†’ (D : 𝓀 Μ‡ )
                            β†’ ainjective-type D 𝓀 𝓀 ⇔ (Ξ£ X κž‰ 𝓀 Μ‡ , retract D of (X β†’ 𝓀 Μ‡ ))
ainjective-characterization {𝓀} ua R D = a , b
 where
  a : ainjective-type D 𝓀 𝓀 β†’ Ξ£ X κž‰ 𝓀 Μ‡ , retract D of (X β†’ 𝓀 Μ‡ )
  a i = D , d
   where
    c : ainjective-type D 𝓀 (𝓀 ⁺)
    c = ainjective-resizing R D i

    d : retract D of (D β†’ 𝓀 Μ‡ )
    d = ainjective-is-retract-of-power-of-universe D ua c

  b : (Ξ£ X κž‰ 𝓀 Μ‡ , retract D of (X β†’ 𝓀 Μ‡ )) β†’ ainjective-type D 𝓀 𝓀
  b (X , r) = d
   where
    c : ainjective-type (X β†’ 𝓀 Μ‡ ) 𝓀 𝓀
    c = power-of-ainjective (universes-are-ainjective-Ξ£ ua)

    d : ainjective-type D 𝓀 𝓀
    d = retract-of-ainjective D (X β†’ 𝓀 Μ‡ ) c r

\end{code}

Added 23rd January 2019:

\begin{code}

module ainjectivity-of-Lifting (𝓀 : Universe) where

 open import Lifting.Lifting 𝓀 public
 open import Lifting.Algebras 𝓀
 open import Lifting.EmbeddingViaSIP 𝓀 public

 open import UF.UA-FunExt

\end{code}

The underlying types of algebras of the Lifting monad are aflabby, and
hence injective, and so in particular the underlying objects of the
free 𝓛-algebras are injective.

\begin{code}

 𝓛-alg-aflabby : propext 𝓀 β†’ funext 𝓀 𝓀 β†’ funext 𝓀 π“₯
               β†’ {A : π“₯ Μ‡ } β†’ 𝓛-alg A β†’ aflabby A 𝓀
 𝓛-alg-aflabby pe fe fe' (∐ , ΞΊ , ΞΉ) P i f = ∐ i f , Ξ³
  where
   Ξ³ : (p : P) β†’ ∐ i f ＝ f p
   Ξ³ p = 𝓛-alg-Lawβ‚€-givesβ‚€' pe fe fe' ∐ ΞΊ P i f p

 𝓛-alg-ainjective : propext 𝓀
                  β†’ funext 𝓀 𝓀
                  β†’ funext 𝓀 π“₯
                  β†’ (A : π“₯ Μ‡ ) β†’ 𝓛-alg A β†’ ainjective-type A 𝓀 𝓀
 𝓛-alg-ainjective pe fe fe' A Ξ± = aflabby-types-are-ainjective A
                                    (𝓛-alg-aflabby pe fe fe' Ξ±)

 free-𝓛-algebra-ainjective : is-univalent 𝓀
                           β†’ funext 𝓀 (𝓀 ⁺)
                           β†’ (X : 𝓀 Μ‡ ) β†’ ainjective-type (𝓛 X) 𝓀 𝓀
 free-𝓛-algebra-ainjective ua fe X = 𝓛-alg-ainjective
                                       (univalence-gives-propext ua)
                                       (univalence-gives-funext ua)
                                       fe
                                       (𝓛 X)
                                       (𝓛-algebra-gives-alg (free-𝓛-algebra ua X))
\end{code}

Because the unit of the Lifting monad is an embedding, it follows that
injective types are retracts of underlying objects of free algebras:

\begin{code}

 ainjective-is-retract-of-free-𝓛-algebra : (D : 𝓀 Μ‡ )
                                         β†’ is-univalent 𝓀
                                         β†’ ainjective-type D 𝓀 (𝓀 ⁺)
                                         β†’ retract D of (𝓛 D)
 ainjective-is-retract-of-free-𝓛-algebra D ua = embedding-retract D (𝓛 D) Ξ·
                                                  (Ξ·-is-embedding' 𝓀 D ua
                                                     (univalence-gives-funext ua))
\end{code}

With propositional resizing, the injective types are precisely the
retracts of the underlying objects of free algebras of the Lifting
monad:

\begin{code}

 ainjectives-in-terms-of-free-𝓛-algebras : is-univalent 𝓀
                                         β†’ funext 𝓀 (𝓀 ⁺)
                                         β†’ propositional-resizing (𝓀 ⁺) 𝓀
                                         β†’ (D : 𝓀 Μ‡ ) β†’ ainjective-type D 𝓀 𝓀
                                                      ⇔ (Ξ£ X κž‰ 𝓀 Μ‡ , retract D of (𝓛 X))
 ainjectives-in-terms-of-free-𝓛-algebras ua fe R D = a , b
  where
   a : ainjective-type D 𝓀 𝓀 β†’ Ξ£ X κž‰ 𝓀 Μ‡ , retract D of (𝓛 X)
   a i = D , ainjective-is-retract-of-free-𝓛-algebra D ua (ainjective-resizing R D i)

   b : (Ξ£ X κž‰ 𝓀 Μ‡ , retract D of (𝓛 X)) β†’ ainjective-type D 𝓀 𝓀
   b (X , r) = retract-of-ainjective D (𝓛 X) (free-𝓛-algebra-ainjective ua fe X) r

\end{code}

Added 21st January 2019. We now consider injectivity as property
rather than data.

\begin{code}

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

 open PropositionalTruncation pt

 injective-type : 𝓦 Μ‡ β†’ (𝓀 π“₯ : Universe) β†’ 𝓀 ⁺ βŠ” π“₯  ⁺ βŠ” 𝓦 Μ‡
 injective-type D 𝓀 π“₯ = {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (j : X β†’ Y) β†’ is-embedding j
                       β†’ (f : X β†’ D) β†’ βˆƒ g κž‰ (Y β†’ D), g ∘ j ∼ f


 injectivity-is-prop : (D : 𝓦 Μ‡ ) (𝓀 π“₯ : Universe)
                     β†’ is-prop (injective-type D 𝓀 π“₯)
 injectivity-is-prop {𝓦} D 𝓀 π“₯ = Ξ -is-prop' (fe (𝓀 ⁺) (𝓀 βŠ” (π“₯ ⁺) βŠ” 𝓦))
                                        (Ξ» X β†’ Ξ -is-prop' (fe (π“₯ ⁺) (𝓀 βŠ” π“₯ βŠ” 𝓦))
                                          (Ξ» Y β†’ Ξ -is-prop (fe (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯ βŠ” 𝓦))
                                            (Ξ» j β†’ Ξ -is-prop (fe (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯ βŠ” 𝓦))
                                              (Ξ» e β†’ Ξ -is-prop (fe (𝓀 βŠ” 𝓦) (𝓀 βŠ” π“₯ βŠ” 𝓦))
                                                (Ξ» f β†’ βˆ₯βˆ₯-is-prop)))))


 ainjective-gives-injective : (D : 𝓦 Μ‡ ) β†’ ainjective-type D 𝓀 π“₯ β†’ injective-type D 𝓀 π“₯
 ainjective-gives-injective D i j e f = ∣ i j e f ∣

 βˆ₯ainjectiveβˆ₯-gives-injective : (D : 𝓦 Μ‡ )
                              β†’ βˆ₯ ainjective-type D 𝓀 π“₯ βˆ₯
                              β†’ injective-type D 𝓀 π“₯
 βˆ₯ainjectiveβˆ₯-gives-injective {𝓦} {𝓀} {π“₯} D = βˆ₯βˆ₯-rec (injectivity-is-prop D 𝓀 π“₯)
                                                      (ainjective-gives-injective D)

 embedding-βˆ₯retractβˆ₯ : (D : 𝓦 Μ‡ ) (Y : π“₯ Μ‡ ) (j : D β†’ Y)
                     β†’ is-embedding j
                     β†’ injective-type D 𝓦 π“₯
                     β†’ βˆ₯ retract D of Y βˆ₯
 embedding-βˆ₯retractβˆ₯ D Y j e i = βˆ₯βˆ₯-functor Ο† a
  where
   a : βˆƒ r κž‰ (Y β†’ D), r ∘ j ∼ id
   a = i j e id

   Ο† : (Ξ£ r κž‰ (Y β†’ D), r ∘ j ∼ id) β†’ Ξ£ r κž‰ (Y β†’ D) , Ξ£ s κž‰ (D β†’ Y), r ∘ s ∼ id
   Ο† (r , p) = r , j , p

 retract-of-injective : (D' : 𝓀 Μ‡ ) (D : π“₯ Μ‡ )
                       β†’ injective-type D 𝓦 𝓣
                       β†’ retract D' of D
                       β†’ injective-type D' 𝓦 𝓣
 retract-of-injective D' D i (r , (s , rs)) {X} {Y} j e f = Ξ³
  where
   i' : βˆƒ f' κž‰ (Y β†’ D), f' ∘ j ∼ s ∘ f
   i' = 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))

   Ξ³ : βˆƒ f'' κž‰ (Y β†’ D') , f'' ∘ j ∼ f
   Ξ³ = βˆ₯βˆ₯-functor Ο† i'

\end{code}

The given proof of power-of-injective doesn't adapt to the following,
so we need a new proof, but hence also new universe assumptions.

\begin{code}

 power-of-injective : {A : 𝓣 Μ‡ } {D : 𝓣 βŠ” 𝓦 Μ‡ }
                     β†’ injective-type D       (𝓀 βŠ” 𝓣) (π“₯ βŠ” 𝓣)
                     β†’ injective-type (A β†’ D) (𝓀 βŠ” 𝓣) (π“₯ βŠ” 𝓣)
 power-of-injective {𝓣} {𝓦} {𝓀} {π“₯} {A} {D} i {X} {Y} j e f = Ξ³
  where
   g : X Γ— A β†’ D
   g = uncurry f

   k : X Γ— A β†’ Y Γ— A
   k (x , a) = j x , a

   c : is-embedding k
   c = pair-fun-is-embedding j (Ξ» x a β†’ a) e (Ξ» x β†’ id-is-embedding)

   ψ : βˆƒ g' κž‰ (Y Γ— A β†’ D), g' ∘ k ∼ g
   ψ = i k c g

   Ο† : (Ξ£ g' κž‰ (Y Γ— A β†’ D), g' ∘ k ∼ g) β†’ (Ξ£ f' κž‰ (Y β†’ (A β†’ D)), f' ∘ j ∼ f)
   Ο† (g' , h) = curry g' , (Ξ» x β†’ dfunext (fe 𝓣 (𝓣 βŠ” 𝓦)) (Ξ» a β†’ h (x , a)))

   Ξ³ : βˆƒ f' κž‰ (Y β†’ (A β†’ D)), f' ∘ j ∼ f
   Ξ³ = βˆ₯βˆ₯-functor Ο† ψ

 injective-βˆ₯retractβˆ₯-of-power-of-universe : (D : 𝓀 Μ‡ ) β†’ is-univalent 𝓀
                                         β†’ injective-type D 𝓀 (𝓀 ⁺)
                                         β†’ βˆ₯ retract D of (D β†’ 𝓀 Μ‡ ) βˆ₯
 injective-βˆ₯retractβˆ₯-of-power-of-universe {𝓀} D ua = embedding-βˆ₯retractβˆ₯ D (D β†’ 𝓀 Μ‡ ) Id
                                                      (UA-Id-embedding ua fe)

 injective-gives-βˆ₯ainjectiveβˆ₯ : is-univalent 𝓀
                              β†’ (D : 𝓀 Μ‡ )
                              β†’ injective-type D 𝓀 (𝓀 ⁺)
                              β†’ βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯
 injective-gives-βˆ₯ainjectiveβˆ₯ {𝓀} ua D i = Ξ³
  where
   Ο† : retract D of (D β†’ 𝓀 Μ‡ ) β†’ ainjective-type D 𝓀 𝓀
   Ο† = retract-of-ainjective D (D β†’ 𝓀 Μ‡ )
         (power-of-ainjective (universes-are-ainjective-Ξ  ua))

   Ξ³ : βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯
   Ξ³ = βˆ₯βˆ₯-functor Ο† (injective-βˆ₯retractβˆ₯-of-power-of-universe D ua i)

\end{code}

So, in summary, regarding the relationship between winjectivity and
truncated injectivity, so far we know that

  βˆ₯ ainjective-type D 𝓀 π“₯ βˆ₯ β†’ injective-type D 𝓀 π“₯

and

  injective-type D 𝓀 (𝓀 ⁺) β†’ βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯,

and hence, using propositional resizing, we get the following
characterization of a particular case of winjectivity in terms of
injectivity.

\begin{code}

 injectivity-in-terms-of-ainjectivity' : is-univalent 𝓀
                                      β†’ propositional-resizing (𝓀 ⁺) 𝓀
                                      β†’ (D : 𝓀  Μ‡ ) β†’ injective-type D 𝓀 (𝓀 ⁺)
                                                   ⇔ βˆ₯ ainjective-type D 𝓀 (𝓀 ⁺) βˆ₯
 injectivity-in-terms-of-ainjectivity' {𝓀} ua R D = a , b
  where
   a : injective-type D 𝓀 (𝓀 ⁺) β†’ βˆ₯ ainjective-type D 𝓀 (𝓀 ⁺) βˆ₯
   a = βˆ₯βˆ₯-functor (ainjective-resizing R D) ∘ injective-gives-βˆ₯ainjectiveβˆ₯ ua D

   b : βˆ₯ ainjective-type D 𝓀 (𝓀 ⁺) βˆ₯ β†’ injective-type D 𝓀 (𝓀 ⁺)
   b = βˆ₯ainjectiveβˆ₯-gives-injective D

\end{code}

What we really would like to have for D : 𝓀 is

  injective-type D 𝓀 𝓀 ⇔ βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯,

and, perhaps, more generally, also

  injective-type D π“₯ 𝓦 ⇔ βˆ₯ ainjective-type D 𝓀 𝓦 βˆ₯.

This is now answered 8th Feb (see below).

Added 7th Feb 2019. (Preliminary answer.)

However, with Ξ©β‚€-resizing, for a ⋆set⋆ D : 𝓀 we do have

  injective-type D 𝓀 𝓀 ⇔ βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯,

The reason is that the embedding Id : D β†’ (D β†’ 𝓀) factors through
(D β†’ Ξ©β‚€).

\begin{code}

 set-injectivity-in-terms-of-ainjectivity : Ξ©-resizingβ‚€ 𝓀
                                          β†’ PropExt
                                          β†’ (D  : 𝓀 Μ‡ ) (i  : is-set D)
                                          β†’ injective-type D 𝓀 𝓀
                                          ⇔ βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯
 set-injectivity-in-terms-of-ainjectivity {𝓀} (Ξ©β‚€ , eβ‚€) pe D i = Ξ³ , βˆ₯ainjectiveβˆ₯-gives-injective D
  where
   down-≃ : (D β†’ Ξ© 𝓀) ≃ (D β†’ Ξ©β‚€)
   down-≃ = β†’cong' (fe 𝓀 𝓀₀) (fe 𝓀 (𝓀 ⁺)) (≃-sym eβ‚€)

   down : (D β†’ Ξ© 𝓀) β†’ (D β†’ Ξ©β‚€)
   down = ⌜ down-≃ ⌝

   down-is-embedding : is-embedding down
   down-is-embedding = equivs-are-embeddings down (⌜⌝-is-equiv down-≃)

   Id-setβ‚€ : D β†’ (D β†’ Ξ©β‚€)
   Id-setβ‚€ = down ∘ Id-set i

   Id-setβ‚€-is-embedding : is-embedding Id-setβ‚€
   Id-setβ‚€-is-embedding = ∘-is-embedding
                           (Id-set-is-embedding (fe 𝓀 (𝓀 ⁺)) (pe 𝓀) i)
                           down-is-embedding

   injective-set-retract-of-powerset : injective-type D 𝓀 𝓀 β†’ βˆ₯ retract D of (D β†’ Ξ©β‚€) βˆ₯
   injective-set-retract-of-powerset = embedding-βˆ₯retractβˆ₯ D (D β†’ Ξ©β‚€) Id-setβ‚€
                                         Id-setβ‚€-is-embedding

   Ξ©β‚€-injective : ainjective-type Ξ©β‚€ 𝓀 𝓀
   Ξ©β‚€-injective = equiv-to-ainjective Ξ©β‚€ (Ξ© 𝓀) (Ξ©-ainjective (pe 𝓀)) eβ‚€

   Ξ³ : injective-type D 𝓀 𝓀 β†’ βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯
   Ξ³ j = βˆ₯βˆ₯-functor Ο† (injective-set-retract-of-powerset j)
    where
     Ο† : retract D of (D β†’ Ξ©β‚€) β†’ ainjective-type D 𝓀 𝓀
     Ο† = retract-of-ainjective D (D β†’ Ξ©β‚€) (power-of-ainjective Ξ©β‚€-injective)

\end{code}

Added 8th Feb. Solves a problem formulated above.

\begin{code}

 injectivity-in-terms-of-ainjectivity : Ξ©-resizing 𝓀
                                      β†’ is-univalent 𝓀
                                      β†’ (D  : 𝓀 Μ‡ ) β†’ injective-type D 𝓀 𝓀
                                                   ⇔ βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯
 injectivity-in-terms-of-ainjectivity {𝓀} Ο‰β‚€ ua D = Ξ³ , βˆ₯ainjectiveβˆ₯-gives-injective D
  where
   open import Lifting.Size 𝓀
   open ainjectivity-of-Lifting 𝓀

   L : 𝓀 Μ‡
   L = pr₁ (𝓛-resizing Ο‰β‚€ D)

   e : 𝓛 D ≃ L
   e = ≃-sym (prβ‚‚ (𝓛-resizing Ο‰β‚€ D))

   down : 𝓛 D β†’ L
   down = ⌜ e ⌝

   down-is-embedding : is-embedding down
   down-is-embedding = equivs-are-embeddings down (⌜⌝-is-equiv e)

   Ξ΅ : D β†’ L
   Ρ = down ∘ η

   Ξ΅-is-embedding : is-embedding Ξ΅
   Ξ΅-is-embedding = ∘-is-embedding (Ξ·-is-embedding' 𝓀 D ua (fe 𝓀 𝓀)) down-is-embedding

   injective-retract-of-L : injective-type D 𝓀 𝓀 β†’ βˆ₯ retract D of L βˆ₯
   injective-retract-of-L = embedding-βˆ₯retractβˆ₯ D L Ξ΅ Ξ΅-is-embedding

   L-injective : ainjective-type L 𝓀 𝓀
   L-injective = equiv-to-ainjective L (𝓛 D)
                   (free-𝓛-algebra-ainjective ua (fe 𝓀 (𝓀 ⁺)) D) (≃-sym e)

   Ξ³ : injective-type D 𝓀 𝓀 β†’ βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯
   Ξ³ j = βˆ₯βˆ₯-functor Ο† (injective-retract-of-L j)
    where
     Ο† : retract D of L β†’ ainjective-type D 𝓀 𝓀
     Ο† = retract-of-ainjective D L L-injective

\end{code}

Here are some corollaries:

\begin{code}

 injective-resizing : is-univalent 𝓀 β†’ Ξ©-resizing 𝓀
                    β†’ (D : 𝓀 Μ‡ )
                    β†’ injective-type D 𝓀 𝓀
                    β†’ (π“₯ 𝓦 : Universe) β†’ propositional-resizing (π“₯ βŠ” 𝓦) 𝓀 β†’ injective-type D π“₯ 𝓦
 injective-resizing {𝓀} ua Ο‰β‚€ D i π“₯ 𝓦 R = c
  where
   a : βˆ₯ ainjective-type D 𝓀 𝓀 βˆ₯
   a = pr₁ (injectivity-in-terms-of-ainjectivity Ο‰β‚€ ua D) i

   b : βˆ₯ ainjective-type D π“₯ 𝓦 βˆ₯
   b = βˆ₯βˆ₯-functor (ainjective-resizing R D) a

   c : injective-type D π“₯ 𝓦
   c = βˆ₯ainjectiveβˆ₯-gives-injective D b

 EM-gives-pointed-types-injective : EM 𝓀 β†’ (D : 𝓀 Μ‡ ) β†’ D β†’ injective-type D 𝓀 𝓀
 EM-gives-pointed-types-injective {𝓀} em D d = ainjective-gives-injective D
                                                  (EM-gives-pointed-types-ainjective em D d)

 pointed-types-injective-gives-EM : Ξ©-resizing 𝓀
                                  β†’ is-univalent 𝓀
                                  β†’ ((D : 𝓀 Μ‡ ) β†’ D β†’ injective-type D 𝓀 𝓀)
                                  β†’ EM 𝓀
 pointed-types-injective-gives-EM {𝓀} Ο‰ ua Ξ² P i = e
  where
   a : injective-type ((P + Β¬ P) + πŸ™) 𝓀 𝓀
   a = Ξ² ((P + Β¬ P) + πŸ™) (inr ⋆)

   b : βˆ₯ ainjective-type ((P + Β¬ P) + πŸ™) 𝓀 𝓀 βˆ₯
   b = pr₁ (injectivity-in-terms-of-ainjectivity Ο‰ ua ((P + Β¬ P) + πŸ™)) a

   c : βˆ₯ aflabby ((P + Β¬ P) + πŸ™) 𝓀 βˆ₯
   c = βˆ₯βˆ₯-functor (ainjective-types-are-aflabby ((P + Β¬ P) + πŸ™)) b

   d : βˆ₯ P + Β¬ P βˆ₯
   d = βˆ₯βˆ₯-functor (aflabby-EM-lemma P i) c

   e : P + Β¬ P
   e =  βˆ₯βˆ₯-rec (decidability-of-prop-is-prop (fe 𝓀 𝓀₀) i) id d

\end{code}

Fixities:

\begin{code}

infixr 4 _β‰Ύ_

\end{code}