Martin Escardo, August 2023

More about injectivity.

\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}
                             β†’ (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. As an
application of the above, we get the following version of
embedding-retract from InjectiveTypes/Blackboard with better universe
levels.

\begin{code}

open import UF.Retracts

embedding-retract' : {𝓀 π“₯ 𝓦 𝓣 𝓣' : 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}

Added by Martin Escardo and Tom de Jong 7th November 2024. We now
improve the universe levels of the module ainjectivity-of-Lifting in
the file BlackBoard.

\begin{code}

open import UF.Univalence

module ainjectivity-of-Lifting'
        (𝓣 : Universe)
        (ua : is-univalent 𝓣)
       where

 private
  pe : propext 𝓣
  pe = univalence-gives-propext ua

 open ainjectivity-of-Lifting 𝓣

 open import Lifting.UnivalentPrecategory 𝓣
 open import UF.UA-FunExt
 open import UF.EquivalenceExamples

 Ξ·-is-small-map : {X : 𝓀 Μ‡ } β†’ (Ξ· ∢ (X β†’ 𝓛 X)) is 𝓣 small-map
 Ξ·-is-small-map {𝓀} {X} l = is-defined l ,
                            ≃-sym (Ξ·-fiber-same-as-is-defined X pe fe' fe' fe' l)

 ainjective-is-retract-of-free-𝓛-algebra' : (D : 𝓀 Μ‡ )
                                          β†’ ainjective-type D (𝓣 βŠ” π“₯) 𝓦
                                          β†’ retract D of (𝓛 D)
 ainjective-is-retract-of-free-𝓛-algebra' {𝓀} {π“₯} {𝓦} D =
  embedding-retract' {𝓀} {𝓣 ⁺ βŠ” 𝓀} {𝓦} {𝓣} {π“₯} D (𝓛 D) Ξ·
   (Ξ·-is-embedding' 𝓀 D ua fe')
   Ξ·-is-small-map

 ainjectives-in-terms-of-free-𝓛-algebras'
  : (D : 𝓀 Μ‡ ) β†’ ainjective-type D 𝓣 𝓣 ↔ (Ξ£ X κž‰ 𝓀 Μ‡ , retract D of (𝓛 X))
 ainjectives-in-terms-of-free-𝓛-algebras' {𝓀} D = a , b
  where
   a : ainjective-type D 𝓣 𝓣 β†’ Ξ£ X κž‰ 𝓀 Μ‡ , retract D of (𝓛 X)
   a i = D , ainjective-is-retract-of-free-𝓛-algebra' {𝓀} {𝓣} {𝓣} D i

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

\end{code}

A particular case of interest that arises in practice is the following.

\begin{code}

 ainjectives-in-terms-of-free-𝓛-algebras⁺
  : (D : 𝓣 ⁺ Μ‡ ) β†’ ainjective-type D 𝓣 𝓣 ↔ (Ξ£ X κž‰ 𝓣 ⁺ Μ‡ , retract D of (𝓛 X))
 ainjectives-in-terms-of-free-𝓛-algebras⁺ =  ainjectives-in-terms-of-free-𝓛-algebras'

 _ : {X : 𝓣 ⁺ Μ‡ } β†’ type-of (𝓛 X) ＝ 𝓣 ⁺ Μ‡
 _ = refl

\end{code}