Martin Escardo and Tom de Jong 7th - 21st November 2024.

We improve the universe levels of Lemma 14 of [1], which corresponds
to `embedding-retract` from InjectiveTypes/Blackboard.

We use this to remove resizing assumption of Theorem 51 of [1], which
characterizes the algebraically injective types as the retracts of the
algebras of the lifiting monad (also known as the partial-map
classifier monad.

[1] M.H. EscardΓ³. Injective type in univalent mathematics.
    https://doi.org/10.1017/S0960129520000225

\begin{code}

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

open import UF.FunExt

module InjectiveTypes.CharacterizationViaLifting (fe : FunExt) where

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

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

\end{code}

We first improve the universe levels of Blackboard.ainjectivity-of-Lifting.

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

 Ξ·-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)

\end{code}

The following improves the universe levels of Lemma 50 of [1].

\begin{code}

 ainjective-is-retract-of-free-𝓛-algebra' : ({𝓀} π“₯ {𝓦} : Universe)
                                            (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}

The following removes the resizing assumption of Theorem 51 of [1].

\begin{code}

 ainjectives-in-terms-of-𝓛-algebras
  : (D : 𝓀 Μ‡ ) β†’ ainjective-type D 𝓣 𝓣 ↔ (Ξ£ A κž‰ 𝓣 ⁺ βŠ” 𝓀 Μ‡ , 𝓛-alg A Γ— retract D of A)
 ainjectives-in-terms-of-𝓛-algebras {𝓀} D = a , b
  where
   a : ainjective-type D 𝓣 𝓣 β†’ (Ξ£ A κž‰ 𝓣 ⁺ βŠ” 𝓀 Μ‡ , 𝓛-alg A Γ— retract D of A)
   a i = 𝓛 D ,
         𝓛-algebra-gives-alg (free-𝓛-algebra ua D) ,
         ainjective-is-retract-of-free-𝓛-algebra' 𝓣 D i

   b : (Ξ£ A κž‰ 𝓣 ⁺ βŠ” 𝓀 Μ‡ , 𝓛-alg A Γ— retract D of A) β†’ ainjective-type D 𝓣 𝓣
   b (A , Ξ± , ρ) = retract-of-ainjective D A (𝓛-alg-ainjective pe A Ξ±) ρ

\end{code}

Particular case of interest:

\begin{code}

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

\end{code}