Martin Escardo, August 2023

Algebraic injectivity over small maps.

\begin{code}

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

open import UF.FunExt

module InjectiveTypes.OverSmallMaps (fe : FunExt) where

open import InjectiveTypes.Blackboard fe
open import MLTT.Spartan
open import UF.Embeddings
open import UF.Equiv
open import UF.Size
open import UF.Subsingletons

private
 fe' : Fun-Ext
 fe' {𝓀} {π“₯} = fe 𝓀 π“₯

\end{code}

Added 3rd August 2023. Extensions over small embeddings induced by
algebraic flabbiness. The point is to reduce size without resizing
axioms. An application is in Taboos.Decomposability.

\begin{code}

module _ (D : 𝓦 Μ‡ )
         (D-is-flabby : aflabby D 𝓣)
         {X : 𝓀 Μ‡ }
         {Y : π“₯ Μ‡ }
         (j : X β†’ Y)
         (j-is-embedding : is-embedding j)
         (j-small : j is 𝓣 small-map)
         (f : X β†’ D)
       where

 private
  R : Y β†’ 𝓣 Μ‡
  R y = resized (fiber j y) (j-small y)

  ρ : (y : Y) β†’ R y ≃ fiber j y
  ρ y = resizing-condition (j-small y)

  R-is-prop : (y : Y) β†’ is-prop (R y)
  R-is-prop y = equiv-to-prop (ρ y) (j-is-embedding y)

  e : (y : Y) β†’ Ξ£ d κž‰ D , ((r : R y) β†’ d ＝ f (pr₁ (⌜ ρ y ⌝ r)))
  e y = D-is-flabby (R y) (R-is-prop y) (Ξ» r β†’ f (pr₁ (⌜ ρ y ⌝ r)))

 sflabby-extension : (Y β†’ D)
 sflabby-extension y = pr₁ (e y)

 sflabby-extension-property : sflabby-extension ∘ j ∼ f
 sflabby-extension-property x =
  sflabby-extension (j x)                 ＝⟨ I ⟩
  f (pr₁ (⌜ ρ (j x) ⌝ (⌜ ρ (j x) ⌝⁻¹ w))) ＝⟨ II ⟩
  f (pr₁ w)                               ＝⟨ refl ⟩
  f x                                     ∎
  where
   w : fiber j (j x)
   w = x , refl

   I  = prβ‚‚ (e (j x)) (⌜ ρ (j x) ⌝⁻¹ w)
   II = ap (f ∘ pr₁) (≃-sym-is-rinv (ρ (j x)) w)

 aflabbiness-gives-injectivity-over-small-maps : Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ f
 aflabbiness-gives-injectivity-over-small-maps = sflabby-extension ,
                                                 sflabby-extension-property
\end{code}

An extension property for injective types, with more general universes
and less general embeddings.

\begin{code}

ainjectivity-over-small-maps : {𝓀 π“₯ 𝓦 𝓣₀ 𝓣₂ : Universe}
                             β†’ (𝓣₁ : Universe)
                             β†’ (D : 𝓦 Μ‡ )
                             β†’ ainjective-type D (𝓣₀ βŠ” 𝓣₁) 𝓣₂
                             β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                               (j : X β†’ Y)
                             β†’ is-embedding j
                             β†’ j is 𝓣₀ small-map
                             β†’ (f : X β†’ D) β†’ Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ f
ainjectivity-over-small-maps {𝓀} {π“₯} {𝓦} {𝓣₀} {𝓣₂} 𝓣₁ D D-ainj =
 aflabbiness-gives-injectivity-over-small-maps D
  (aflabbiness-resizing₁ {𝓦} {𝓣₀} {𝓣₁} D (ainjective-types-are-aflabby D D-ainj))

\end{code}

Added by Martin Escardo and Tom de Jong 24th October 2024. This
improves the universe levels of BlackBoard.embedding-retract.

\begin{code}

open import UF.Retracts

embedding-retract' : {𝓀 π“₯ 𝓦 𝓣 : Universe}
                   β†’ (𝓣' : Universe)
                   β†’ (D : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ ) (j : D β†’ Y)
                   β†’ is-embedding j
                   β†’ j is 𝓣 small-map
                   β†’ ainjective-type D (𝓣 βŠ” 𝓣') 𝓦
                   β†’ retract D of Y
embedding-retract' 𝓣' D Y j e s i = pr₁ a , j , prβ‚‚ a
 where
  a : Ξ£ f' κž‰ (Y β†’ D) , f' ∘ j ∼ id
  a = ainjectivity-over-small-maps 𝓣' D i j e s id

\end{code}