change of implicit arguments with Tom de Jong

martinescardo · Nov 14, 2024 · 2c3ce3d · 2c3ce3d
1 parent d4ee556
commit 2c3ce3d
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 3 deletions.
diff --git a/source/InjectiveTypes/Resizing.lagda b/source/InjectiveTypes/Resizing.lagda
@@ -144,7 +144,7 @@ small-ainjective-type-with-two-distinct-points-gives-Ω¬¬-resizing
   f ₁ = x₁
 
   I : Σ s ꞉ (Ω¬¬ 𝓤 → D) , s ∘ 𝟚-to-Ω¬¬ ∼ f
-  I = ainjectivity-over-small-maps {𝓤₀} {𝓤 ⁺} {𝓤} {𝓤} {𝓥} {𝓦}
+  I = ainjectivity-over-small-maps 𝓥
        D
        D-ainj
        𝟚-to-Ω¬¬

diff --git a/source/InjectiveTypes/Subtypes.lagda b/source/InjectiveTypes/Subtypes.lagda
@@ -39,7 +39,7 @@ module _ (D : 𝓤 ̇ )
  necessary-condition-for-injectivity-of-subtype {𝓦} {𝓣} Σ-ainj = f , g , h
   where
    ρ : retract Σ P of D
-   ρ = embedding-retract' {𝓤 ⊔ 𝓥} {𝓤} {𝓣} {𝓥} {𝓦}
+   ρ = embedding-retract' 𝓦
         (Σ P)
         D
         s

diff --git a/source/Taboos/Decomposability.lagda b/source/Taboos/Decomposability.lagda
@@ -529,7 +529,7 @@ ainjective-types-have-Ω-Paths {𝓥} {𝓤} {𝓦} pe D D-ainj x₀ x₁ = II I
   f ₁ = x₁
 
   I : Σ g ꞉ (Ω 𝓥 → D) , g ∘ 𝟚-to-Ω ∼ f
-  I = ainjectivity-over-small-maps {𝓤₀} {𝓥 ⁺} {𝓤} {𝓥} {𝓥} {𝓦}
+  I = ainjectivity-over-small-maps 𝓥
        D
        D-ainj
        𝟚-to-Ω

diff --git a/source/UF/UniverseEmbedding.lagda b/source/UF/UniverseEmbedding.lagda
@@ -160,6 +160,9 @@ prop-fiber-criterion : PropExt
                      → is-prop (fiber f Q)
 prop-fiber-criterion pe fe 𝓤 𝓥 f i Q j (P , r) = d (P , r)
  where
+  _ : f P ＝ Q
+  _ = r
+
   k : is-prop (f P)
   k = transport⁻¹ is-prop r j