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

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  #-}

open import UF-FunExt

module InjectiveTypes (fe : FunExt) where

open import SpartanMLTT

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

\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 = Ξ  w κ fiber j y , f (prβ w)
Ξ£-extension y = Ξ£ w κ fiber j y , f (prβ w)

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 (back-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-in-range : is-embedding j β (x : X) β f/j (j x) β f x
Ξ -extension-in-range e x = prop-indexed-product (fe (π€ β π₯) π¦) {fiber j (j x)} {Ξ» (z : fiber j (j x)) β f (prβ z)} (e (j x)) (x , refl)

Ξ -extension-equivalence : is-embedding j β (x : X) β is-equiv (Ξ -proj (x , refl))
Ξ -extension-equivalence e x = prβ (Ξ -extension-in-range 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-in-range : is-embedding j β (x : X) β fβj (j x) β f x
Ξ£-extension-in-range 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-in-range 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-in-range e a))

\end{code}

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}

(Conjectural conjecture (2nd July 2018): if j is an embedding, then we
have an embedding Ξ£ f β Ξ£ f/j.)

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}

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}

\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-in-range 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-in-range 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-in-range 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}

\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 (prβ 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}

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 (prβ 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.

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}

\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) = back-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}

\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 (Ξ© (π€ β π₯)) π€ π₯

\end{code}

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}

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}

\begin{code}

module ainjectivity-of-Lifting (π€ : Universe) where

open import Lifting π€ public
open import LiftingAlgebras π€
open import LiftingEmbeddingViaSIP π€ 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

\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).

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

\begin{code}

β 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-β = βcong' (fe π€ π€β) (fe π€ (π€ βΊ)) (β-sym eβ)

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-type D π€ π€ β β₯ ainjective-type D π€ π€ β₯
Ξ³ j = β₯β₯-functor Ο (injective-set-retract-of-powerset j)
where
Ο : retract D of (D β Ξ©β) β ainjective-type D π€ π€

\end{code}

Added 8th Feb. Solves a problem formulated above.

\begin{code}

β is-univalent π€
β (D  : π€ Μ ) β injective-type D π€ π€
β β₯ ainjective-type D π€ π€ β₯
injectivity-in-terms-of-ainjectivity {π€} Οβ ua D = Ξ³ , β₯ainjectiveβ₯-gives-injective D
where
open import LiftingSize π€
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}