Martin Escardo, 27 April 2014

(Right-Kan) Injectivity of the universe.
----------------------------------------

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

We show that the universe is (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=U, a universe, in which case, if one
doesn't want to assume univalence, then it makes sense to consider
commutation up to "isomorphism":

                   j
              X ------> Y
               \       / 
                \  ≅  /
             f   \   / f/j
                  \ /
                   v
                   U

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
                   U

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

\begin{code}

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

module InjectivityOfTheUniverse where

open import SpartanMLTT
open import Sets
open import Fibers
open import Equivalence

\end{code}

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

                   j
              X ------> Y
               \       / 
                \  <- /
             f   \   / f/j
                  \ /
                   v
                   U


\begin{code}

_/_ : {X Y : U}  (X  U)  (X  Y)  Y  U
(f / j)(y) = (w : j ⁻¹ y)  f(pr₁ w)

\end{code}

For arbitrary j:X→Y, this gives a right Kan extension:

\begin{code}

right-kan-extension₀ : {X Y : U} (f : X  U) (j : X  Y)
     (x : X)  (f / j)(j x)  f x
right-kan-extension₀ f j x t = t(x , refl)

right-kan-extension₁ : {X Y : U} (f : X  U) (j : X  Y) (g : Y  U) 
     ((x : X)  g(j x)  f x)
     (y : Y)  g y  (f / j) y
right-kan-extension₁ f j g t y a (x , p) = t x (transport g p a)

\end{code}

The above formula actually gives an extension up to pointwise
isomorphism if j:X→Y is an embedding in the sense of HoTT.

\begin{code}

open import Embedding
open import Prop-indexed-product

extension-in-range : {X Y : U} (f : X  U) (j : X  Y)  embedding j  (x : X)  (f / j)(j x)  f x
extension-in-range f j e x = prop-indexed-product  y y'  e (j x) y y') (x , refl)

extension-out-of-range : {X Y : U} (f : X  U) (j : X  Y)  (y : Y)  ((x : X)  y  j x)  (f / j) y  𝟙
extension-out-of-range {X} {Y} f j y φ = prop-indexed-product-one (uncurry φ)

\end{code}

We now rewrite the extension formula in an equivalent way:

\begin{code}

2nd-extension-formula : {X Y : U} (f : X  U) (j : X  Y) (y : Y) 
                       (f / j)(y)  ((x : X)  y  j x  f x)
2nd-extension-formula f j x = Curry-Uncurry

\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 : {X Y : U} (f : X  U) (a : X) (j : X  Y)  embedding j 
         ((x : X)  j a  j x  f x)  f a
observation f a j e = ≃-trans (≃-sym (2nd-extension-formula f j (j a))) (extension-in-range f j e a)

\end{code}

Mini-appendix. 

\begin{code}

open import Injection

embedding-is-injective : {X Y : U} (j : X  Y)  embedding j  left-cancellable j
embedding-is-injective j e {x} {x'} p = ap pr₁ (e (j x) (x , refl) (x' , p))

\end{code}

The point is that "injective" is too weak for the above theorem. One
really does need the HoTT notion of embedding for the universe to be
injective.

To do. (Dis)prove the following conjecture. If f/j is an extension of
f for every f then j is an embedding.