update README

martinescardo · Sep 6, 2023 · bc6402c · bc6402c
1 parent 77bb868
commit bc6402c
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 7 deletions.
diff --git a/README.md b/README.md
@@ -28,7 +28,7 @@ with only your name as author.
 
 ## Root of the development
 
- * [source/index.lagda](source/index.lagda) (only `--safe` modules`).
+ * [source/index.lagda](source/index.lagda) (only `--safe` modules).
 
  * [source/AllModulesIndex.lagda](source/AllModulesIndex.lagda) (including "unsafe" ones).
 

diff --git a/source/InjectiveTypes/MathematicalStructures.lagda b/source/InjectiveTypes/MathematicalStructures.lagda
@@ -306,10 +306,10 @@ equivalently formulated with T:
 
    σ-and-τ-agree : σ ∼ τ
    σ-and-τ-agree s =
-    σ s                                                       ＝⟨ refl ⟩
-    ((λ h → transport S (eqtoid (ua 𝓤) (Π A) (A h) (π h)) s)) ＝⟨ I ⟩
-    (λ h → T (π h) s)                                         ＝⟨ refl ⟩
-    τ s                                                       ∎
+    σ s                                                     ＝⟨ refl ⟩
+    (λ h → transport S (eqtoid (ua 𝓤) (Π A) (A h) (π h)) s) ＝⟨ I ⟩
+    (λ h → T (π h) s)                                       ＝⟨ refl ⟩
+    τ s                                                     ∎
     where
      I = dfunext fe' (λ h → (transport-eqtoid (π h) s)⁻¹)
 
@@ -461,8 +461,9 @@ such as the above, form injective types.
 
 \begin{code}
 
-variable
- 𝓥₁ 𝓥₂ : Universe
+private
+ variable
+  𝓥₁ 𝓥₂ : Universe
 
 closure-under-prop-Π-× :
       {S₁ : 𝓤 ̇ → 𝓥₁ ̇ } {S₂ : 𝓤 ̇ → 𝓥₂ ̇ }

diff --git a/source/InjectiveTypes/index.lagda b/source/InjectiveTypes/index.lagda
@@ -64,6 +64,7 @@ import Iterative.Multisets-Addendum
 import Iterative.Sets-Addendum
 import Iterative.Ordinals
 import InjectiveTypes.MathematicalStructures
+import InjectiveTypes.Sigma
 
 \end{code}