code formatting

martinescardo · Nov 7, 2024 · aa0e521 · aa0e521
1 parent a9e7027
commit aa0e521
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/source/InjectiveTypes/OverSmallMaps.lagda b/source/InjectiveTypes/OverSmallMaps.lagda
@@ -137,7 +137,7 @@ module ainjectivity-of-Lifting'
  open import UF.UA-FunExt
  open import UF.EquivalenceExamples
 
- η-is-small-map : {X : 𝓤 ̇} → (η ∶ (X → 𝓛 X)) is 𝓣 small-map
+ η-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)