improve universe levels of ainjectives as retracts of free lifting al…

…gebras

Co-authored-by: Tom de Jong <[email protected]>

source/InjectiveTypes/Blackboard.lagda

@@ -1427,7 +1427,7 @@ Added 23rd January 2019:
 module ainjectivity-of-Lifting (𝓤 : Universe) where
 
  open import Lifting.Construction 𝓤 public
- open import Lifting.Algebras 𝓤
+ open import Lifting.Algebras 𝓤 public
  open import Lifting.EmbeddingViaSIP 𝓤 public
 
 \end{code}
@@ -1439,33 +1439,26 @@ free 𝓛-algebras are injective.
 \begin{code}
 
  𝓛-alg-aflabby : propext 𝓤
-               → funext 𝓤 𝓤
-               → funext 𝓤 𝓥
                → {A : 𝓥 ̇ }
                → 𝓛-alg A
                → aflabby A 𝓤
- 𝓛-alg-aflabby pe fe fe' (∐ , κ , ι) P i f = ∐ i f , γ
+ 𝓛-alg-aflabby pe (∐ , κ , ι) P i f = ∐ i f , γ
   where
    γ : (p : P) → ∐ i f ＝ f p
-   γ p = 𝓛-alg-Law₀-gives₀' pe fe fe' ∐ κ P i f p
+   γ p = 𝓛-alg-Law₀-gives₀' pe fe' fe' ∐ κ P i f p
 
  𝓛-alg-ainjective : propext 𝓤
-                  → funext 𝓤 𝓤
-                  → funext 𝓤 𝓥
                   → (A : 𝓥 ̇ )
                   → 𝓛-alg A
                   → ainjective-type A 𝓤 𝓤
- 𝓛-alg-ainjective pe fe fe' A α = aflabby-types-are-ainjective A
-                                    (𝓛-alg-aflabby pe fe fe' α)
+ 𝓛-alg-ainjective pe A α = aflabby-types-are-ainjective A
+                            (𝓛-alg-aflabby pe α)
 
  free-𝓛-algebra-ainjective : is-univalent 𝓤
-                           → funext 𝓤 (𝓤 ⁺)
-                           → (X : 𝓤 ̇ ) → ainjective-type (𝓛 X) 𝓤 𝓤
- free-𝓛-algebra-ainjective ua fe X =
+                           → (X : 𝓥 ̇ ) → ainjective-type (𝓛 X) 𝓤 𝓤
+ free-𝓛-algebra-ainjective ua X =
   𝓛-alg-ainjective
    (univalence-gives-propext ua)
-   (univalence-gives-funext ua)
-   fe
    (𝓛 X)
    (𝓛-algebra-gives-alg (free-𝓛-algebra ua X))
 
@@ -1507,7 +1500,7 @@ monad:
    b (X , r) = retract-of-ainjective
                 D
                 (𝓛 X)
-                (free-𝓛-algebra-ainjective ua fe X)
+                (free-𝓛-algebra-ainjective ua X)
                 r
 
 \end{code}
@@ -1755,7 +1748,7 @@ Added 8th Feb. Solves a problem formulated above.
 
    L-injective : ainjective-type L 𝓤 𝓤
    L-injective = equiv-to-ainjective L (𝓛 D)
-                   (free-𝓛-algebra-ainjective ua (fe 𝓤 (𝓤 ⁺)) D) (≃-sym e)
+                   (free-𝓛-algebra-ainjective ua D) (≃-sym e)
 
    γ : injective-type D 𝓤 𝓤 → ∥ ainjective-type D 𝓤 𝓤 ∥
    γ j = ∥∥-functor φ (injective-retract-of-L j)

source/InjectiveTypes/OverSmallMaps.lagda

@@ -92,7 +92,10 @@ ainjectivity-over-small-maps {𝓤} {𝓥} {𝓦} {𝓣₀} {𝓣₁} {𝓣₂}
 
 \end{code}
 
-Added by Martin Escardo and Tom de Jong 24th October 2024.
+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}
 
@@ -110,3 +113,63 @@ embedding-retract' {𝓤} {𝓥} {𝓦} {𝓣} {𝓣'} D Y j e s i = pr₁ a , j
   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}