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.